All missions

Motivation

Probability distortion models the empirical tendency, documented by Kahneman and Tversky and central to rank-dependent utility and cumulative prospect theory, to overweight small probabilities and underweight large ones. A distortion function $\varphi$ is applied to the survival function of a payoff, and the distorted expectation

$$\mathcal E[\xi]=\int_0^\infty \varphi\bigl(\mathbb P(\xi\ge x)\bigr)\,dx$$

replaces the ordinary expectation $\mathbb E[\xi]=\int_0^\infty\mathbb P(\xi\ge x)\,dx$. This nonlinear expectation is neither sub- nor super-additive, so it lies outside Peng's framework of sublinear expectations.

The difficulty appears in dynamic problems. The naive conditional version $\mathcal E_t[\xi]=\int_0^\infty\varphi(\mathbb P(\xi>x\mid\mathcal F_t))\,dx$ violates the tower property $\mathcal E_s[\mathcal E_t[\xi]]=\mathcal E_s[\xi]$ already on a two-period binomial tree (Example 2.7 of the paper). This is the time-inconsistency that drives the literature on precommitment and equilibrium strategies under distortion (Ekeland–Lazrak, Björk–Murgoci, Hu–Jin–Zhou). Ma, Wong and Zhang (arXiv:1809.08262, Math. Oper. Res. 2021) follow the dynamic-utility idea of Karnam–Ma–Zhang: let the distortion depend on the current time, the horizon and the current state, and ask whether it can be chosen so that the tower property holds while the time-$0$ expectation is the prescribed distorted one. This mission formalizes their discrete-time answer.

Setting

Distortion function. A map $\varphi:[0,1]\to[0,1]$ that is continuous, strictly increasing, with $\varphi(0)=0$, $\varphi(1)=1$. The class $\mathcal I$ consists of the functions $g:\mathbb R\to[0,\infty)$ that are bounded, continuous and (non-strictly) increasing.

The tree. Fix $N$ and times $0=t_0<\dots<t_N$. At time $t_i$ the process $X$ takes values $x_{i,0}<\dots<x_{i,i}$; from $x_{i,j}$ it moves to $x_{i+1,j+1}$ with probability $p^+_{i,j}$ and to $x_{i+1,j}$ with probability $p^-_{i,j}=1-p^+_{i,j}$, where $0<p^+_{i,j}<1$. The filtration is the one generated by $X$. Distortion functions $\varphi_{t_1},\dots,\varphi_{t_N}$ are given, describing the time-$0$ perception of events at each future time, and $\varphi_{t_0}(p)=p$.

Survival probabilities and the distorted probability. $G_{i,j}=\mathbb P(X_{t_i}\ge x_{i,j})$, $G_{i,i+1}=0$, and

$$q^+_{i,j}=\frac{\varphi_{t_{i+1}}(G_{i+1,j+1})-\varphi_{t_i}(G_{i,j+1})}{\varphi_{t_i}(G_{i,j})-\varphi_{t_i}(G_{i,j+1})},\qquad 0\le j\le i\le N-1 .$$

$\mathbb Q$ is the probability under which $X$ moves up from $x_{i,j}$ with probability $q^+_{i,j}$. The standing condition (3.14) is $\varphi_{t_i}(G_{i,j+1})<\varphi_{t_{i+1}}(G_{i+1,j+1})<\varphi_{t_i}(G_{i,j})$.

Dynamic distortion function. A map $\Phi(s,t,x;p)$, for $s<t$ in the time set, $x\in\mathbb R$, $p\in[0,1]$, that is jointly Lebesgue measurable in $(x,p)$ and a distortion function in $p$. Its conditional nonlinear expectation is

$$\mathcal E_{s,t}[\xi]=\int_0^\infty\Phi\bigl(s,t,X_s;\mathbb P(\xi\ge x\mid\mathcal F_s)\bigr)\,dx ,$$

and $\Phi$ is time-consistent if $\mathcal E_{r,t}[g(X_t)]=\mathcal E_{r,s}[\mathcal E_{s,t}[g(X_t)]]$ for all $r<s<t$ and $g\in\mathcal I$.

Formalization targets

Goal: Theorem 3.4

Under (3.14) there exists a time-consistent dynamic distortion function $\Phi$ with $\Phi(t_0,t_n,x_{0,0};\cdot)=\varphi_{t_n}$ for $n=1,\dots,N$ such that, for all $0\le i<n\le N$, $0\le j\le i$, $0\le k\le n$,

$$\Phi\bigl(t_i,t_n,x_{i,j};\mathbb P\{X_{t_n}\ge x_{n,k}\mid X_{t_i}=x_{i,j}\}\bigr)=\mathbb Q\{X_{t_n}\ge x_{n,k}\mid X_{t_i}=x_{i,j}\}, \tag{3.17}$$

and $\mathcal E_{t_i,t_n}[g(X_{t_n})]=\mathbb E^{\mathbb Q}[g(X_{t_n})\mid\sigma(X_{t_i})]$ for $g\in\mathcal I$ (3.12). Conversely, every time-consistent dynamic distortion function with the same initial condition satisfies (3.17) and (3.12): it is unique at the conditional survival probabilities. The goal is the discrete main result of the paper; its continuous-time counterpart, Theorem 4.7, is not part of this mission.

Milestones

1. Proposition 2.5(i): $\mathcal E$ of a finitely valued variable as a finite sum, (2.2)–(2.3).
2. Condition (3.14) gives $0<q^+_{i,j}<1$.
3. Lemma 3.3: the backward recursion $u_i=q^+u_{i+1}(\cdot^+)+q^-u_{i+1}(\cdot^-)$ is increasing and equals $\mathbb E^{\mathbb Q}[g(X_{t_n})\mid\mathcal F_{t_i}]$.
4. (3.18): $\varphi_{t_n}(\mathbb P\{X_{t_n}\ge x_{n,k}\})=\mathbb Q\{X_{t_n}\ge x_{n,k}\}$.
5. A distortion function carrying the conditional survival probabilities under $\mathbb P$ to those under $\mathbb Q$ at each node.
6. (3.17) implies (3.12).
7. (3.12) implies time-consistency.
8. One-step uniqueness: $\Phi(t_i,t_{i+1},x_{i,k};p^+_{i,k})=q^+_{i,k}$ for any admissible $\Phi$.
9. Any admissible $\Phi$ has $\mathcal E_{t_i,t_n}[g(X_{t_n})]=\mathbb E^{\mathbb Q}[g(X_{t_n})\mid\mathcal F_{t_i}]$.

Significance

The theorem gives a conditional expectation under probability distortion that equals the distorted expectation at time $0$, obeys the tower property, and is linear on $\{g(X_t):g\in\mathcal I\}$: it is the ordinary conditional expectation under the explicit measure $\mathbb Q$. Dynamic programming arguments under distortion can therefore be run as linear backward recursions under $\mathbb Q$, which is the starting point of the paper's continuous-time PDE characterization. Uniqueness shows that no other time-consistent choice with the same time-$0$ perception exists on the tree, so $\mathbb Q$ is forced, not chosen.

The result is proved in the paper; no machine-checked proof exists. A formal proof would supply the details the paper calls "obvious" or "straightforward" (the Markov computation of $\mathbb E^{\mathbb Q}[\cdot\mid\mathcal F_{t_i}]$, the interpolation, and the separation of node weights by functions in $\mathcal I$) and a reusable layer for distorted expectations of finitely valued random variables.

Difficulty

The obvious construction, a fixed distortion $\varphi$ applied to conditional probabilities, is time-inconsistent, so the dynamic distortion must be built from both the $\mathbb P$- and the $\mathbb Q$-survival functions. Existence needs three facts to fit together: $\mathbb Q$ reproduces the distorted survival function at every time (3.18), the conditional survival probabilities under $\mathbb P$ and $\mathbb Q$ have the same order and the same zeros and ones at each node, and the inner expectation $\mathcal E_{t_m,t_n}[g(X_{t_n})]$ is again an increasing function of $X_{t_m}$, so that time-consistency, which is only required on $\mathcal I$, applies to it. Uniqueness has to extract the one-step distortions $\Phi(t_i,t_{i+1},x_{i,k};p^+_{i,k})$ from the tower property tested on all of $\mathcal I$, which requires functions in $\mathcal I$ that separate the weights of consecutive nodes. The recombining structure and the monotonicity of the nodes are essential: Example 3.2 of the paper shows that on a tree with crossing edges no time-consistent $\Phi$ exists in general.

Formalization scope

The tree is realized on the canonical path space Fin N → Bool (true is an up-move); $X_{t_i}(\omega)=x_{i,\ell}$ where $\ell$ is the number of up-moves before $i$, and a path has probability $\prod p^\pm$. Times are indices $0,\dots,N$. $\mathcal F_{t_i}$ is generated by the sets of paths that agree in the first $i$ moves, and conditioning on $\sigma(X_{t_i})$ at $\omega$ is conditioning on $\{X_{t_i}=X_{t_i}(\omega)\}$. Identities between random variables are stated at every path; every path has positive probability. The integrals (1.2) and (2.11) are Bochner integrals over $(0,\infty)$, finite for the bounded variables they are applied to. Lebesgue measurability in Definition 2.8 is null-measurability for the Lebesgue measure on $\mathbb R\times[0,1]$. The given family $\varphi$ is indexed by $1,\dots,N$, and $\varphi_{t_0}=\mathrm{id}$ is built in.

The uniqueness clause quantifies over all time-consistent dynamic distortion functions with the initial condition; it does not assume (3.17), so it is not tautological, and the existence clause asserts the existence of $\Phi$ without naming the interpolant. Proposition 2.5(i)'s formula (2.3) is stated for real-valued $\eta$, because the proof of Theorem 3.4 applies it to $X_{t_n}$, whose nodes may be negative.

A complete development needs finite sums over paths, the Markov property of the path weights, a layer-cake computation of the Bochner integral for step functions, and piecewise-linear interpolation of finitely many points. The distorted-expectation layer (Proposition 2.5(i)) is reusable for rank-dependent utility and distortion risk measures. Proofs of any milestone, and alternative routes to uniqueness, are welcome.

Selected references

• J. Ma, T.-K. L. Wong, J. Zhang, Time-consistent conditional expectation under probability distortion, Mathematics of Operations Research (2021); arXiv:1809.08262v5, 2020. https://arxiv.org/abs/1809.08262v5
• C. Karnam, J. Ma, J. Zhang, Dynamic approaches for some time-inconsistent optimization problems, The Annals of Applied Probability 27(6):3435–3477, 2017. https://doi.org/10.1214/17-AAP1273
• I. Ekeland, A. Lazrak, The golden rule when preferences are time inconsistent, Mathematics and Financial Economics 4(1):29–55, 2010. https://doi.org/10.1007/s11579-010-0034-x
• D. Kahneman, A. Tversky, Prospect theory: an analysis of decision under risk, Econometrica 47(2):263–292, 1979. https://doi.org/10.2307/1914185
• A. Tversky, D. Kahneman, Advances in prospect theory: cumulative representation of uncertainty, Journal of Risk and Uncertainty 5(4):297–323, 1992. https://doi.org/10.1007/BF00122574
• X. Y. Zhou, Mathematicalising behavioural finance, Proceedings of the International Congress of Mathematicians 2010, pp. 3185–3209, World Scientific, 2010.
• S. Peng, G-Brownian motion and dynamic risk measure under volatility uncertainty, arXiv:0711.2834, 2007. https://arxiv.org/abs/0711.2834

Motivation

Mean-field games (MFGs) approximate stochastic games with many identical, interchangeable players by a single representative player who interacts with the distribution of the population (Huang, Malhamé, Caines 2006; Lasry, Lions 2007). In applications such as online ad auctions the reward and the dynamics are not known in closed form, and the equilibrium has to be learned from a simulator. Guo, Hu, Xu and Zhang (arXiv:2003.06069v3) set up a general mean-field game (GMFG), in which reward and transition depend on the joint state-action distribution of the population, and give a learning algorithm with a convergence and sample-complexity guarantee. Its stabilizing devices, softmax smoothing and projection onto a finite net, have been taken up in later work on learning in MFGs, for example by Cui and Koeppl and by Anahtarcı et al. (cited on p.3 of the paper).

Setting

The state space $\mathcal S$ and the action space $\mathcal A$ are compact metric spaces with their Borel $\sigma$-fields; $\mathcal P(X)$ is the set of Borel probability measures on $X$. A population state-action law is $\mathcal L\in\mathcal P(\mathcal S\times\mathcal A)$, with state marginal $\mu$. A GMFG has a measurable transition law $P(\cdot\mid s,a,\mathcal L)\in\mathcal P(\mathcal S)$, a measurable mean reward $\bar r(s,a,\mathcal L)\in[0,R_{\max}]$, and a discount factor $\gamma\in(0,1)$.

A policy $\pi\in\Pi$ is a measurable map $\mathcal S\to\mathcal P(\mathcal A)$. For fixed $\mathcal L$, the value is $V(s,\pi,\mathcal L)=\mathbb E[\sum_{t\ge0}\gamma^t r(s_t,a_t,\mathcal L)\mid s_0=s]$ with $a_t\sim\pi(s_t)$ and $s_{t+1}\sim P(\cdot\mid s_t,a_t,\mathcal L)$. A stationary Nash equilibrium (Definition 1) is a pair $(\pi^\star,\mathcal L^\star)$ such that $\pi^\star$ maximizes $V(s,\cdot,\mathcal L^\star)$ at every state, and the state-action law of the player who starts from $\mu^\star$ and plays $\pi^\star$ equals $\mathcal L^\star$ at every time.

Distances between laws are measured by the Wasserstein distance $W_1$: the infimum of the expected transport cost over couplings. On $\mathcal S\times\mathcal A$ the cost is the $\ell_2$ product distance $\sqrt{d_{\mathcal S}^2+d_{\mathcal A}^2}$. Policies are compared by $D(\pi,\pi')=\sup_sW_1(\pi(s),\pi'(s))$.

The equilibrium is a fixed point of a composite map. $\Gamma_1(\mathcal L)$ selects one optimal policy against $\mathcal L$; $\Gamma_2(\pi,\mathcal L)$ is the state-action law after one step of play from $\mu$; and $\Gamma(\mathcal L)=\Gamma_2(\Gamma_1(\mathcal L),\mathcal L)$. Assumption 1 asks $D(\Gamma_1(\mathcal L),\Gamma_1(\mathcal L'))\le d_1W_1(\mathcal L,\mathcal L')$, and Assumption 2 asks $\Gamma_2$ to be $d_2$-Lipschitz in the policy and $d_3$-Lipschitz in the law.

For finite $\mathcal S,\mathcal A$, $Q^\star_{\mathcal L}$ is the optimal Q-function of the MDP with transition $P(\cdot\mid\cdot,\cdot,\mathcal L)$ and reward $\bar r(\cdot,\cdot,\mathcal L)$, and $\Gamma_1(\mathcal L)_s=\mathrm{argmax\text{-}e}(Q^\star_{\mathcal L}(s,\cdot))$, the uniform law on the maximizing actions. The algorithm GMF-V (Algorithm 2) starts from any $\mathcal L_0$. At step $k$ it obtains an estimate $\hat Q_k$ of $Q^\star_{\mathcal L_k}$ from a learner, plays $\pi_k(s)=f(\hat Q_k(s,\cdot))$ for a smoothed argmax $f\in\mathcal F_{c,c'}$ (Lipschitz with constant $c$, within $2n e^{-c'\delta}$ of argmax-e when the gap is $\delta$), and sets $\mathcal L_{k+1}=\mathrm{Proj}_{S_\epsilon}(\Gamma_2(\pi_k,\mathcal L_k))$. Here $S_\epsilon$ is a finite $\epsilon$-net in total variation whose points have action gap at least $\varphi(\epsilon)$.

Formalization targets

Goal: Theorem 2 (corrected)

Let $d=d_1d_2+d_3\in(0,1)$, $\epsilon_k=(k+1)^{-(1+\eta)}$, $\delta_k=\delta/K$, and

$$K=\Big\lceil2\max\big\{(\eta\epsilon/c)^{-1/\eta},\ \log_d\big(\epsilon/\max\{\operatorname{diam}(\mathcal S\times\mathcal A),c\}\big)+1\big\}\Big\rceil .$$

There is $C_0$, depending only on the model and $d_1,d_2,d_3$, such that if each estimate fails with probability $\mathbb P(\|\hat Q_k-Q^\star_{\mathcal L_k}\|_\infty>\epsilon_k)\le2\delta_k$, then

$$\mathbb P\big(W_1(\mathcal L_K,\mathcal L^\star)>C_0\epsilon\big)\le2\delta,$$

where $\mathcal L^\star=\Gamma(\mathcal L^\star)$. In the same item, the total sample count satisfies

$$\sum_{k<K}T(\epsilon_k,\delta_k)\le\sum_{i=1}^m2^{\alpha^{(i)}_2}C^{(i)}K^{2\alpha^{(i)}_1+1}(K/\delta)^{\alpha^{(i)}_3}\big(\log(K/\delta)\big)^{\alpha^{(i)}_2+\alpha^{(i)}_4}.$$

Milestones

1. Appendix A: $W_1$ and $D$ are finite metrics and $(\mathcal P(\mathcal S\times\mathcal A),W_1)$, $(\Pi,D)$ are complete.
2. Proof of Theorem 1: $(\Gamma_1(\mathcal L),\mathcal L)$ is a stationary NE iff $\mathcal L=\Gamma(\mathcal L)$.
3. (18): $W_1(\Gamma(\mathcal L_1),\Gamma(\mathcal L_2))\le(d_1d_2+d_3)W_1(\mathcal L_1,\mathcal L_2)$.
4. Theorem 1: for $d_1d_2+d_3<1$, exactly one $\mathcal L$ makes $(\Gamma_1(\mathcal L),\mathcal L)$ a stationary NE.
5. (39): on a finite set, $W_1\le\operatorname{diam}\cdot d_{TV}\le\frac{\operatorname{diam}\sqrt{|X|}}2\|\cdot\|_2$.
6. Lemma 6: $\mathrm{softmax}_h$ is $c$-Lipschitz.
7. Lemma 7: $\|\mathrm{softmax}_h(x)-\mathrm{argmax\text{-}e}(x)\|_2\le2ne^{-c'\delta}$.
8. §4.2: $\mathcal B_{c,c'}\subseteq\mathcal F_{c,c'}$.

Significance

Theorem 1 gives existence and uniqueness of the equilibrium selected by $\Gamma_1$ under a contraction condition. Theorem 2 says that any single-agent Q-learner with a polynomial sample guarantee becomes, after smoothing and projection, an algorithm that finds that equilibrium to accuracy $O(\epsilon)$ with high probability, at a polynomial total sample cost. The constant $C_0$ does not depend on $\epsilon$, $\delta$, $\eta$ or the temperatures. Lemma 2 and Corollary 1 of the paper instantiate the learner with Q-learning.

The results are proved in the paper, not formalized; no machine-checked proof of these statements or of the GMFG layer is known. Several printed statements are false as written and are corrected minimally here, each with a counterexample in the item's difference list. The equilibrium in Theorems 1 and 2 must be the one selected by $\Gamma_1$. $K_{\epsilon,\eta}$ must use $\operatorname{diam}(\mathcal S\times\mathcal A)$, because $\operatorname{diam}(\mathcal S)\operatorname{diam}(\mathcal A)$ vanishes with a single action. The bound (23) holds without its factor $1/(2\alpha_1+1)$ and for $\delta\le1$. The printed Bellman equation has its maximum outside the sum, and only the equation with the maximum inside has the optimal Q-function as its solution. The hypotheses of Lemmas 6 and 7 are also corrected: the first must be two-sided, and the second has the wrong inequality direction.

Difficulty

The obvious proof of Theorem 1 is "contraction plus Banach". It needs $(\mathcal P(\mathcal S\times\mathcal A),W_1)$ to be a complete metric space for the $\ell_2$ product cost on general compact metric spaces. That requires the gluing lemma for the triangle inequality and weak compactness for completeness, and Mathlib has neither for this $W_1$. For Theorem 2, the naive per-step bound fails at the first iterate: $\mathcal L_0$ is not in the net, so no action gap controls the smoothing error there. The geometric recursion must also be summed with the exponent $d^{K-1-k}$ and tail sums of $(k+1)^{-(1+\eta)}$. Finally, the union bound over $K$ iterations has to work with failure events that need not be measurable.

Formalization scope

$\mathcal P(X)$ is ProbabilityMeasure X with the Giry $\sigma$-algebra. $W_1$ is a real infimum over couplings with an explicit cost; the product coupling makes it genuine. The model stores the mean reward rather than the reward law. $V$ is a discounted sum over state laws built by kernel composition. $Q^\star$ is the solution of the Bellman optimality equation, which exists and is unique (proved in the verification file). The learner enters Theorem 2 only through the per-iteration failure hypothesis, for random estimates on any probability space; the failure event of the conclusion is bounded in outer measure. $\mathcal L^\star$ is quantified over fixed points of $\Gamma$, and $C_0$ precedes every algorithmic parameter. Requiring $\mathcal L_0$ to lie in the net would make the first step free, and the statement does not assume it.

A complete development needs the metric and completeness theory of $W_1$ on compact metric spaces, the softmax Lipschitz and approximation bounds, and the finite $W_1$–$d_{TV}$ comparison. The first is reusable well beyond this mission. Contributions of any milestone, and of alternative proofs of the smoothing lemmas, are welcome.

Selected references

• X. Guo, A. Hu, R. Xu, J. Zhang, A General Framework for Learning Mean-Field Games, arXiv:2003.06069v3, 2023 (Mathematics of Operations Research). https://arxiv.org/abs/2003.06069
• X. Guo, A. Hu, R. Xu, J. Zhang, Learning Mean-Field Games, NeurIPS 2019. https://arxiv.org/abs/1901.09585
• M. Huang, R. P. Malhamé, P. E. Caines, Large population stochastic dynamic games, Communications in Information and Systems, 2006. https://doi.org/10.4310/CIS.2006.v6.n3.a5
• J.-M. Lasry, P.-L. Lions, Mean field games, Japanese Journal of Mathematics, 2007. https://doi.org/10.1007/s11537-007-0657-8
• F. Bolley, Separability and completeness for the Wasserstein distance, Séminaire de Probabilités XLI, 2008. https://doi.org/10.1007/978-3-540-77913-1_17
• E. Even-Dar, Y. Mansour, Learning rates for Q-learning, JMLR, 2003. https://www.jmlr.org/papers/v5/evendar03a.html

Motivation

Scenario planning asks a decision maker to consider several possible futures side by side: a world in which a technology matures, one in which regulation tightens, one shaped by a dramatic event. Decision analysts who support such exercises want to run a Bayesian analysis inside each scenario, but the classical foundations of subjective expected utility (Savage; Anscombe–Aumann; DeGroot's qualitative-probability route) axiomatize a single "small world" whose events can be freely combined. In scenario work the worlds may be unrelated, their states and consequences different, and the beliefs and values attached to them held by different stakeholders.

Simon French, Axiomatising the Bayesian Paradigm in Parallel Small Worlds (accepted manuscript of the Operations Research article, doi:10.1287/opre.2019.1896), gives an axiom system for parallel small worlds. Its one shared ingredient is a reference experiment, a uniform randomiser such as a probability wheel. Every likelihood judgement in every world is a comparison with an event of that randomiser, and every utility is elicited by a standard gamble on it. The paper argues that this is how probabilities are elicited in practice, and that it makes probabilities, but not utilities, comparable across scenarios.

Setting

For each world $w$ there is a set of states $\Theta_w$, a field $Q_w$ of events on $\Theta_w$, a set of consequences $C_w$, and a set of acts $A_w$, functions $a:\Theta_w\to C_w$.

The reference events $\mathcal B$ are the Borel subsets of $[0,1]$ (RefEvents), the same in every world. A likelihood relation $\succeq_{\Theta_w}$ compares elements of the set union $Q_w\cup\mathcal B$: events of the world with each other, reference events with each other, and events with reference events, but never mixed unions of the two.

A simple distribution over $C_w$ has finite support and weights summing to one (SimpleDist); $\Psi_c$ is the point mass at $c$, and $c_1\alpha c_2$ gives probability $\alpha$ to $c_1$ and $1-\alpha$ to $c_2$. Compound gambles have prizes that are consequences or simple distributions (Gamble). A preference $\succeq_{C_w}$ on consequences extends to $\succeq_{S_w}$ on consequences and gambles, and $\succeq_{A_w}$ ranks acts. All of these relations are primitive.

Sixteen axioms constrain them: PSW1–PSW6 make $\succeq_{\Theta_w}$ a weak order that is a qualitative probability on each of $Q_w$ and $\mathcal B$, uniform on intervals, and consistently comparable across the two (LikelihoodAxioms); PSW7 is monotone continuity, PSW8 governs conditional likelihood; PSW9–PSW15 are von Neumann–Morgenstern-type axioms for $\succeq_{S_w}$ (UtilityAxioms); PSW16 says an act is valued as the simple distribution over consequences it induces.

The calibrated probability of an event is

$$P_{\Theta_w}(R)=\inf\{\pi\in[0,1]:[0,\pi]\succeq_{\Theta_w}R\}$$

(calib), the length of the reference arc held equally likely to $R$. The subjective expected utility of an act is $E(u_w\mid a)=\sum_{c}u_w(c)\,P_{\Theta_w}(a^{-1}\{c\})$ (actEU).

Formalization targets

Goal: Theorem 1

In every world, under PSW1–PSW6 and PSW9–PSW16 (with the two corrections below), $P_{\Theta_w}$ is a finitely additive probability agreeing with $\succeq_{\Theta_w}$, and there is $u_w$, unique up to positive affine transformations, with

$$a\succeq_{A_w}a'\iff E(u_w\mid a)\ge E(u_w\mid a').$$

Under PSW7, $P_{\Theta_w}$ is countably additive; under PSW8, conditional likelihood is represented by $P_{\Theta_w}(R\cap T)/P_{\Theta_w}(T)$.

Milestones

1. Calibration, eqs. (9)–(10): $R\sim_{\Theta_w}[0,P_{\Theta_w}(R)]$ for a unique value.
2. Monotonicity, eq. (11), and additivity, eqs. (12)–(13).
3. Lemma 1(a)–(c): finite additivity and agreement; countable additivity; conditional probability.
4. The standard-gamble equivalent $c\sim_{S_w}c^*_w\alpha c_{w*}$, and its extension (16) to simple distributions.
5. Lemma 2: the expected-utility representation of $\succeq_{S_w}$ with uniqueness.

Significance

The theorem gives a constructive subjective expected utility representation: the probability is the calibration against the reference experiment, and the utility is the standard-gamble probability. Because every world uses the same reference experiment, a probability of $0.3$ means the same degree of belief in every scenario; utilities carry no such common scale (p.33 of the manuscript). This is the property scenario-focused decision analysis needs to compare judgements across scenarios.

Formalization adds three reusable results with explicit hypotheses: a qualitative-probability representation calibrated by a uniform reference experiment (Lemma 1), a von Neumann–Morgenstern expected-utility theorem with uniqueness for simple lotteries (Lemma 2), and the combination into an act-level representation. The paper's proofs are outlines. Checking them exposed two places where a printed axiom is weaker than what the proof uses; both are recorded below with counterexamples. No machine-checked version of these results is on the platform.

Difficulty

The argument is elementary but long, and the obvious shortcuts fail. Showing that $\pi_R$ exists needs the connectedness of $[0,1]$ together with the closedness axiom PSW6; the closedness is not decoration. Additivity cannot be read off qualitative probability on $Q_w$ alone: it comes from comparing $S$ with the half-open reference interval $(P(R),P(R\cup S)]$, which is not an interval PSW2 speaks about, so its likelihood has to be derived from PSW2 and PSW4, and the comparison needs the strict form of PSW5(b). Countable additivity needs continuity at the empty set. On the utility side, reducing a simple distribution to one standard gamble needs one substitution (PSW14) per consequence and a single reduction (PSW15), with distinct consequences possibly receiving equal standard-gamble probabilities. The uniqueness of $u_w$ up to positive affine transformations is a separate argument in both directions.

Formalization scope

Each world is a SmallWorld Θ C. Events of $\Theta$ and reference events are kept apart in Set Θ ⊕ Set ℝ; the paper's single empty set is restored by requiring $\emptyset_\Theta\sim\emptyset_{\mathcal B}$. PSW2 is imposed for open and closed intervals only, as printed. Probabilities $\alpha,\pi\in[0,1]$ are elements of unitInterval. Compound gambles are one level deep. Every act is assumed to have finite range and events as fibres, which covers both cases of the paper's standing finiteness assumption. The goal is stated for a family of worlds indexed by an arbitrary type.

Two corrections are explicit, separate hypotheses. C1 (CorrectionC1): PSW5(b) also holds with strict conclusions when one premise is strict, as the proof of additivity uses; without it, a two-state example satisfying PSW1–PSW8 as printed has $\pi_{\{a\}}+\pi_{\{b\}}=1.2$. C2 (CorrectionC2): $c\sim_{S_w}\Psi_c$, as the proof of Lemma 2 uses; without it, a lexicographic order satisfies PSW9–PSW15 and has no utility representation. Lemma 1's uniqueness is stated among probabilities calibrated on the reference experiment, since uniqueness among all agreeing probabilities is false.

The probability in the goal is the definition calib, not "some probability agreeing with $\succeq_{\Theta_w}$", and none of the relations is defined from a measure or a utility; either shortcut would make the goal a different theorem. A verification file exhibits a world satisfying every hypothesis of the goal.

Proofs of the milestones, alternative arguments for Lemma 2, and an extension to Theorem 2 (infinite consequence spaces, not part of this mission) are welcome.

Selected references

• S. French, Axiomatising the Bayesian Paradigm in Parallel Small Worlds, author's accepted manuscript, Operations Research manuscript OPRE-2018-05-258, WRAP 118263. http://wrap.warwick.ac.uk/118263
• S. French, Axiomatizing the Bayesian Paradigm in Parallel Small Worlds, Operations Research, 2022. https://doi.org/10.1287/opre.2019.1896
• M. H. DeGroot, Optimal Statistical Decisions, McGraw-Hill, 1970 (Wiley Classics reprint, 2004). https://doi.org/10.1002/0471729000
• S. French and D. Rios Insua, Statistical Decision Theory, Arnold, 2000. ISBN 978-0340740590
• L. J. Savage, The Foundations of Statistics, Wiley, 1954. https://archive.org/details/foundationsofsta00sava

Motivation

Patent offices, grant agencies and journals screen proposals with limited reviewer time. A reviewer who cannot find concrete evidence about a proposal leaves the decision maker with a choice: reject it and possibly lose a good idea, or give it the benefit of the doubt and possibly fund a bad one. Figueroa and Lemus (SSRN 3840423, version of April 4, 2022) show that the second option has a further cost. An applicant who knows that an idea is bad gains from a report that finds nothing, and so has a reason to make the proposal harder to read. The paper calls this strategic obfuscation.

The policy question is direct. Concerns about insufficient examination time (Frakes and Wasserman, 2017) led the United States Patent and Trademark Office to give examiners more resources. If applicants respond strategically, more resources need not help. The model's communication technology follows Dewatripont and Tirole (2005), in which the sender can affect how likely a message is to get through. The published version of the paper appeared as The Benefit of the Doubt: Patent Examination Under Strategic Obfuscation in Management Science (doi:10.1287/mnsc.2023.00140). This mission uses the numbering of the SSRN version only.

Setting

An idea has value $v\in\{0,V\}$ with prior $p=\Pr(v=V)$, and its value is known to the applicant. The sponsor pays $c$ to fund any idea, with $0<c<V$, and the applicant receives $g>0$ if funded. The applicant chooses obfuscation effort $e\ge 0$ at cost $e$. A reviewer with fixed resources $\sigma\in[0,1]$ finds hard evidence of $v$ with probability $\pi(\sigma,e)$, where $\pi$ increases in $\sigma$, decreases in $e$, $\pi(1,0)=1$ and $\pi(\sigma,0)<1$ for $\sigma<1$. The function is submodular: more effort lowers the marginal value of resources (Assumption 1). Without evidence the proposal is uncertified. The sponsor then holds a posterior $Q$ and funds with probability $\alpha$. Certified ideas are funded, rejected ones are not, and good applicants do not obfuscate.

A bad applicant's best response solves

$$e(\alpha,\sigma)\in\arg\max_{e\ge 0}\ \alpha g(1-\pi(\sigma,e))-e.$$

An equilibrium at $\sigma$ is $(e^*,\alpha^*,Q^*)$ with $e^*=e(\alpha^*,\sigma)$, $Q^*$ given by Bayes' rule, and $\alpha^*$ maximizing $\alpha(Q^*V-c)$. The sponsor's payoff is

$$u_S=p\,\pi(\sigma,0)(V-c)+\alpha^*\bigl[p(1-\pi(\sigma,0))(V-c)-(1-p)(1-\pi(\sigma,e^*))c\bigr].$$

The threshold $\bar\sigma_1$ is the largest $\sigma$ below which $e(1,\cdot)$ vanishes. With $f(\sigma)=[1-\pi(\sigma,0)]p(V-c)-[1-\pi(\sigma,e(1,\sigma))](1-p)c$, the benefit minus the cost of funding at maximal effort, the threshold $\bar\sigma_2$ is the largest $\sigma$ with $f(\sigma)>0$.

Formalization targets

Goal: Proposition 2

For $0<p<1$, every detection probability $\pi$, every effort selection and every equilibrium family, $u_S$ is strictly increasing on $[0,1]$ if $pV\le c$, and on $[0,\bar\sigma_1)$ and $(\bar\sigma_2,1]$ if $pV>c$. At each $\sigma\in(0,1)$ where $e^*$ and $\pi$ are differentiable,

$$u_S'(\sigma)<0\iff pV>c,\ \ \sigma\in(\bar\sigma_1,\bar\sigma_2),\ \ \frac{\partial\pi(\sigma,e^*)}{\partial\sigma}+\frac{\partial\pi(\sigma,e^*)}{\partial e}\frac{\partial e^*}{\partial\sigma}<0.$$

Some instance and equilibrium family have $\sigma<\sigma'$ in $(\bar\sigma_1,\bar\sigma_2)$ with $u_S(\sigma')<u_S(\sigma)$.

Milestones

1. Effort vanishes at $\alpha=0$ or $g=0$ and increases in $\alpha$, $\sigma$ and $g$.
2. Inequality (3) is equivalent to $Q^*V>c$, and $Q^*\le p$.
3. Proposition 1: the three kinds of equilibrium.
4. Equilibria without obfuscation.
5. The Claim: the threshold $\bar\sigma_2$ and its comparative statics.
6. Equilibria with obfuscation.
7. The payoff formulas for $\alpha^*<1$ and $\alpha^*=1$.
8. The worked example $\pi(\sigma,e)=\sigma q(e)$ with $q(e)=1-\sqrt{2e}$ for $e\le 1/2$, $q(e)=0$ otherwise.

Significance

The result. Proposition 2 says that the value of examination resources is not monotone. A sponsor comparing budgets has to know the prior quality of ideas and the current level of resources, because near the middle of the range a larger budget buys detection that induced obfuscation more than cancels. This is the first policy finding of the paper. Propositions 3 to 7, on investment in knowledge and on competition, are built on the same equilibrium analysis.

The formalization. The results are proved on paper and, as far as the platform's catalog shows, have not been machine-checked. The mission produces a complete treatment of all equilibria of a screening game with costly obfuscation, including non-unique equilibria and off-path beliefs. It also records the corrections needed for the printed statements. Proposition 2 fails at $p=1$ and at $p=0$. Step a.2 of the proof of Proposition 1 draws a conclusion about $\alpha^*$ that does not follow. The Claim needs $e(1,1)>0$, $e(1,0)=0$ and $p<1$, and its inequality (3) holds strictly below $\bar\sigma_2$.

Difficulty

The paper's proof reads the sign of $u_S'$ directly from two payoff formulas and treats $e^*$ as differentiable. That argument does not close in the generality stated. Effort is an arbitrary selection of an argmax and can jump, $e^*$ has a kink at $\bar\sigma_1$, and the mixing regime starts at $\bar\sigma_2$, where the two payoff formulas meet. The iff therefore has to be decided at the boundary points $\sigma=\bar\sigma_1$ and $\sigma=\bar\sigma_2$, where the formula on one side tells nothing about the derivative. Equilibrium need not be unique at a given $\sigma$, so a statement about one chosen branch would not be Proposition 2. The monotonicity of $f$, which the paper derives by differentiating, has to hold with no derivative of $e$ available.

Formalization scope

The Lean development works with functions $\pi,E:\mathbb R\to\mathbb R\to\mathbb R$ read on $[0,1]\times[0,\infty)$ and $[0,1]^2$; no hypothesis looks outside those sets. Assumption 1 is stated in difference form (IsDetection), which contains the paper's $C^2$ class and its own example, whose $q$ is flat for $e\ge 1/2$. A fixed selection $E$ of (1) is used consistently in the equilibrium and in both thresholds. Bayes' rule (2) and equation (4) are cross-multiplied, so that an off-path report at $\sigma=1$, $e=0$ leaves $Q$ free instead of inheriting $0/0=0$. The thresholds are suprema, which agree with the paper's definitions for continuous $f$ and keep the goal free of continuity hypotheses. The partial of $\pi$ in $e$ is a derivative within $[0,\infty)$. Continuity appears only in the location of $\bar\sigma_2$ and in the existence of a solution of (4).

A trivializing reading is ruled out: the goal is a conditional on an equilibrium at every $\sigma$, and its last clause supplies an instance with such a family and a real fall in payoff.

No new infrastructure is needed beyond one-variable real analysis in Mathlib. The two-point revealed-preference comparisons of milestone 1 are reusable for other games with an argmax selection. Proofs of milestones in any order are welcome. Propositions 3 to 8 are outside this mission.

Selected references

• N. Figueroa and J. Lemus, The Benefit of the Doubt: Decision Making under Strategic Obfuscation, SSRN working paper 3840423, version of April 4, 2022. https://ssrn.com/abstract=3840423
• N. Figueroa and J. Lemus, The Benefit of the Doubt: Patent Examination Under Strategic Obfuscation, Management Science, 2023. https://doi.org/10.1287/mnsc.2023.00140
• M. Dewatripont and J. Tirole, Modes of Communication, Journal of Political Economy 113, 1217–1238, 2005. https://doi.org/10.1086/498586
• M. D. Frakes and M. F. Wasserman, Is the Time Allocated to Review Patent Applications Inducing Examiners to Grant Invalid Patents? Evidence from Microlevel Application Data, Review of Economics and Statistics 99, 550–563, 2017. https://doi.org/10.1162/REST_a_00605

Motivation

A prophet inequality compares an online decision maker, who sees random values one at a time and must accept or reject each irrevocably, with a "prophet" who sees all values in advance. The classical single-item version (Krengel–Sucheston, Samuel-Cahn) guarantees half of the prophet's expected value. Since the work of Hajiaghayi, Kleinberg and Sandholm (2007) and Chawla, Hartline, Malec and Sivan (2010), prophet inequalities have been the standard tool for designing posted-price mechanisms: a competitive ratio for the online problem becomes a revenue or welfare guarantee for sequential pricing.

Matching markets (ride-sharing, kidney exchange, online advertising) are the natural combinatorial setting. Ezra, Feldman, Gravin and Tang (arXiv:2002.09807; Mathematics of Operations Research, 2022) study the case where the edges of a known graph arrive one by one, each with an independently drawn weight, and the algorithm must keep a matching. The paper gives the ratio 0.337 for every graph, improving the constant $1/(2e)\approx0.18$ obtainable from the greedy OCRSs of Feldman, Svensson and Zenklusen.

Timeline:

• 1977–1984: Krengel–Sucheston and Samuel-Cahn, ratio 1/2 for one item.
• 2012: Kleinberg–Weinberg, ratio 1/2 for matroids.
• 2016: Feldman, Svensson and Zenklusen introduce online contention resolution schemes (OCRS), with a $(b,e^{-2b})$-selectable greedy OCRS for matchings, i.e. selectability $1/(2e)$ at $b=1/2$ (arXiv:1508.00142).
• 2020: this paper, ratio 0.337 for edge arrivals in general graphs and 1/2 (tight) for vertex arrivals.

Setting

A finite simple graph $G=(V,E)$, not necessarily bipartite, is known. Each edge $e$ has a weight $w_e\sim F_e$, the weights are independent, and the laws $F_e$ are known; no sign condition is imposed. A matching is a set of edges no two of which share a vertex; $\mathcal M$ is the family of matchings and $w(M)=\sum_{e\in M}w_e$.

The edges arrive in an order $\sigma$ chosen by an oblivious adversary, who does not see the weights or the algorithm's coins. When an edge arrives, its weight is revealed and an online policy decides, from the edges seen so far, their weights and its own randomness, whether to add the edge; it is added only if both its ends are still unmatched. The policy's value under $\sigma$ is $\mathbb E[w(I)]$.

The fractional matching polytope is $\mathcal F_M=\{y\ge0:\ \sum_u y_{(uv)}\le1\ \forall v\}$. An ex-ante rule chooses measurable acceptance probabilities $q_e:\mathbb R\to[0,1]$ whose marginals $x_e=\mathbb E[q_e(w_e)]$ lie in $\mathcal F_M$; its value is $V(q)=\sum_e\mathbb E[w_e\,q_e(w_e)]$. The ex-ante optimum of §6 and §B.2 is the best threshold rule.

An OCRS for $x\in\mathcal F_M$ faces edges that are realized independently with probabilities $x_e$; it selects realized edges online, keeping a matching, and is $c$-selectable if every edge is selected with probability at least $c\,x_e$ under every order.

Formalization targets

Goal

$$\exists\ \text{policy}\ \forall\sigma:\quad \mathbb E_{w,I}[w(I)]\ \ge\ 0.337\cdot\mathbb E_w\Big[\max_{M\in\mathcal M}w(M)\Big],$$

and, for every ex-ante rule $q$,

$$\exists\ \text{policy}\ \forall\sigma:\quad \mathbb E_{w,I}[w(I)]\ \ge\ 0.337\cdot V(q).$$

One policy serves all orders; it never learns $\sigma$ in advance.

Milestones, in proof order

• Eq. (2) and Theorem 2.3: a $c$-selectable batched OCRS for the resampled optimum $R(w,F)$ yields a $c$-competitive batched prophet algorithm.
• §3: the marginals $x^{opt}_e=\Pr[e\in\mathrm{OPT}(w)]$ lie in $\mathcal F_M$.
• Eq. (8): Algorithm 3 selects each realized edge with probability exactly $c$, provided $\alpha_e=c/\Pr[\text{both ends unmatched at }e]\le1$.
• Eqs. (10)–(13), Lemmas 5.4 and 5.5, Eq. (15): lower bounds on $\Pr[u,v\text{ unmatched at }(uv)]$ through witnesses.
• Lemma 5.6 and Lemma 5.2: $\Pr[u,v\text{ unmatched at }(uv)]\ge1-2c+\frac{c^2}{2}\big(\frac{1-2c}{1-c}\big)^2$.
• Theorem 5.3: a 0.337-OCRS for every $x\in\mathcal F_M$.
• §B.2: an OCRS for the marginals of an ex-ante rule yields a prophet policy against that rule.

Significance

The result gives the first constant-factor prophet inequality for weighted matching with edge arrivals in general graphs, and through the standard pricing reductions a constant-factor posted-price mechanism for matching markets in which pairs are offered sequentially. The guarantee holds against the ex-ante relaxation, which dominates both the optimal fractional and the optimal integral matching, so it also bounds the gap between online and offline stochastic matching LPs. The reduction of Theorem 2.3 is general: any batched OCRS for any downward closed family yields a batched prophet inequality, which the paper also uses for vertex arrivals.

The paper's proofs are on paper only. As far as is known, no prophet inequality for matchings, and no OCRS analysis with a correlation lower bound of this kind, has a machine-checked proof. The mission asks for a formal proof of the full chain: the general reduction, the exact selection probability of Algorithm 3, the witness argument, and the final assembly. Sharper constants are out of scope: the paper's own upper bounds (3/7 against the fractional optimum, 135/321 against the ex-ante optimum, §6) leave the true constant open.

Difficulty

The obvious analysis is the union bound of the warm-up Theorem 5.1: $u$ and $v$ are each matched before $(uv)$ with probability at most $c$, so both are free with probability at least $1-2c$, which equals $c$ at $c=1/3$. Beyond $1/3$ one needs a lower bound on $\Pr[u\text{ and }v\text{ both matched}]$. Treating the two events as independent would give about $0.382$, but they can be negatively correlated, and their law depends on every earlier $\alpha_e$, which itself depends on the bound being proved. The paper breaks this circularity by induction along the order and by exhibiting witnesses: neighbours of $u$ whose only active edge goes to $u$. Bounding the witness probability requires a resampling argument (the candidate samplers $\pi_u,\pi_v$) and a monotonicity lemma (Lemma 5.4) that does not follow from independence.

Formalization scope

The Lean development fixes:

• $G$ is a Mathlib SimpleGraph on a finite vertex type; edges are the elements of G.edgeSet. A matching is a finite set of pairwise vertex-disjoint edges, and the benchmark is a finite maximum over matchings (never a real supremum).
• Weights have law Measure.pi F with each $F_e$ a probability measure with finite mean. The constant is the literal $337/1000$.
• A policy is a structure carrying its probability space and a decision rule whose inputs are only the earlier edges with weights, the current edge and weight, and its randomness; its decision is measurable. The run adds an accepted edge only if both ends are free, so every run is a matching. The quantifier order is $\exists$ policy $\forall$ order. A policy that could read the order or the future weights would make the goal trivial; the types exclude it.
• Conditional probabilities are stated in product form, since the conditioning events may be null.
• The analysis of Algorithm 3 is stated in the paper's active-edge process (p. 14), with probabilities as finite sums over activation patterns. The well-definedness hypothesis is $c\le\Pr[\text{both ends free}]$, never $\alpha_e\le1$, which would be vacuous at the junk value $c/0=0$.
• The batched reduction is stated for any finite ground set, any downward closed family, any set of ordered partitions and any measurable maximizer.

Useful infrastructure, reusable beyond this mission: finite product measures of Bernoulli realizations, the expectation of a function of independent coordinates, and the bookkeeping of greedy runs on ordered edge lists. Contributions of proofs of any milestone, or of sketches decomposing them, are welcome.

Selected references

• T. Ezra, M. Feldman, N. Gravin, Z. G. Tang, Online Stochastic Max-Weight Matching: prophet inequality for vertex and edge arrival models, arXiv:2002.09807v2, 2020; published as Prophet Matching with General Arrivals, Mathematics of Operations Research, 2022. https://arxiv.org/abs/2002.09807
• M. Feldman, O. Svensson, R. Zenklusen, Online Contention Resolution Schemes, SODA 2016. https://arxiv.org/abs/1508.00142
• R. Kleinberg, S. M. Weinberg, Matroid Prophet Inequalities, STOC 2012. https://arxiv.org/abs/1201.4764
• S. Chawla, J. Hartline, D. Malec, B. Sivan, Multi-parameter Mechanism Design and Sequential Posted Pricing, STOC 2010. https://arxiv.org/abs/0907.2435
• M. T. Hajiaghayi, R. Kleinberg, T. Sandholm, Automated Online Mechanism Design and Prophet Inequalities, AAAI 2007. https://www.aaai.org/Papers/AAAI/2007/AAAI07-009.pdf

Why error bounds for composite surrogates matter

In derivative-free and blackbox optimization, the objective can often be evaluated but not differentiated, and algorithms work with surrogate models built from function values. Their convergence theory depends on how accurate those models are. Conn, Scheinberg and Vicente codified this through fully linear and fully quadratic models; a fully linear class controls the function error to order $\Delta^2$ and the gradient error to order $\Delta$ over a ball of radius $\Delta$.

Many objectives are not pure blackboxes. They are products, quotients or compositions of several expensive components, each of which can be modelled on its own. One then needs to know how the accuracy of the sub-models carries over to the assembled surrogate. Chen, Hare and Jarry-Bolduc (arXiv:2112.08411v1) answer this with explicit error constants, in the order-$N$ terminology of Hare (Set-Valued and Variational Analysis, 2020). This mission covers their product results.

Setting

Fix $x_0\in\mathbb R^d$ and $\bar\Delta>0$. Write $B_\Delta(x_0)$ for the closed ball of radius $\Delta$. A class of models of $f:\mathbb R^d\to\mathbb R$ is a family $\{\tilde f_\Delta\}_{(0,\bar\Delta]}$ of real functions on $\mathbb R^d$, one for each $\Delta\in(0,\bar\Delta]$.

For $N\ge0$ and $\kappa\ge0$, the class has order-$N$ function accuracy at $x_0$ with constant $\kappa$ if $|f(x_0)-\tilde f_\Delta(x_0)|\le\kappa\Delta^N$ for every $\Delta\in(0,\bar\Delta]$. It has this accuracy near $x_0$ if the same bound holds for every $x\in B_\Delta(x_0)$; the radius of the ball is the model's own index. Gradient accuracy and Hessian accuracy replace $f,\tilde f_\Delta$ by $\nabla f,\nabla\tilde f_\Delta$ and by $\nabla^2f,\nabla^2\tilde f_\Delta$.

The class is uniformly bounded at $x_0$ if $|\tilde f_\Delta(x_0)|\le M$ for one $M\ge0$ and every $\Delta$, and near $x_0$ if the bound holds on each $B_\Delta(x_0)$. Order-$\infty$ function accuracy at $x_0$ with constant $0$ means $\tilde f_\Delta(x_0)=f(x_0)$ for all $\Delta$. For sub-models $\tilde f_{i,\Delta}$ of $f_i$, write $F=f_1\cdots f_n$, $\tilde F_\Delta=\tilde f_{1,\Delta}\cdots\tilde f_{n,\Delta}$ and $F_i=\prod_{j\ne i}f_j$. Let $M_{\nabla f_i}(x_0)$ bound $\|\nabla f_i\|$ on $B_{\bar\Delta}(x_0)$, and let $M_{\nabla\tilde f_i}(x_0)$ bound $\|\nabla\tilde f_{i,\Delta}(x_0)\|$ uniformly in $\Delta$.

Formalization targets

Goal: Theorem 19

Let each $f_i$ be $C^2$. Suppose each class is exact at $x_0$ and provides order-$N^g_i$ gradient accuracy with constant $\kappa^g_i(x_0)$ and order-$N^h_i$ Hessian accuracy with constant $\kappa^h_i(x_0)$ at $x_0$. With $N^{gh}_F=\min\{N^g_i,N^h_i\}$, for every $\Delta\in(0,\bar\Delta]$,

$$\|\nabla^2F(x_0)-\nabla^2\tilde F_\Delta(x_0)\|\le K^h_F(x_0)\,\Delta^{N^{gh}_F},$$ $$K^h_F(x_0)=\sum_{i=1}^n\Bigl[\sum_{j\ne i}\Bigl(\prod_{k\ne i,j}|f_k(x_0)|\Bigr)\bigl(M_{\nabla f_j}(x_0)+M_{\nabla\tilde f_j}(x_0)\bigr)\Bigr]\kappa^g_i(x_0)\bar\Delta^{N^g_i-N^{gh}_F}+\sum_{i=1}^n|F_i(x_0)|\,\kappa^h_i(x_0)\bar\Delta^{N^h_i-N^{gh}_F},$$

and $\{\tilde F_\Delta\}_{(0,\bar\Delta]}$ provides order-$N^{gh}_F$ Hessian accuracy of $F$ at $x_0$. Both the explicit bound and the order statement are part of the goal.

Milestones

In the order the paper builds them:

• Corollary 5: function, gradient and Hessian accuracy of $f$ of class $C^0$, $C^1$, $C^2$ give uniform boundedness of $\{\tilde f_\Delta\}$, $\{\|\nabla\tilde f_\Delta\|\}$, $\{\|\nabla^2\tilde f_\Delta\|\}$, at and near $x_0$.
• Theorem 6: function accuracy of $f_1f_2$, at and near $x_0$, with a minimum of two constants.
• Theorem 8: gradient accuracy of $f_1f_2$ for models exact at $x_0$.
• Theorem 12: Hessian accuracy of $f_1f_2$ for models exact at $x_0$.
• Theorem 14: function accuracy of $f_1\cdots f_n$, at and near $x_0$, with a constant that is a minimum over the permutations of the factors.
• Theorem 16: gradient accuracy of $f_1\cdots f_n$ for models exact at $x_0$.

Significance

The result. Theorem 19 tells an algorithm designer what accuracy to demand from each component model, and supplies a constant computed from sub-model data rather than an unspecified $O(\cdot)$. The order in the bound is the worst among the factors, so under this bound making one factor far more accurate than the others does not raise the order of the product.

The formalization. The theorems are proved in the paper by direct calculation; none is an open problem. A search of the available formal libraries found no machine-checked proof of them and no formal definition of order-$N$ model accuracy. The mission gives a reusable vocabulary of accuracy predicates and a checked form of the constants, including the indexing of the double sum in (3).

Difficulty

For two factors the obvious expansion is short, and the difficulty lies in the passage to $n$ factors and in Lean. The Hessian of a product contains the rank-one terms $\nabla f_i\nabla f_j^\top$ over ordered pairs, which couple true and model gradients; this is why both $M_{\nabla f_j}$ and $M_{\nabla\tilde f_j}$ appear in (3), and why the indexing of (3) is easy to get wrong. The second derivative of an $n$-fold product is awkward for the Fréchet derivative: it is a bilinear map, and a first-derivative formula valid only at $x_0$ cannot be differentiated again. The models are assumed regular only at $x_0$, so reasoning that treats $\tilde F_\Delta$ as $C^2$ everywhere uses more than the statement assumes.

Formalization scope

Theorems are stated on EuclideanSpace ℝ (Fin d); the accuracy predicates are stated on any real normed space. Gradients are fderiv ℝ f with the operator norm, which agrees with the Euclidean norm of $\nabla f$; Hessians are fderiv ℝ (fderiv ℝ f) with the operator norm of the bilinear map, the spectral norm. A class of models is a map ℝ → E → ℝ, used only for Δ ∈ Set.Ioc 0 Δbar, and $\Delta^N$ is Real.rpow. The predicates carry $\kappa$ as an argument and contain $N\ge0$ and $\kappa\ge0$; "provides order-$N$ accuracy" is ∃ κ, ….

The paper leaves the regularity of the models implicit. Since fderiv is $0$ at a non-differentiable point, a Lean statement without it would be false or empty, so the at-$x_0$ gradient theorems assume DifferentiableAt of each model at $x_0$ and the Hessian theorems ContDiffAt ℝ 2. The bounds $M$ are numbers with hypotheses rather than suprema, so each theorem holds for every valid choice and no junk value can enter. Minima are stated with IsLeast, which also forces $n\ge1$. Exactness at $x_0$ is the equality $\tilde f_{i,\Delta}(x_0)=f_i(x_0)$.

A complete development needs the Leibniz rule for second derivatives of finite products, reusable beyond this mission, plus routine rpow monotonicity. Proofs of the milestones and of the Leibniz formula are welcome, and so are proofs of Theorem 19 that do not pass through the two-factor case.

Selected references

• Y. Chen, W. Hare, G. Jarry-Bolduc, Error Analysis of Surrogate Models Constructed through Operations on Sub-models, arXiv:2112.08411v1, 2021. https://arxiv.org/abs/2112.08411
• A. R. Conn, K. Scheinberg, L. N. Vicente, Introduction to Derivative-Free Optimization, SIAM, 2009. https://doi.org/10.1137/1.9780898718768
• W. Hare, A discussion on variational analysis in derivative-free optimization, Set-Valued and Variational Analysis 28, 2020, pp. 643–659 (reference [9] of the paper above).