Probability

Motivation

Remote driving, or tele-driving, lets a human operator in a control center drive a vehicle over a wireless link. A ride-hailing platform that adopts it decouples drivers from vehicles: a driver is attached to a vehicle only while that vehicle carries or fetches a customer, and is released the moment the trip ends. Since an idle vehicle needs no driver, the platform can run a fleet of $m$ vehicles with $n \le m$ drivers. The operational question is how much service is lost by having fewer drivers than vehicles.

Benjaafar, Wang and Yang study this question with a loss queue in which the service rate depends on the number of idle vehicles, capturing the fact that pickups take longer when fewer vehicles are free (SSRN 4130757; published in Management Science, 2024, doi:10.1287/mnsc.2022.01687). The state-dependent rate builds on the spatial capacity model of Besbes, Castro and Lobel (doi:10.1287/opre.2021.2112). Their main finite-system results describe how the service level changes with the number of drivers in three regimes of vehicle supply. This mission formalizes the third regime, where vehicles are ample. The source is the authors' 2023 SSRN working paper; all labels and page numbers below refer to it.

Setting

A fleet of $m$ vehicles is operated by $n \le m$ remote drivers. Customers request trips according to a Poisson process with rate $\lambda > 0$. A request that arrives when all $n$ drivers are busy is lost. When $q$ customers are in service, each one completes at rate $\mu(m,q)$, so the total completion rate is $q\,\mu(m,q)$. The rate is defined for real $q \in [1,m]$. Let

$$\rho(q) = \frac{\lambda}{q\,\mu(m,q)}.$$

The number of customers in service is a birth–death chain on $\{0,\dots,n\}$. Its stationary law is

$$\pi_{m,n}(q) = \frac{\prod_{k=1}^{q}\rho(k)}{1 + \sum_{i=1}^{n}\prod_{k=1}^{i}\rho(k)}, \qquad 0 \le q \le n,$$

and the service level is the long-run fraction of demand served, $SL(m,n) = 1 - \pi_{m,n}(n)$.

The paper's standing assumptions on the rate are:

• Assumption 1. $\mu(m,q)$ is strictly increasing in $m$, decreasing in $q$, and strictly concave in $q$; $\mu(m,q) \to 1/s$ as $m \to \infty$, where $s > 0$ is the expected trip time; and $\mu(m,m)$ does not depend on $m$.
• Assumption 2. There is $\bar m > 0$ such that, for every $m \ge \bar m$, the map $q \mapsto q\,\mu(m,q)$ first increases and then decreases.
• Size restriction (p. 13). $m \ge \bar m$ and $\lambda > \max\{1/s,\ \max_{q \le \bar m} q\,\mu(\bar m,q)\}$.

The supply-rich regime $m > \gamma_2(\lambda)$ is the case $\rho(m) < 1$, that is, $\lambda < m\,\mu(m,m)$: even with every vehicle busy, the system clears work faster than it arrives. In this regime there is a unique $q_3 \in (1,m)$ with $\rho(q_3) = 1$, and $\rho(q) < 1$ exactly when $q > q_3$.

Formalization targets

Goal: Theorem 1.C (pp. 20–21)

In the supply-rich regime, $SL(m,n)$ is strictly increasing in $n \in \{1,\dots,m\}$. For every $n \in \{1,\dots,m\}$ with $n > q_3$,

$$SL(m,n) > 1 - \frac{1}{n - \lfloor q_3 \rfloor}.$$

Milestones

1. Lemma 3, first sentence: $\rho$ is strictly convex and $1/\rho$ is strictly concave on $[1,m]$.
2. Lemma 3(iii): in the supply-rich regime the root $q_3$ exists, with $\rho < 1$ exactly to its right.
3. Lemma 4: $\pi_{m,n-1}(n-1) > \pi_{m,n}(n)$ holds if and only if $\pi_{m,n-1}(n-1) > (\rho(n)-1)/\rho(n)$, and if and only if $\pi_{m,n}(n) > (\rho(n)-1)/\rho(n)$.
4. App. C.3: $\pi_{m,n}(n)$ is strictly decreasing in $n \in \{1,\dots,m\}$.
5. App. C.3: $\pi_{m,n}(n) < 1/(n - \lfloor q_3 \rfloor)$ for $q_3 < n \le m$.

Significance

The first part of Theorem 1.C says that, when vehicles are ample, every driver removed costs some service. The second part says the cost is small once $n$ exceeds $q_3$ by a margin. The bound $1 - 1/(n - \lfloor q_3 \rfloor)$ is increasing and concave in $n$, so a platform can run noticeably fewer drivers than vehicles at a controlled loss of service. The paper's numerical study (Figure 7) reports reductions of 35–60% in the number of drivers at a service loss below 0.01. The same objects carry over to the paper's asymptotic Theorem 2.C, where the driver-to-vehicle ratio needed in a large supply-rich market tends to $1/\alpha$.

The result is proved on paper and has no machine-checked proof. The work this mission adds is formal:

• statements of the model in which the regimes are explicit and the threshold $q_3$ is pinned by its characterization;
• a proof of the convexity and root structure of $\rho$ that does not rely on second derivatives, which the paper uses but the assumptions do not supply;
• the comparison lemma for consecutive blocking probabilities, which the companion missions on this paper also use.

Difficulty

$\pi_{m,n}(n)$ is a ratio whose numerator and denominator both change with $n$. For the drivers beyond $q_3$, monotonicity is immediate, since each additional factor $\rho(n) < 1$ shrinks the numerator while the denominator grows. Below $q_3$, $\rho(n) \ge 1$ and the numerator grows, so that argument fails, and the comparison has to use the shape of $\rho$ on $[1, q_3]$. The shape of $\rho$ (Lemma 3) has to be derived from concavity and monotonicity of $\mu$ alone: the assumptions give no smoothness, although the paper's proof differentiates twice. The page argues the two ranges separately, so the step across $q_3$ also has to be covered. The lower bound needs care at the integer part of $q_3$: the sum in the denominator is taken from $\lfloor q_3 \rfloor$, which is at least 1 only because $q_3 > 1$.

Formalization scope

• The rate is a function $\mu : \mathbb N \to \mathbb R \to \mathbb R$, with $m$ natural and $q$ real. Assumptions 1–2 are imposed only for $q \in [1,m]$. "Decreasing in $q$" is read as non-increasing. Positivity of $\mu$ and $s > 0$, implicit on the page, are stated. Assumption 2's "first increases then decreases" is a turning point strictly inside $(1,m)$.
• Every statement carries Assumptions 1–2 and the size restriction as explicit hypotheses. The regime $m > \gamma_2(\lambda)$ is stated through its characterization $\lambda < m\,\mu(m,m)$; $\gamma_2$ itself is not defined.
• $q_3$ is a real variable with its Lemma 3(iii) characterization: $q_3 \in [1,m]$, $\rho(q_3) = 1$, and $\rho(q) < 1$ exactly for $q > q_3$ in $[1,m]$. This determines $q_3$ uniquely, and milestone 2 shows that such a $q_3$ exists. No monotonicity of $\rho$, $\pi$ or $SL$ is assumed anywhere; such facts are milestones.
• $n$ ranges over $\{1,\dots,m\}$. $\lfloor q_3 \rfloor$ is the natural-number floor, and $n - \lfloor q_3 \rfloor$ is computed in $\mathbb R$.
• "Increasing" and "lower bounded" are stated strictly, as the paper's proof derives them.
• A statement that assumed $\pi_{m,n}(n)$ decreasing, or left $q_3$ unconstrained, would make the goal trivial or vacuous. Neither is done here.

Needed infrastructure: finite products and sums over Finset.Icc, StrictConvexOn/StrictConcaveOn on intervals, and the intermediate value theorem for a function that is continuous on $[1,m)$. The model file is shared, up to namespace, with four companion missions on the same paper. Proofs of the general facts used here are reusable beyond this mission and are welcome as separate contributions: the product of a positive increasing linear function and a positive antitone concave function is concave, and the reciprocal of a positive strictly concave function is strictly convex.

Selected references

• S. Benjaafar, Z. Wang, X. Yang, Human in the Loop Automation: Ride-Hailing with Remote (Tele-)Drivers, SSRN working paper 4130757, version of 1 June 2023. https://ssrn.com/abstract=4130757 . Published in Management Science, 2024. https://doi.org/10.1287/mnsc.2022.01687
• O. Besbes, F. Castro, I. Lobel, Spatial Capacity Planning, Operations Research 70(2):1271–1291, 2022. https://doi.org/10.1287/opre.2021.2112

Motivation

Decision makers facing uncertainty treat different sources of uncertainty differently. The Ellsberg paradox, home bias in investment, and the competence effect all show people preferring bets on one source (a known urn, domestic stocks, a familiar domain) over equally likely bets on another. Ambiguity theories try to describe these differences. Most of them are hard to apply empirically because they work with sets of priors or nonadditive measures on the whole state space.

Baillon, Bleichrodt, Li and Wakker (Management Science 71(10), 2025) propose source theory. Within a source, the agent behaves as if she has a probability measure (probabilistic sophistication). Across sources, she may weight those probabilities differently, through a source function $w_{\mathcal S}$. Two attitude components measure the difference between sources: source preference (ambiguity aversion) and insensitivity (a-insensitivity, the tendency to treat all intermediate likelihoods alike). Their Theorem 4 answers a basic question for this framework. When are two sources at exactly the same level on both components?

Setting

A state space $S$ carries an algebra $\mathcal E$ of events. An act is a finite-valued map $x : S \to \Gamma$ into an outcome set $\Gamma$ whose level sets are events. A weak order $\succcurlyeq$ on acts is represented by biseparable utility: a utility $U$ on outcomes and a weighting function $W$ on events ($W(\emptyset)=0$, $W(S)=1$, monotone) evaluate a binary act $\gamma E \beta$ with $\gamma \succcurlyeq \beta$ by $W(E)U(\gamma) + (1-W(E))U(\beta)$. Structural Assumption 1 adds three nonindifferent outcomes, convex rangedness of $W$, strong monotonicity, cumulative dominance and an Archimedean axiom. Events are ranked by $W$: $A \succcurlyeq B$ iff $W(A) \ge W(B)$.

A source is a subalgebra $\mathcal S \subseteq \mathcal E$ on which $W$ is convex ranged. It is uniform if a finitely additive probability measure $P_{\mathcal S}$ on $\mathcal S$ satisfies stochastic dominance for all acts from $\mathcal S$. Then $W = w_{\mathcal S} \circ P_{\mathcal S}$ on $\mathcal S$ for a continuous, strictly increasing $w_{\mathcal S} : [0,1] \to [0,1]$, the source function.

For two sources $\mathcal A$ and $\mathcal C$:

• $\mathcal C$ is preferred to $\mathcal A$ (Definition 2) if for $A_1 \in \mathcal A$, $C_1 \in \mathcal C$, $W(A_1) = W(C_1)$ implies $W(A_1^c) \le W(C_1^c)$.
• $\mathcal A$ is more insensitive than $\mathcal C$ with insensitivity region $[B, D]$ (Definition 4) if, for matching threefold partitions, the middle cell of $\mathcal A$ gains at least as much weight as that of $\mathcal C$ when moved from the worst to the middle rank (if the worst cell is large enough, bounded by $D$), and dually at the best rank (if the best cell is at least as likely as $B$).
• The region $[B, D]$ is regular for $\mathcal S$ if every fourfold partition of $S$ from $\mathcal S$ has a cell $E_j$ with $E_j \succcurlyeq B$ and $E_j^c \preccurlyeq D$.
• Two sources are equally preferred (equally insensitive) if the relation holds in both directions.

Formalization targets

Goal: Theorem 4

Under Assumption 1, sources $\mathcal A$ and $\mathcal C$ are equally preferred and equally insensitive with a regular insensitivity region if and only if both are uniform and

$$w_{\mathcal A} = w_{\mathcal C}.$$

Moreover, $\mathcal A$ and $\mathcal C$ are then equally insensitive with the maximal region $[\emptyset, S]$.

Milestones

In the order of the proof (p. 8780):

1. the reversed implication, which the paper calls direct;
2. transitivity of source preference and insensitivity (Observation 3);
3. Theorem 1: a source is uniform iff it is equally preferred and insensitive to itself with a regular region;
4. for a uniform source, a regular region $[B, D]$ from the source has $P(B) \le \tfrac14 \le \tfrac34 \le P(D)$;
5. for equally preferred uniform sources, the pmatcher $\varphi$ with $w_{\mathcal A} = w_{\mathcal C} \circ \varphi$ satisfies $\varphi(p) + \varphi(1-p) = 1$, so $\varphi(\tfrac12) = \tfrac12$;
6. insensitivity in each direction makes $\varphi$ and $\varphi^{-1}$ sub-additive on $[0, \tfrac12]$;
7. these two inequalities and $\varphi(\tfrac12) = \tfrac12$ force $\varphi$ to be linear on $[0, \tfrac12]$;
8. $\varphi$ is then the identity on $[0, 1]$.

Significance

The theorem says that a comparison of ambiguity attitudes "at the same level" is only possible between uniform sources. Equal preference and equal insensitivity, both observable through bets, already force probabilistic sophistication within each source and identical source functions. With risk as the second source, it characterizes ambiguity neutrality of a source behaviorally (Corollary 1 of the paper). It also shows that both attitude components are needed: the paper's Example 1 exhibits sources that are equally preferred but differ in insensitivity.

The result is proved in the paper, partly by reference. The linearity step defers to an Online Appendix, and Theorem 1's proof relies on a representation theorem of Krantz, Luce, Suppes and Tversky (1971). As far as known, none of the paper's results has a machine-checked proof. A formalization would check the paper's proof, including the deferred functional-equation step and the boundary bookkeeping of insensitivity regions. It would also provide a reusable Lean layer for Savage-style acts, biseparable utility and comparative ambiguity attitudes.

Difficulty

The forward direction is the hard one. The obvious route is to compare the two sources directly through the pmatcher $\varphi$. But $\varphi$ exists only once both sources are known to be uniform, and nothing in the hypotheses says so. The proof first collapses the cross-source conditions into conditions of each source with itself, by transitivity, and then invokes Theorem 1. Theorem 1 in turn needs a qualitative-probability representation theorem.

Once $\varphi$ exists, the insensitivity conditions give only one-sided inequalities: $\varphi$ and $\varphi^{-1}$ are sub-additive on $[0, \tfrac12]$. Sub-additivity of $\varphi^{-1}$ gives super-additivity of $\varphi$ only where $\varphi(p) + \varphi(\varepsilon) \le \tfrac12$. The symmetry $\varphi(\tfrac12) = \tfrac12$, which comes from source preference, is what closes the gap. Regularity is used twice: it brings Theorem 1 into play, and it guarantees that the region's upper bound lies above probability $\tfrac12$.

Formalization scope

The Lean development works in the sub-namespace SourceTheory.EqualSources, with one definition module holding the whole model:

• Assumption1 bundles Structural Assumption 1.
• IsSource is a subalgebra on which $W$ is convex ranged.
• IsUniformWith and IsSourceFunction encode uniformity and (5).
• IsPreferredTo, IsMoreInsensitive and IsRegularRegion encode Definition 2, Definition 4 and regularity.

Conventions committed to:

• events form an algebra $\mathcal E$, which the paper allows in its endnote 1;
• convex rangedness is imposed on $\mathcal E$ and on each named source, since the trivial algebra is never convex ranged;
• event preference is $W$-order;
• probability measures are finitely additive;
• twofold partitions are $(A_1, A_1^c)$, and partitions may have empty cells;
• a "transformation" is a continuous probability weighting function;
• the pmatcher is a binder with $w_{\mathcal A} = w_{\mathcal C} \circ \varphi$ on $[0,1]$, and its inverse is a binder with two-sided inverse laws, never Function.invFun;
• the region in Theorem 4 is read as regular for both sources, and "$w_{\mathcal A} = w_{\mathcal C}$" as a single function that is the source function of both.

The goal deliberately has no Assumption 2: the paper says it is implied by the other conditions, and adding it would weaken the theorem. Neither regularity hypothesis may be dropped either. Without regularity, a degenerate region such as $[S, \emptyset]$ makes the insensitivity conditions nearly empty, and the left-hand side holds for sources that are not uniform.

A complete development needs:

• finitely additive probabilities on algebras;
• a range lemma (convex rangedness makes $P_{\mathcal S}$ onto $[0,1]$);
• the Krantz et al. representation of qualitative probabilities;
• an interval version of the Cauchy functional equation.

The last two are reusable beyond this mission. Contributions to any milestone, and to the shared model layer, are welcome.

Selected references

• A. Baillon, H. Bleichrodt, C. Li, P. P. Wakker, Source Theory: A Tractable and Positive Ambiguity Theory, Management Science 71(10):8767–8782, 2025. https://doi.org/10.1287/mnsc.2023.03307
• D. H. Krantz, R. D. Luce, P. Suppes, A. Tversky, Foundations of Measurement, Vol. I, Academic Press, 1971.
• D. Ellsberg, Risk, Ambiguity, and the Savage Axioms, Quarterly Journal of Economics 75(4):643–669, 1961. https://doi.org/10.2307/1884324
• L. J. Savage, The Foundations of Statistics, Wiley, 1954.

Motivation

Decision makers facing uncertainty do not treat all events alike. Beyond liking or disliking ambiguity (the Ellsberg paradox, the home bias, the competence effect), people show insensitivity: a lack of discriminatory power that makes them overweight unlikely and underweight likely events, more so when they understand the uncertainty less. For risk this is the empirically prevalent inverse-S shape of probability weighting; for uncertainty it is linked to ambiguity perception and cognitive ability. Trautmann and van de Kuilen (2015) and many empirical studies stress its importance, yet most theoretical work on ambiguity models only the preference component.

Baillon, Bleichrodt, Li and Wakker (Management Science 71(10), 2025) propose source theory: within each source of uncertainty (a family of events generated by one mechanism, such as a stock index or an urn) the agent is probabilistically sophisticated, and differences in attitude appear across sources. Their third main result, Theorem 3, characterises comparative insensitivity between two sources through a single function of probabilities, the pmatcher. This mission formalizes that theorem.

Setting

A state space $S$ carries an algebra $\mathcal E$ of events, and $\Gamma$ is a set of outcomes. An act is a finite-valued map $x : S \to \Gamma$ whose level sets are events; a preference $\succcurlyeq$ ranks acts. Structural Assumption 1 requires a utility $U$ on outcomes and a weighting function $W$ on events ($W(\emptyset)=0$, $W(S)=1$, monotone) such that binary acts are ranked by biseparable utility, $W(E)U(\gamma) + (1-W(E))U(\beta)$ for $\gamma \succcurlyeq \beta$, together with convex rangedness of $W$, strong monotonicity, cumulative dominance, an Archimedean axiom, and three outcomes of distinct utility. Events are ranked by $W$: $A \succcurlyeq B$ means $W(A) \ge W(B)$.

A source is a subalgebra $\mathcal A \subseteq \mathcal E$ on which $W$ is convex ranged. It is uniform if a finitely additive probability $P_{\mathcal A}$ on $\mathcal A$ (the a-neutral probability) satisfies stochastic dominance for acts from $\mathcal A$. Then $W = w_{\mathcal A} \circ P_{\mathcal A}$ on $\mathcal A$ for a continuous, strictly increasing source function $w_{\mathcal A} : [0,1] \to [0,1]$. Assumption 2 says that two sources $\mathcal C$ and $\mathcal A$ are uniform, with $P_{\mathcal C}, w_{\mathcal C}$ and $P_{\mathcal A}, w_{\mathcal A}$. The pmatcher from $\mathcal A$ to $\mathcal C$ is the transformation $\varphi$ with

$$w_{\mathcal A} = w_{\mathcal C} \circ \varphi, \qquad \varphi = w_{\mathcal C}^{-1} \circ w_{\mathcal A}.$$

More insensitivity (Definition 4): $\mathcal A$ is more insensitive than $\mathcal C$ with insensitivity region $[B, D]$ if, for all threefold partitions $(C_1,C_2,C_3)$ from $\mathcal C$ and $(A_1,A_2,A_3)$ from $\mathcal A$,

$$W(A_1) = W(C_1)\ \&\ W(A_3^c) = W(C_3^c) \le W(D) \implies W(A_2) \ge W(C_2),$$ $$W(B) \le W(A_1) = W(C_1)\ \&\ W(A_3^c) = W(C_3^c) \implies W(A_2^c) \le W(C_2^c).$$

A function $w$ on $[0,1]$ is insensitive with region $[b, d]$ if for all $p_1, p_2, p_3 \ge 0$ summing to 1, $w(p_2) \ge w(p_1+p_2) - w(p_1)$ whenever $p_1 + p_2 \le d$, and $1 - w(p_1+p_3) \ge w(p_1+p_2) - w(p_1)$ whenever $p_1 \ge b$.

Formalization targets

Goal: Theorem 3

Under Assumptions 1 and 2, for boundary events $B, D \in \mathcal A$:

$$\mathcal A \text{ is more insensitive than } \mathcal C \text{ with region } [B,D] \iff \exists\, \varphi \text{ insensitive with region } [P_{\mathcal A}(B), P_{\mathcal A}(D)],\ w_{\mathcal A} = w_{\mathcal C} \circ \varphi.$$

Milestones

1. The a-neutral probability of a uniform source takes every value in $[0,1]$ (proof of Observation 1).
2. The pmatcher exists, is continuous, strictly increasing and unique ((18)).
3. Observation 4: $\varphi(P_{\mathcal A}(A)) \gtreqless P_{\mathcal C}(C)$ iff $A \succ, \sim, \prec C$.
4. Threefold partitions match iff $\varphi(q_1) = p_1$ and $\varphi(q_1+q_2) = p_1+p_2$.
5. For matching partitions, $A_2 \succcurlyeq C_2$ iff $\varphi(q_2) \ge \varphi(q_1+q_2) - \varphi(q_1)$.
6. The boundary condition $A_3^c \preccurlyeq D$ means $q_1 + q_2 \le P_{\mathcal A}(D)$.
7. The dual case, (9) against (14), with $B \preccurlyeq A_1$ iff $P_{\mathcal A}(B) \le q_1$.

Significance

Theorem 3 shows that comparative insensitivity, a condition on preferences over events of two sources, is equivalent to a shape condition (sub-additivity bounded away from the extremes) on one real function. With $\mathcal C$ the risky source, $\varphi$ is the matching-probability function measured in experiments (Dimmock et al. 2016), so the theorem justifies reading inverse-S matching probabilities as ambiguity-generated insensitivity, and it identifies the probability interval on which the shape condition applies. Together with Theorem 2 (source preference iff a disliked pmatcher), it lets a single function capture both components of uncertainty attitudes.

The result is proved in the paper, in a short argument relying on a range property whose general finitely additive proof is in an online appendix. No part of the paper is formalized anywhere to our knowledge. A formal development fixes the model precisely (Assumption 1 has many components), checks the region correspondence, and provides a reusable layer of decision-theoretic definitions (acts, biseparable utility, sources, source functions) for the rest of the paper's results.

Difficulty

The pmatcher translates events into probabilities, but Definition 4 quantifies over partitions while (13)–(14) quantify over real triples. The direction from preferences to $\varphi$ needs every triple $(p_1,p_2,p_3)$ to be realised by a partition of $\mathcal A$ and a matching partition of $\mathcal C$, with nested events. This rests on convex rangedness and on the fact that a finitely additive a-neutral probability of a convex-ranged source takes every value in $[0,1]$, which is elementary only for countably additive measures. Matching must also respect the boundary condition in both sources at once, so the region $[B,D]$ has to be carried exactly to $[P_{\mathcal A}(B), P_{\mathcal A}(D)]$, not merely to some interval.

Formalization scope

Lean represents events as an algebra $\mathcal E$ of Set S (MeasureTheory.IsSetAlgebra), allowed by the paper's endnote 1; the paper's own case is all subsets. $W$, $U$, $P_{\mathcal A}$, $P_{\mathcal C}$ are real-valued; $W$ is total on Set S and every event in a statement is required to belong to $\mathcal E$ or to a named source. Structural Assumption 1 is one structure with a field per axiom; "W is convex ranged for every source" is read as convex rangedness on $\mathcal E$ and on each source a theorem names, since the trivial algebra is never convex ranged. Event preference is $W$-order. Probabilities are finitely additive. Partitions are ordered and may have empty cells. A "transformation" is read as a continuous probability weighting function, the properties (18) gives the pmatcher. The pmatcher is asserted to exist, never defined through an inverse function. The function region $[b,d]$ is not constrained to $0 \le b < d \le 1$, because $P_{\mathcal A}(B) \ge P_{\mathcal A}(D)$ can happen for $B, D \in \mathcal A$.

The goal is stated in the theorem's "Furthermore" form with both regions pinned. The bare equivalence with both regions existentially quantified would be trivialized: a function region with $b > 1$ and $d < 0$ satisfies (13)–(14) vacuously, which would reduce condition (ii) to the existence of a pmatcher.

A complete development needs the range lemma for finitely additive probabilities on convex-ranged algebras, the construction of nested events of prescribed probability, and the inverse of a continuous strictly increasing map of $[0,1]$ onto itself. The model layer is shared with the other missions of this paper series and is reusable for any result on biseparable preferences and sources of uncertainty. Proofs of the milestones and of the range lemma are welcome individually.

Selected references

• A. Baillon, H. Bleichrodt, C. Li, P. P. Wakker, Source Theory: A Tractable and Positive Ambiguity Theory, Management Science 71(10):8767–8782, 2025. https://doi.org/10.1287/mnsc.2023.03307
• S. G. Dimmock, R. Kouwenberg, P. P. Wakker, Ambiguity Attitudes in a Large Representative Sample, Management Science 62(5):1363–1380, 2016. https://doi.org/10.1287/mnsc.2015.2198
• S. T. Trautmann, G. van de Kuilen, Ambiguity Attitudes, in The Wiley Blackwell Handbook of Judgment and Decision Making, 2015. https://doi.org/10.1002/9781118468333.ch3
• I. Gilboa, Expected Utility with Purely Subjective Non-Additive Probabilities, Journal of Mathematical Economics 16(1):65–88, 1987. https://doi.org/10.1016/0304-4068(87)90022-X

Motivation

Decisions under uncertainty rarely come with known probabilities. Since Ellsberg's (1961) urn experiments it has been documented that people prefer betting on events whose likelihood they understand — a known urn, a familiar domestic stock, a domain they feel competent in — over events of an unfamiliar source of uncertainty, even when they judge the events equally likely. This phenomenon, ambiguity aversion, together with the competence effect and home bias, is central to behavioural economics, finance and decision analysis, and its measurement requires a way to compare attitudes across sources.

Baillon, Bleichrodt, Li and Wakker (Management Science 71(10), 2025) develop source theory, in which every source of uncertainty carries its own probability-weighting function, and comparisons between sources are carried by a single function, the pmatcher. Their Theorem 2 characterises when one source is preferred to another: exactly when the pmatcher between them is disliked. With risk as the reference source, the pmatcher is the matching-probability function measured in experiments (Dimmock, Kouwenberg and Wakker 2016, Theorem 3.1), so the theorem connects a preference axiom with an observable function.

Setting

$S$ is a state space and $\Gamma$ a set of outcomes. Events are the members of an algebra $\mathcal E$ of subsets of $S$. An act is a map $x : S \to \Gamma$ with finitely many values whose level sets are events; $\gamma E \beta$ is the bet paying $\gamma$ on $E$ and $\beta$ on $E^c$. A preference $\succcurlyeq$ over acts is represented by biseparable utility: a utility $U : \Gamma \to \mathbb R$ and a weighting function $W$ on events with $W(\emptyset) = 0$, $W(S) = 1$, $W$ monotone, such that bets $\gamma E\beta$ with $\gamma \succcurlyeq \beta$ are ranked by $W(E)U(\gamma) + (1 - W(E))U(\beta)$. Structural Assumption 1 adds three outcomes of distinct utility, convex rangedness of $W$ (between two nested events every intermediate weight is attained by an event in between), strong monotonicity, cumulative dominance and an Archimedean axiom. Events are compared by $W$: $A \succcurlyeq B$ means $W(A) \ge W(B)$.

A source is a subalgebra $\mathcal S \subseteq \mathcal E$ on which $W$ is convex ranged. It is uniform if some finitely additive probability measure $P_{\mathcal S}$ on $\mathcal S$ makes the agent respect first-order stochastic dominance for acts measurable with respect to $\mathcal S$. Then $W = w_{\mathcal S} \circ P_{\mathcal S}$ on $\mathcal S$ for a continuous, strictly increasing source function $w_{\mathcal S} : [0,1] \to [0,1]$ with $w_{\mathcal S}(0) = 0$, $w_{\mathcal S}(1) = 1$; $P_{\mathcal S}$ is the a-neutral probability. Assumption 2 says that two sources $\mathcal C$ and $\mathcal A$ are uniform, with $P_{\mathcal C}, P_{\mathcal A}, w_{\mathcal C}, w_{\mathcal A}$.

Source preference (Definition 2): $\mathcal C$ is preferred to $\mathcal A$ if for all $C_1 \in \mathcal C$ and $A_1 \in \mathcal A$,

$$W(A_1) = W(C_1) \implies W(A_1^c) \le W(C_1^c).$$

A function $w$ on $[0,1]$ is disliked if $w(p) \le 1 - w(1-p)$ for all $p \in [0,1]$. The pmatcher from $\mathcal A$ to $\mathcal C$ is $\varphi = w_{\mathcal C}^{-1} \circ w_{\mathcal A}$, so that $w_{\mathcal A} = w_{\mathcal C} \circ \varphi$.

Formalization targets

Goal: Theorem 2

Under Assumptions 1 and 2,

$$\mathcal C \text{ is preferred to } \mathcal A \iff \exists\ \text{a disliked transformation } \varphi \text{ with } w_{\mathcal A} = w_{\mathcal C} \circ \varphi \text{ on } [0,1].$$

Milestones

1. Range of the a-neutral probability (proof of Observation 1, p. 8779, with (5)): $P_{\mathcal A}$ takes every value in $[0,1]$.
2. Equation (18): the pmatcher exists, is a continuous strictly increasing transformation, and is unique among maps of $[0,1]$ into itself with $w_{\mathcal A} = w_{\mathcal C} \circ \varphi$.
3. Observation 4: $\varphi(P_{\mathcal A}(A)) = P_{\mathcal C}(C)$ iff $A \sim C$, with the strict versions.
4. The matching step of the proof of Theorem 2: for matching partitions, $\varphi(q_1) = p_1$, and $A_2 \preccurlyeq C_2$ iff $\varphi(q_2) \le 1 - \varphi(1 - q_2)$.
5. Lemma A.1: the definition of source preference is equivalent to its weak-premise form $W(A_1) \ge W(C_1) \Rightarrow W(A_2) \le W(C_2)$.

Significance

The theorem turns a qualitative axiom on preferences between bets into a single inequality on one real function. Ambiguity aversion (take $\mathcal C$ to be risk, Corollary 1 of the paper) becomes dislike of the matching-probability function, which can be estimated from choice data without specifying any parametric ambiguity model. The pmatcher also carries the companion insensitivity result (Theorem 3), so source preference and insensitivity are both read off the same function.

The result is proved in the paper, in one paragraph that relies on (18), Observation 4 and a range property of uniform sources whose general (finitely additive) proof is deferred to an online appendix. No part of source theory has been formalized before. A machine-checked proof makes explicit what the short argument uses: that convex rangedness forces the a-neutral probabilities to fill $[0,1]$, that the pmatcher is well defined from the source functions alone, and that the twofold partitions of the definition can be realised for every probability level.

Difficulty

Source preference speaks only about pairs of events, while dislike is a condition on every probability $p \in [0,1]$. Passing between them requires every probability level to be realised by events of both sources. The familiar route to such a range statement uses countable additivity or a measure-theoretic continuity argument, which is not available here: the a-neutral probabilities are only finitely additive, and the paper defers the general case to an online appendix. The range has to come from convex rangedness of $W$ and the properties of the source function. A second point is that the pmatcher $w_{\mathcal C}^{-1} \circ w_{\mathcal A}$ is only meaningful on $[0,1]$, so it cannot be handled as a total inverse function.

Formalization scope

All objects are in the namespace SourceTheory.PrefMatch, defined in one module Model.

• Events are an algebra 𝓔 : Set (Set S) (MeasureTheory.IsSetAlgebra), as the paper's endnote 1 permits. Preference is a relation pref on acts; W : Set S → ℝ and U : Γ → ℝ are total functions whose values off events are never used.
• Assumption1 bundles Structural Assumption 1: weak order, normalised monotone W, utility on constant acts, three outcomes, biseparable utility, convex rangedness on 𝓔, strong monotonicity, cumulative dominance with event preference read as W-order, and the Archimedean axiom.
• A source (IsSource) is a subalgebra of 𝓔 on which W is convex ranged; the paper's "W is convex ranged for every source" is read this way because the trivial algebra $\{\emptyset, S\}$ is never convex ranged.
• Probabilities on a source are finitely additive (IsProbOn); uniformity is stochastic dominance with that probability (IsUniformWith); source functions and transformations are continuous strictly increasing self-maps of $[0,1]$ fixing $0$ and $1$.
• Twofold partitions are $(A_1, A_1^c)$. "Transformation", undefined in the paper, is read as a continuous probability weighting function; since $w_{\mathcal C}$ is a bijection of $[0,1]$, every map of $[0,1]$ into itself with $w_{\mathcal A} = w_{\mathcal C} \circ \varphi$ is the pmatcher, so nothing is lost. The equality $w_{\mathcal A} = w_{\mathcal C} \circ \varphi$ is stated on $[0,1]$.
• Disliked is required for all $p \in [0,1]$, not only for probabilities attained by events; the pmatcher is quantified, never defined through Function.invFun, which would return junk off the range.

A formalization in which Assumption 2 or the source hypotheses were contradictory would make the goal vacuous; the statements use exactly the paper's assumptions, and a sanity file checks that the identity and $p \mapsto p^2$ are disliked transformations while $\sqrt{\cdot}$ is a transformation that is not.

Proofs of the milestones, and of a full model of Assumption 1 (for example expected utility with Lebesgue measure on the Borel sets of $[0,1)$), are welcome contributions; the model layer is shared verbatim with the other missions of this series.

Selected references

• A. Baillon, H. Bleichrodt, C. Li, P. P. Wakker, Source Theory: A Tractable and Positive Ambiguity Theory, Management Science 71(10):8767–8782, 2025. https://doi.org/10.1287/mnsc.2023.03307
• D. Ellsberg, Risk, Ambiguity, and the Savage Axioms, Quarterly Journal of Economics 75(4):643–669, 1961. https://doi.org/10.2307/1884324
• S. G. Dimmock, R. Kouwenberg, P. P. Wakker, Ambiguity Attitudes in a Large Representative Sample, Management Science 62(5):1363–1380, 2016. https://doi.org/10.1287/mnsc.2015.2198
• I. Gilboa, Expected Utility with Purely Subjective Non-Additive Probabilities, Journal of Mathematical Economics 16(1):65–88, 1987. https://doi.org/10.1016/0304-4068(87)90022-X

Motivation

In a principal–agent problem with moral hazard, a principal (an employer) pays an agent whose effort she cannot observe; she sees only an output process whose drift the effort controls. Continuous-time versions of the problem, starting with Holmström–Milgrom (1987) and Sannikov (2008), are solved by turning the agent's continuation utility into a state variable and writing a Hamilton–Jacobi–Bellman (HJB) equation for the principal's value.

Most of this literature assumes two-sided commitment: the agent cannot leave. In labour markets the agent can quit whenever an outside offer beats his continuation utility, and the principal must then hire someone else. Zhang and Zhu (arXiv:2208.06473; Mathematics of Operations Research, 2025) study this one-sided commitment: the principal is committed to the contract, the agent is free to quit at a stopping time of his choice, and after each quitting the principal pays a cost and hires a new agent, possibly of another type. The principal's value then depends on every future hire, and the paper characterises it by a coupled system of HJB equations.

Setting

Fix a horizon $T>0$ and a payment cap $C_0>0$. A standard Brownian motion $B$ on $(\Omega,\mathcal F,\mathbb P)$ is the output. Agents have types $\theta\in\Theta$. An agent of type $\theta$ receiving a payment rate $\eta\le C_0$ and exerting effort $\alpha$ has running utility $f(\theta;s,\eta)$ and running cost $h(\theta;s,\alpha)$; $f$ is increasing and concave in $\eta$, $h$ is convex in $\alpha$ (Assumption 2.2). Effort shifts the drift of $B$ through the Girsanov measure $\mathbb P^\alpha$ (weak formulation). The agent's optimal effort against a sensitivity process $Z$ is $\alpha=I^h(\theta;\cdot,Z)$, the inverse of $\partial_\alpha h$, and $\mathbb E^{\theta,Z}$ denotes expectation under the corresponding measure.

A contract started at time $t$ is described in forward form by $(\eta,Z)$: the agent's continuation utility is

$$\mathcal X^{\theta;t,x,\eta,Z}_s=x-\int_t^s\big[f(\theta;r,\eta_r)+H(\theta;r,Z_r)\big]dr+\int_t^sZ_r\,dB_r,$$

with $H(\theta;s,z)=\sup_\alpha[\alpha z-h(\theta;s,\alpha)]$ and the constraint $\mathcal X_T=0$. The agent's utility is capped by the upper barrier $\overline L^\theta_t=\int_t^Tf(\theta;s,C_0)\,ds$. He quits at the first time $\mathcal X$ reaches the lower barrier $\underline L^\theta_t=R^\theta_t-c^\theta_t$, where $R^\theta$ is his market value and $c^\theta\ge1/\Lambda_0$ his quitting cost (Assumptions 2.7, 3.1). The relevant domain is

$$D_\theta=\{(t,x):0\le t<T,\ \underline L^\theta_t<x\le\overline L^\theta_t\}.$$

When the $i$-th agent quits at $\tau_i<T$, the principal pays $c^P_{\tau_i}$ and hires an agent of type $\zeta_{\tau_i}$ at utility $R^{\zeta_{\tau_i}}_{\tau_i}$ (the quitting sequence (5.8)). The principal's value is

$$u_\infty(\theta;t,x)=\sup_{(\eta,Z,\zeta)}\mathbb E^{\zeta,Z}\Big[\int_t^T\big[I^h(\zeta_s;s,Z_s)-\eta_s\big]ds-\sum_{i\ge1}c^P_{\tau_i}\mathbf 1_{\{\tau_i<T\}}\Big],$$

and the value of the best new hire at time $t$ is $\overline u_\infty(t)=\sup_\theta u_\infty(\theta;t,R^\theta_t)-c^P_t$.

Formalization targets

Goal: Theorem 6.3

The family $\{u_\infty(\theta;\cdot,\cdot)\}_{\theta\in\Theta}$ is the minimal continuous viscosity solution of

$$\partial_tu+\sup_{\eta\le C_0,\ z\in\mathbb R}\Big[\tfrac12|z|^2\partial_{xx}u-\big[f(\theta;t,\eta)+\tilde H(\theta;t,z)\big]\partial_xu+I^h(\theta;t,z)-\eta\Big]=0\quad\text{on }D_\theta,\ \theta\in\Theta,$$

with boundary conditions

$$u(\theta;t,\overline L^\theta_t)=-C_0(T-t),\qquad u(\theta;T-,x)=0,\qquad u(\theta;t,\underline L^\theta_t+)\ge\sup_{\theta'}u(\theta';t,R^{\theta'}_t)-c^P_t.$$

The last condition couples the equations for different types. The goal also asserts that the value sets in (6.1) are nonempty and bounded above, so that $u_\infty$ is a genuine real-valued function.

Milestones

1. Lemma 3.4: explicit contracts with $\int_t^T[C_0-\eta_s]ds\le\delta$ under which the agent never quits.
2. Lemma 2.5 (2.20): a priori estimates for admissible contracts.
3. Proposition 2.8 and Lemma 3.6: the self-enforcing value $V^P_0$ and the new-hire value $\overline u_0$ are uniformly continuous with modulus $C\sqrt\rho$.
4. Theorem 4.5: with at most one quitting, $u_1$ is the minimal continuous viscosity solution of the same equation with boundary datum $\overline u_0$.
5. Proposition 5.4: a non-recursive representation of $u_n$ (at most $n$ quittings).
6. Proposition 6.1: $\mathbb P^{\zeta,Z}(\tau_n<T)\le C/n$, and $|u_n-u_\infty|\le C/n$.
7. Proposition 6.2: monotonicity and uniform continuity of $u_\infty$, regularity of $\overline u_\infty$, and the boundary conditions.
8. (6.7): the dynamic programming principle for $u_\infty$.

Significance

The theorem identifies the principal's value under one-sided commitment as a PDE object, which makes it computable and comparable with other contracting regimes. Along the way the paper shows that the principal sees only finitely many quittings (Proposition 6.1) and that tolerating more quittings never lowers her value, so contracts that prevent quitting altogether (self-enforcing contracts) are in general suboptimal. The coupling through $\overline u_\infty$ turns the problem into an infinite system of HJB equations indexed by agent types, a structure that also appears in switching and re-hiring problems.

The result is proved in the paper; none of it is formalized. A formalization would add to the platform a continuous-time moral-hazard model in the weak formulation, hitting-time stopping driven by an Itô integral, a quitting sequence with random restarts and type switching, and a viscosity-solution notion for a fully nonlinear HJB equation on a time-dependent domain. The paper's own proof leaves several steps to the reader (the dynamic programming principle, the viscosity property, comparison for a truncated equation), so a complete development would also supply these.

Difficulty

The obvious route is "dynamic programming principle, then viscosity property, then comparison". Each step is harder here than in a textbook control problem. The control $z$ is unbounded, so the Hamiltonian can be $+\infty$ and the viscosity property must be derived without a finite Hamiltonian. The process is stopped at a hitting time of a moving barrier and restarted at a random level with a new type, so the dynamic programming principle must handle restarts. Minimality cannot come from a standard comparison principle, because the boundary datum at $\underline L^\theta$ depends on the competitor itself and no growth condition is imposed on competitors; the paper argues through approximation by $u_n$ and Theorem 4.5 instead.

Formalization scope

All objects are defined in the namespace DynPrincipalAgent.HJB. Process time is $\mathbb R_{\ge0}$; deterministic data are functions of real time. The Itô integral is the published Peng1990.SMP.IsItoIntegral, with a continuous version required wherever hitting times read paths. Controls started at $t$ are progressively measurable for the filtration $\mathbb F^t$ of $B_s-B_t$. Value functions are real suprema of value sets that record an expectation only when it is genuine (integrable payoffs, almost surely integrable drifts and running rewards, summable quitting costs); these conditions hold for every admissible control.

Pinned readings, all disclosed in the items: viscosity solutions are the standard Crandall–Ishii–Lions notion with $C^2$ test functions on $\mathbb R^2$, tested on the interior of $D_\theta$, with the supremum in the HJB operator never formed; the boundary condition at $\underline L^\theta$ requires a real right limit compared against every $u(\theta';t,R^{\theta'}_t)-c^P_t$; $\Theta$ carries a σ-algebra and $f$, $h$, $\partial_\alpha h$ are jointly measurable; Assumption 2.7 (ii) is read as $|R^\theta_s-R^\theta_{s'}|\le\rho(|s-s'|)$; a modulus of continuity is nondecreasing, vanishes at $0^+$ and satisfies $\rho(\delta)\ge\delta$; generic constants depend only on $(T,C_0,\Lambda_0,\Lambda_1)$ and are fixed before the model; $H$ and $\tilde H$ take the closed forms of (2.11)–(2.12). The agent's BSDE and reflected BSDE (Propositions 2.3, 3.2), §7's standard contracts and the economic interpretation of $R^\theta$, $c^\theta$, $c^P$ are out of scope.

A formalization in which a value function equals a junk value (an empty or unbounded real supremum, a Bochner integral of a non-integrable payoff, a hitting time of an empty set) or in which the viscosity notion is vacuous does not count: the goal states that the value sets are nonempty and bounded, and the definitions avoid junk by construction. Competitors in the minimality clause satisfy exactly the printed boundary conditions, with no added growth bound.

Reusable infrastructure: Girsanov measures for BMO drifts, forward utility processes, hitting times of continuous semimartingales, and viscosity solutions of HJB equations on non-cylindrical domains. Contributions on any milestone, and on general lemmas such as the dynamic programming principle for controlled diffusions stopped at hitting times, are welcome.

Selected references

• J. Zhang, Z. Zhu, A Dynamic Principal Agent Problem with One-sided Commitment, Mathematics of Operations Research, 2025. Preprint arXiv:2208.06473v3. https://arxiv.org/abs/2208.06473
• Y. Sannikov, A Continuous-Time Version of the Principal–Agent Problem, Review of Economic Studies 75 (2008). https://doi.org/10.1111/j.1467-937X.2008.00486.x
• B. Holmström, P. Milgrom, Aggregation and Linearity in the Provision of Intertemporal Incentives, Econometrica 55 (1987). https://doi.org/10.2307/1913238
• M. G. Crandall, H. Ishii, P.-L. Lions, User's guide to viscosity solutions of second order partial differential equations, Bull. AMS 27 (1992). https://doi.org/10.1090/S0273-0979-1992-00266-5

Motivation

Mean-variance (MV) preferences, $U_\theta(X)=\mathbb E[X]-\frac\theta2\mathrm{Var}(X)$, are the standard objective of portfolio selection since Markowitz. They are not monotone: an investor can prefer a terminal wealth $X$ to a wealth $X'\ge X$ that is larger in every state, because the extra upside raises the variance. Monotone mean-variance (MMV) preferences (Maccheroni, Marinacci, Rustichini and Taboga, 2009) repair this. They are the largest monotone preferences that agree with MV preferences on the domain of monotonicity $\mathcal G_\theta=\{f\in\mathcal L^2:f-\mathbb E[f]\le1/\theta\}$.

A natural question is when switching from MV to MMV changes the optimal investment. In continuous-time markets driven only by Brownian motions, the optimal strategies under the two preferences coincide (Trybuła and Zawisza, 2019, for a stochastic factor model; Strub and Li, 2020, for continuous semimartingale markets), and whether this persists with jumps was left open by Trybuła and Zawisza. Li, Liang and Pang study a market whose risky asset also jumps and whose coefficients depend on a stochastic factor. They show that the two problems agree if and only if a pathwise condition on the jumps, Assumption 1, holds.

Setting

On a probability space $(\Omega,\mathcal F,\mathbb P)$ live two independent Brownian motions $W^1,W^2$ and an independent Poisson random measure $N(\mathrm ds,\mathrm dp)$ with finite Lévy measure $\nu$ and compensated measure $\tilde N$. The filtration $\{\mathcal F_t\}$ is generated by $W^1,W^2,N$. A stochastic factor follows

$$\mathrm dZ_s=a(Z_s)\,\mathrm ds+b(Z_s)(\rho_W\,\mathrm dW^1_s+\bar\rho_W\,\mathrm dW^2_s),\qquad Z_t=z,$$

with $\rho_W^2+\bar\rho_W^2=1$. Investing the amount $\pi_s$ in the risky asset gives the (discounted) wealth

$$\mathrm dX^\pi_s=\pi_s(\mu(Z_s)-r)\,\mathrm ds+\pi_s\sigma(Z_s)\,\mathrm dW^1_s+\pi_s\int_{\mathbb R}\gamma(Z_s,p)\,\tilde N(\mathrm ds,\mathrm dp),\qquad X_t=x,$$

on $[t,T]$, with $\gamma>-1$. Write $\Sigma(z)=\sigma(z)^2+\int\gamma(z,p)^2\nu(\mathrm dp)$ and $\lambda(z)=(\mu(z)-r)^2/\Sigma(z)$.

The MMV preference is

$$V_\theta(X)=\inf_{\mathbb Q}\Big\{\mathbb E^{\mathbb Q}[X]+\frac1{2\theta}\Big(\mathbb E^{\mathbb P}\Big[\Big(\frac{\mathrm d\mathbb Q}{\mathrm d\mathbb P}\Big)^2\Big]-1\Big)\Big\}.$$

The infimum runs either over the Doléans-Dade measures $\mathcal Q^t$ or over all of $\mathcal Q_0=\{\mathbb Q\ll\mathbb P:\mathbb E[(\mathrm d\mathbb Q/\mathrm d\mathbb P)^2]<\infty\}$. A measure in $\mathcal Q^t$ has density $\mathcal E_T$, where $\mathcal E$ is the stochastic exponential of $\int\eta_1\mathrm dW^1+\int\eta_2\mathrm dW^2+\int\!\int\phi\,\mathrm d\tilde N$ with $\mathcal E_T\ge0$, $\mathbb E[\mathcal E_T]=1$ and $\mathcal E_T\in L^2$.

The optimal utilities from $(x,z,t)$ are suprema over the admissible strategies of the paper's Definitions 2 and 3: predictable $\pi$ whose wealth has $\mathbb E[\sup_s|X^\pi_s|^2]<\infty$, under $\mathbb P$ for MV and under every $\mathbb Q\in\mathcal Q^t$ for MMV. Both solutions are expressed through the solution $G=-e^F$ of the nonlinear parabolic PDE (20),

$$G_t+\alpha(z)G_z+\tfrac12b(z)^2G_{zz}-\beta(z)b(z)^2\frac{G_z^2}{G}+\lambda(z)G=0,\qquad G(z,T)=-1.$$

Through $\zeta(z,s)=-(\mu(z)-r-\sigma(z)b(z)\rho_WG_z/G)/\Sigma(z)$ it also enters Assumption 1. Let $\tau$ be the first jump time after $t$ at which $\zeta(Z_s,s)\gamma(Z_s,\Delta L_s)=-1$. Assumption 1 requires $\zeta\gamma\ge-1$ at every jump in $(t,T]$ up to time $\tau$.

Formalization targets

Goal: Theorem 9

$$\sup_{\pi\in\mathcal B_{x,z,t}}U_\theta(X^\pi_T)=\sup_{\pi\in\mathcal A_{x,1/(2\theta),z,t}}V_\theta(X^\pi_T)\iff\text{Assumption 1 holds at }(z,t).$$

The same holds when $V_\theta$ ranges over $\mathcal Q_0$ instead of $\mathcal Q^t$.

Milestones

1. Theorem 3 links the market player's density process to the wealth: $2Y_sG(Z_s,s)=X^{\pi^*}_s-x+2yG(z,t)$.
2. Theorem 4 solves the MMV problem: the value is $V(x,y,z,t)=-x+G(z,t)y$, with an explicit saddle point.
3. Theorem 6 solves the auxiliary quadratic problem: $U_D(x,z,t)=-(x-D)^2/G(z,t)$.
4. Theorem 7 gives the Lagrange multiplier and the optimal target.
5. (39) gives the optimal MV strategy.
6. The moment identities $\mathbb E[R_T]=\mathbb E[R_T^2]=H(z,t)=-1/G(z,t)$.
7. Theorem 8: under Assumption 1 the optimal strategies coincide.
8. Lemma 4: the optimal MV wealth lies in $\mathcal G_\theta$ if and only if Assumption 1 holds.
9. (44)–(45): the mean and variance of the optimal wealth.

Significance

The result separates the two preferences by an observable property of the market. The Brownian theory gives agreement for free. With jumps the MV-optimal wealth can leave $\mathcal G_\theta$, and that happens exactly when a jump of size $\zeta\gamma<-1$ can occur before the first jump with $\zeta\gamma=-1$. In that case MMV and MV investors hold different portfolios. The paper's §5.4 examines in market data whether Assumption 1 is reasonable. The explicit closed forms (the value $-x+G(z,t)y$, the variance $-(G(z,t)+1)/\theta^2$ of the optimal wealth, the efficient frontier) are what applied work uses.

The result is proved on paper, in an arXiv preprint later published in Mathematics of Operations Research (2025). None of it is machine-checked. A formal proof would check the verification arguments for a stochastic differential game with jumps, a Feynman–Kac representation with a jump density, and the comparison with Maccheroni et al.'s monotone hull. The paper's own proofs are brief at several of these steps. The underlying infrastructure (Itô calculus with Poisson jumps, Doléans-Dade exponentials, verification theorems) would be reusable for most of continuous-time portfolio theory.

Difficulty

The obvious argument would show $U_\theta=V_\theta$ along the optimal wealth and conclude. Lemma 4 shows this argument breaks: the optimal MV wealth need not lie in $\mathcal G_\theta$. Remark 7 also notes that membership in $\mathcal G_\theta$ alone does not identify the optimal values; both optimal strategies must be found and compared.

Finding them needs a verification theorem for a two-player stochastic differential game with jumps (Theorems 1 and 4). That in turn needs Itô's formula for jump diffusions and martingale properties of Doléans-Dade exponentials that may vanish (Lemma 2, Mémin's criterion). Identifying the two strategies needs the moment identities $\mathbb E[R_T]=\mathbb E[R_T^2]=H$, which come from a Feynman–Kac argument with a jump-driven density (Lemma 3). The converse direction needs a stopping argument at the first "bad" jump. None of this exists in Mathlib, which has Brownian motion but no stochastic integral and no Poisson process.

Formalization scope

• Time is $[0,\infty)$; every process lives on $[t,T]$ with $t<T$, and $\int_t^s$ is a difference of integral processes whose integrands vanish before $t$.
• Brownian integrals are the $L^2$ Itô integrals of Peng1990.SMP.Stochastic. The admissible classes $\mathcal A$, $\mathcal B$, $\mathcal M^t$ therefore contain only strategies whose Brownian integrands are in $L^2$; all strategies used in the paper qualify.
• The Poisson random measure is JacodTodorov10.LLN.IsFPoisson with $\nu$ finite and $\nu(\{0\})=0$. The compensated integral is the pathwise sum over atoms minus the compensator integral.
• The filtration is the natural (uncompleted) filtration of $(W^1,W^2,N)$.
• Processes are adapted with càdlàg paths; $X_{s-}$ is Mathlib's Function.leftLim. Feedback strategies come with an existence claim, never as bare assumptions.
• All optimal values are infima/suprema in EReal over the full admissible classes. Measures in $\mathcal Q_0$ are probability measures.
• $\mathcal M^t$ is defined by the defining equation (5) of the stochastic exponential. The printed formula (4) has $\Delta X$ where $\Delta M$ is meant and is not used.
• Proposition 1 is not formalized: its hypotheses do not deliver a classical solution. $G$ is a hypothesis: $G=-e^F$ with $F$ bounded, $C^{2,1}$ with bounded derivatives, solving (20). The Conditions of Proposition 1 are kept as printed. $\Sigma,\lambda,\beta>0$ is a standing hypothesis (implicit on p. 12).
• Assumption 1 uses $\tau$ in $[0,\infty]$ ($\inf\emptyset=\infty$), and "a.s." holds simultaneously for all $s\in(t,T]$.
• Printed slips: (37) evaluates $G_z/G$ at $(Z_s,t)$; it is read at $(Z_s,s)$. Lemma 4's "Equation (1)" means (20)/(21).
• Divisions by $1-\mathbb E[R_T]$ and $\mathrm{Var}[R_T]$ carry the hypotheses $\mathbb E[R_T]\neq1$, $\mathrm{Var}[R_T]>0$.

A formalization that replaces either optimal utility by a closed form or by the utility of one fixed strategy is out of scope: it assumes Theorems 4 and 7 and empties the goal. So is one that removes the jumps, freezes the factor, or replaces Assumption 1 by a sufficient condition such as $\gamma\ge0$; each of these makes the "only if" vacuous or false. Contributions that build general infrastructure (an Itô formula for jump diffusions, Doléans-Dade exponentials, a Feynman–Kac theorem) are especially welcome.

Selected references

• B. Li, Z. Liang, L. Pang, Comparison Between Mean-Variance and Monotone Mean-Variance Preferences Under Jump Diffusion and Stochastic Factor Model, arXiv:2211.14473v2, 2023. https://arxiv.org/abs/2211.14473
• F. Maccheroni, M. Marinacci, A. Rustichini, M. Taboga, Portfolio selection with monotone mean-variance preferences, Mathematical Finance 19(3):487–521, 2009. https://doi.org/10.1111/j.1467-9965.2009.00376.x
• J. Trybuła, D. Zawisza, Continuous-time portfolio choice under monotone mean-variance preferences—stochastic factor case, Mathematics of Operations Research 44(3):966–987, 2019 (cited as [Trybuła and Zawisza 2019] in arXiv:2211.14473v2).
• M. S. Strub, D. Li, A note on monotone mean–variance preferences for continuous processes, Operations Research Letters 48(4):397–400, 2020 (cited as [Strub and Li 2020] in arXiv:2211.14473v2).
• P. Protter, Stochastic Integration and Differential Equations, 2nd ed., Springer, 2005, ISBN 978-3-662-10061-5.

Why scoring rules for multivariate distributions

A probabilistic forecast issues a whole distribution $P_X$ for an uncertain quantity $Y\in\mathbb R^d$ rather than a single number: wind and wave heights at several sites, demand for several products, the joint returns of several assets. Forecasts of this kind are compared and estimated with a scoring rule $S(P_X,y)$, a number assigned to the forecast once the realization $y$ is observed. A scoring rule is proper if a forecaster who knows the true distribution $P_Y$ minimizes the expected score by reporting it, and strictly proper if $P_Y$ is the only minimizer (Gneiting and Raftery 2007). Properness is what makes a score usable for model ranking and for M-estimation: an improper score rewards systematic misreporting.

For univariate distributions the continuous ranked probability score (CRPS) and the quadratic score are standard. In several dimensions the choices are thinner: the quadratic score needs a density and is sensitive to its spikes, and the energy score and the multivariate CRPS (MCRPS) were treated as separate constructions. Meng, Taylor, Ben Taieb and Li (arXiv:2002.09578v6, Operations Research, 2025) give one family, the L² scoring rules, which contains the quadratic score, the CRPS and the MCRPS as special cases and produces new ones, such as a score based on lower partial moments. Their Theorem 1 says these rules are proper. This mission formalizes that theorem.

Setting

Work on $\mathbb R^d$ with Lebesgue measure $\mathcal L^d$ and the componentwise order. A distribution is a probability measure $P$ on $\mathbb R^d$; the paper writes it through a generalized density $f_P$ (a PDF, a PMF or a mixture), and every integral $\int g(s)f_P(s)\,ds$ below is $\int g\,dP$. The forecasts range over a class $\mathcal V^d$ of distributions.

Fix a kernel $w:\mathbb R^d\to\mathbb R$ and a weight $h\ge0$ that is integrable. The smoothed density of $P$ is the convolution

$$(f_P*w)(z)=\int_{\mathbb R^d} w(z-s)\,dP(s).$$

For the Heaviside kernel $u(z)=\mathbb 1\{z\ge0\}$ it is the CDF $F_P(z)=P\{s\le z\}$.

The two L² scoring rules are, for a forecast $P_X$ and a realization $y$,

$$S(P_X,y;w,h)=\int_{\mathbb R^d}\big((f_X*w)(z)-w(z-y)\big)^2h(z)\,dz \qquad (2)$$ $$S'(P_X,y;w,h)=\int_{\mathbb R^d}(f_X*w)^2(z)h(z)\,dz-2\int_{\mathbb R^d}(f_X*w)(z)\,w(z-y)\,h(z)\,dz. \qquad (3)$$

The realization $y$ is treated as a point mass, whose convolution with $w$ is $w(\cdot-y)$. The divergence of a score is $\mathbb E_{P_Y}[S(P_X,\bullet)]-\mathbb E_{P_Y}[S(P_Y,\bullet)]$, and the paper's candidate is the weighted L² distance between smoothed densities,

$$\int_{\mathbb R^d}\big((f_X*w)(z)-(f_Y*w)(z)\big)^2h(z)\,dz. \qquad (1)$$

Assumption 1 (p. 32) collects the integrability under which all these integrals are finite.

Formalization targets

Goal: Theorem 1 (p. 8)

Under Assumption 1, for all $P_X,P_Y\in\mathcal V^d$,

$$\mathbb E_{P_Y}[S(P_X,\bullet)]-\mathbb E_{P_Y}[S(P_Y,\bullet)]=\mathbb E_{P_Y}[S'(P_X,\bullet)]-\mathbb E_{P_Y}[S'(P_Y,\bullet)]=\int\big(f_X*w-f_Y*w\big)^2h\,dz\ \ge 0,$$

so both rules are proper. If in addition $h\ne0$ $\mathcal L^d$-a.e. and $f_Y*w$ determines $P_Y$ within $\mathcal V^d$, both are strictly proper. The goal fixes no kernel and no weight: it holds for every pair $(w,h)$ meeting the assumption.

Milestones

1. The relation between (2) and (3): $S=S'+\int w^2(z-y)h(z)\,dz$, a term that does not depend on the forecast (p. 8).
2. The Fubini step of the proof: $\int\!\int g(z)w(z-s)h(z)\,dz\,dP_Y(s)=\int g\,(f_Y*w)\,h\,dz$ (p. 32).
3. The divergence display: the divergence of (2) equals (1) and is nonnegative (p. 32).
4. The strict step: a vanishing divergence with $h\ne0$ a.e. forces $f_X*w=f_Y*w$ a.e. (p. 32).
5. MCRPS (5) and MCRPS′ (6) are strictly proper for all distributions when $h\ne0$ a.e. (p. 11).
6. Lower partial moments of any order $k$ determine the distribution (Appendix, p. 34).

Significance

Theorem 1 is the paper's justification for its whole family of scores. With $w=u$ it shows that the MCRPS is proper; with $w$ the kernel of lower partial moments it shows that a new LPM score is proper; and in Section 4 of the paper the same smoothed densities $f_Y*w$ define the level sets whose scoring functions are the subject of the companion mission (Mission II of this series). Strict properness reduces to one question about the kernel: whether $f_Y*w$ determines $P_Y$. Milestones 5 and 6 answer it for the CDF and for lower partial moments.

The result is proved in the paper (appendix, pp. 32 and 34). To our knowledge none of it is formalized: Mathlib has no scoring rules, and the platform has no proper scoring rule for distributions, no multivariate CRPS and no lower partial moment. The formalization adds the integrability bookkeeping the paper leaves implicit, a machine-checked uniqueness theorem for the multivariate CDF (Mathlib's ext_of_Iic covers linear orders only, i.e. $d=1$), and the same for lower partial moments.

Difficulty

The algebraic core of Theorem 1 is the expansion of a square, and the obvious argument is the paper's. The cost lies elsewhere. Every expectation is an iterated integral of a function of $(s,z)$, and exchanging the order (Fubini) and splitting an integral of a difference require the integrability that Assumption 1 states only as "then (2) is well-defined and finite". The proof also uses $\int dP_Y=1$ when it integrates the $y$-free terms against $P_Y$.

For the companions the obstacle is measure-theoretic. An a.e. equality of multivariate CDFs must first be upgraded to equality everywhere, by right-continuity in each coordinate, and then measures that agree on lower orthants must be shown equal, a π-system argument in $\mathbb R^d$. For lower partial moments the paper differentiates $k$ times under the integral; a rigorous version has to control the finiteness of the lower-order moments.

Formalization scope

• $\mathbb R^d$ is Fin d → ℝ with its product Lebesgue measure volume and the Pi order, so $y\le z$ is componentwise and lower orthants are Set.Iic z. $d$ is any natural number; at $d=0$ the strict clauses are vacuous, as in the paper.
• Distributions are measures with IsProbabilityMeasure; the class $\mathcal V^d$ is a set of such measures. Its convexity (§2) is never used and is not imposed.
• Standing assumptions. The kernel $w$ is a measurable function. The paper also allows a local Borel measure, so that $w=\delta_0$ gives the quadratic score (4); that case is not covered. $h$ is measurable, nonnegative and integrable, not normalized to a density.
• Assumption 1 made explicit. Its clauses (b) and (c) are formalized as integrability hypotheses, each labelled with its clause: $(f_Y*w)^2h$ and $w(\cdot-y)^2h$ integrable; $(s,z)\mapsto w(z-s)^2h(z)$ integrable for $P_Y\otimes\mathcal L^d$; $(f_X*w)\,w(\cdot-y)\,h$ integrable; and $(s,z)\mapsto(f_X*w)(z)\,w(z-s)\,h(z)$ integrable for $P_Y\otimes\mathcal L^d$. Clause (a) adds that $f_Y*w$ is well defined.
• "$f_X*w=f_Y*w$" is an $\mathcal L^d$-a.e. equality. "$f_Y*w$ uniquely characterizes any $P_Y\in\mathcal V^d$" is a property of the whole class $\mathcal V^d$, not of the pair at hand. "$h$ nonzero $\mathcal L^d$-a.e." is used with the paper's quantifier. The theorem's printed "$f_{\mathbf y}*w$" is read as $f_Y*w$.
• Lower partial moments are defined from the explicit kernel printed in (7), $\prod_j (z_j-s_j)^k\mathbb 1\{z_j\ge s_j\}/k!$, for $k\in\mathbb N$, not as a convolution power of $u$. Milestone 6 states equality of the LPMs implying $P_X=P_Y$, the claim of its opening sentence.
• Ruling out trivial readings. A Bochner integral of a non-integrable function is $0$ in Lean, so every expectation in every statement carries the integrability that makes it the paper's integral. Without it, properness could hold because both sides are $0$. The characterization hypothesis is never assumed for the pair $(P_X,P_Y)$ alone.
• Needed infrastructure: product-measure Fubini (integral_integral_swap), integrability of products and squares, and uniqueness of measures from a generating π-system. A general lemma "a multivariate CDF determines its measure" would be reusable well beyond this mission and is welcome as a separate contribution.

Selected references

• X. Meng, J. W. Taylor, S. Ben Taieb, S. Li, Scores for Multivariate Distributions and Level Sets, Operations Research, 2025; preprint arXiv:2002.09578v6, 2023. https://arxiv.org/abs/2002.09578v6
• T. Gneiting, A. E. Raftery, Strictly Proper Scoring Rules, Prediction, and Estimation, Journal of the American Statistical Association 102(477), 359–378, 2007. https://doi.org/10.1198/016214506000000437
• T. Gneiting, R. Ranjan, Comparing Density Forecasts Using Threshold- and Quantile-Weighted Scoring Rules, Journal of Business & Economic Statistics 29(3), 411–422, 2011. https://doi.org/10.1198/jbes.2010.08110