All missions

Why the cost of path simulation matters

Pricing a financial derivative, estimating a risk measure, or computing any expected functional of a stochastic differential equation (SDE) by simulation runs into two errors at once: the statistical error of averaging finitely many sampled paths, and the discretisation bias of replacing the exact SDE solution by a numerical scheme with a positive timestep. With the Euler scheme and $N$ independent paths, the mean-square error behaves like $c_1N^{-1}+c_2h^2$, so a root-mean-square accuracy $\varepsilon$ requires $N\sim\varepsilon^{-2}$ paths of $h^{-1}\sim\varepsilon^{-1}$ steps each: a cost of order $\varepsilon^{-3}$.

Giles' Multilevel Monte Carlo path simulation (Operations Research 56(3), 2008) showed that combining simulations on a geometric hierarchy of timesteps reduces this cost to order $\varepsilon^{-2}(\log\varepsilon)^2$ for the Euler scheme with a Lipschitz payoff, and to $\varepsilon^{-2}$, the cost of an unbiased estimator, when the level differences have fast-decaying variance. The two-level case is due to Kebaier (2005), who reduced the cost to order $\varepsilon^{-2.5}$; Heinrich's multilevel method for parametric integration (2001) is a precursor. The paper's Theorem 3.1 is stated abstractly, in terms of four rate conditions, and has since been applied to SDEs, SPDEs, Markov chains and nested simulation; the survey of Giles (Acta Numerica 2015) traces this development.

The multilevel estimator

Fix an integer refinement factor $M\ge2$ and a horizon $T>0$, and let the timestep of level $l$ be $h_l=M^{-l}T$, $l=0,1,2,\dots$. On a probability space, let $P$ be the quantity of interest (in the paper, a functional of the solution of an SDE driven by a Brownian path) and $\widehat P_l$ its approximation with timestep $h_l$. Since

$$E[\widehat P_L]=E[\widehat P_0]+\sum_{l=1}^{L}E[\widehat P_l-\widehat P_{l-1}],$$

the method estimates each term independently. For each level $l$ and sample size $N_l\ge1$, $\widehat Y_l$ is an estimator of $E[\widehat P_0]$ ($l=0$) or of $E[\widehat P_l-\widehat P_{l-1}]$ ($l>0$) built from $N_l$ samples, with computational complexity $C_l$. The multilevel estimator is $\widehat Y=\sum_{l=0}^{L}\widehat Y_l$, its total complexity is $C=\sum_{l=0}^LC_l$, and its mean-square error is $\mathrm{MSE}=E[(\widehat Y-E[P])^2]$.

The hypotheses are four rate conditions, with constants $\alpha\ge\frac12$ and $\beta,c_1,c_2,c_3>0$: (i) $|E[\widehat P_l-P]|\le c_1h_l^\alpha$ (weak convergence order $\alpha$); (ii) $E[\widehat Y_l]$ equals $E[\widehat P_0]$ or $E[\widehat P_l-\widehat P_{l-1}]$ (unbiasedness of each level); (iii) $V[\widehat Y_l]\le c_2N_l^{-1}h_l^\beta$ (variance decay rate $\beta$); (iv) $C_l\le c_3N_lh_l^{-1}$ (cost proportional to samples times steps).

Formalization targets

Goal: Theorem 3.1

There is a constant $c_4>0$ such that for every $0<\varepsilon<e^{-1}$ there are $L$ and $N_l\ge1$ with

$$\mathrm{MSE}<\varepsilon^2,\qquad C\le\begin{cases}c_4\varepsilon^{-2},&\beta>1,\\ c_4\varepsilon^{-2}(\log\varepsilon)^2,&\beta=1,\\ c_4\varepsilon^{-2-(1-\beta)/\alpha},&0<\beta<1.\end{cases}$$

The constant $c_4$ is uniform in $\varepsilon$; its value is not part of the goal.

Milestones

The milestones are the displayed steps of the paper's proof, in its order: the choice of the finest level and the resulting two-sided bound (6) on $c_1h_L^\alpha$; the bound $\frac12\varepsilon^2$ on the squared bias; the geometric bound (7) on $\sum_l h_l^{-1}$; and, for each of the three regimes $\beta=1$, $\beta>1$, $\beta<1$, a choice of $N_l$ with a $\frac12\varepsilon^2$ bound on the variance (using the geometric bounds (8) and (9) in the last two) and an explicit cost bound with an explicit constant $c_4$. In case $\beta=1$ the bound $L+1\le c_5\log\varepsilon^{-1}$ on the number of levels is a separate milestone.

What the result gives

The theorem turns the multilevel idea into a complexity statement: whenever a discretisation has weak order $\alpha$ and its level corrections have variance decay $\beta$, the cost of accuracy $\varepsilon$ is known up to a constant. It identifies $\beta$ as the parameter governing the method, explains where the effort is spent (coarse levels for $\beta>1$, fine levels for $\beta<1$), and is the template that later multilevel analyses (Milstein schemes, multi-index Monte Carlo, randomised MLMC) follow and refine.

The result is proved in the paper and widely reused. To our knowledge it has no machine-checked proof. The mission produces one: a Lean statement of the abstract theorem and of each step of the proof, with the paper's explicit constants. Its probabilistic content is light (linearity of expectation, the bias-variance decomposition, Bienaymé's identity for independent variables); most of the work is careful real analysis with ceilings, logarithms and real powers.

Where the difficulty lies

No single step is deep; the difficulty is bookkeeping under exact constants. The obvious argument "choose $h_L\approx\varepsilon$, choose $N_l\propto\varepsilon^{-2}h_l^{(\beta+1)/2}$" is asymptotic. The theorem demands, for every $\varepsilon<e^{-1}$, an exact bound with a constant independent of $\varepsilon$. This forces the integer ceilings in $L$ and $N_l$ to be controlled explicitly (each ceiling adds one sample per level, whose total cost is (7)), the number of levels to be bounded by a multiple of $\log\varepsilon^{-1}$, and the three geometric series to be summed with constants independent of $L$. The strict inequality $\mathrm{MSE}<\varepsilon^2$ is not delivered by the paper's own choice in case $\beta=1$, where both halves give only $\le\frac12\varepsilon^2$; a solver must adjust the sample sizes.

Formalization scope

$P$, $\widehat P_l$ and the level estimators are arbitrary real random variables on a probability space $(\Omega,\mu)$; the SDE and its discretisation enter the theorem only through (i)–(iv), so they are not modelled. This makes the statement more general, not weaker. Expectations are Bochner integrals and $V$ is Mathlib's variance. The conventions are:

• the level estimator is indexed by level and sample size, $\widehat Y_l^{(n)}$, and (ii), (iii), (iv), square integrability and mutual independence of $(\widehat Y_l^{(N_l)})_l$ are assumed for every sample size $n\ge1$ (every choice of $N_l\ge1$), because the conclusion chooses the sample sizes;
• (i) carries an absolute value: the page prints the one-sided $E[\widehat P_l-P]\le c_1h_l^\alpha$, under which the theorem is false;
• $P$ and $\widehat P_l$ are integrable and $\widehat Y_l^{(n)}\in L^2$, because Lean's integral and variance return $0$ off these classes;
• $M\ge2$ (the paper's standing assumption), $T>0$, and $\varepsilon>0$ (implicit in "$\varepsilon<e^{-1}$");
• the cost $C_l^{(n)}$ is an abstract real number constrained only by (iv), and $C=\sum_{l=0}^LC_l$;
• $L$ in (6) is an integer ceiling, which can be negative for large $\varepsilon$; the milestones with explicit constants assume it is a natural number, a case the paper's proof assumes silently, while the goal does not;
• real powers are Real.rpow, $\lceil\cdot\rceil$ is Int.ceil for $L$ and Nat.ceil for $N_l$ (whose arguments are positive).

A formalization in which the cost is defined as $c_3\sum_lN_lh_l^{-1}$, in which (ii)–(iv) hold only for one fixed sample size, or in which the MSE and cost bounds are proved for different $L$ and $N_l$, is a different and weaker theorem and is ruled out by the statement.

Infrastructure needed: geometric-series bounds with real ratios, floor and ceiling estimates for logarithms, and Bienaymé's identity (Mathlib's IndepFun.variance_sum). The bias-variance decomposition $\mathrm{MSE}=V[\widehat Y]+(E[\widehat Y]-E[P])^2$ for $L^2$ variables is reusable beyond this mission. Proofs of individual milestones, and alternative proofs of the goal, are welcome.

Selected references

• M. B. Giles, Multilevel Monte Carlo path simulation, Operations Research 56(3):607–617, 2008. https://doi.org/10.1287/opre.1070.0496
• A. Kebaier, Statistical Romberg extrapolation: a new variance reduction method and applications to option pricing, Annals of Applied Probability 15(4):2681–2705, 2005 (cited as reference in Giles 2008, p. 617).
• M. B. Giles, Multilevel Monte Carlo methods, Acta Numerica 24:259–328, 2015. https://doi.org/10.1017/S096249291500001X
• S. Heinrich, Multilevel Monte Carlo methods, Large-Scale Scientific Computing, LNCS 2179, 58–67, Springer, 2001. https://doi.org/10.1007/3-540-45346-6_5

Motivation

Retailers selling several related products can change prices as inventory runs down. A sale of one product changes the stock available in later periods, while changing its price also shifts demand toward or away from the other products. Dong, Kouvelis, and Tian study these linked decisions for substitute product variates under a multinomial logit customer choice model. Their 2009 article gives an exact characterization of the optimal dynamic price vector when each in-stock variate can have its own price. The characterization separates a product's inventory opportunity cost from a margin shared across all products, which makes the result more informative than an opaque Bellman maximization.

The mission isolates Theorem 1 of that article. The paper also studies restricted policies that require a unified price or fixed prices for some variates; those results are separate missions in this series. The present target concerns the fully flexible dynamic policy of §3.1, with the model and conventions of §2.

Setting

There are $n$ product variates, indexed by $i$, with finite quality parameters $a_i$. Time $t$ is the number of periods remaining, so it counts down to zero. The inventory state $x=(x_i)$ has nonnegative integer coordinates, and $S(x)=\{i:x_i>0\}$ is the set of variates still in stock. At most one customer arrives during a period, with probability $\lambda$ satisfying $0<\lambda\leq1$. Inventory is not replenished. The retailer chooses a finite, nonnegative price $r_i$ for each in-stock variate. An out-of-stock variate receives the paper's null price and contributes no demand.

An arriving customer chooses among the in-stock variates and the no-purchase option. The multinomial logit model assigns deterministic utility $a_i-r_i$ to variate $i$ and utility $u_0$ to no purchase, with positive scale $\mu$. Its probabilities are

$$P_i(x,r)=\frac{\exp((a_i-r_i)/\mu)}{\sum_{j\in S(x)}\exp((a_j-r_j)/\mu)+\exp(u_0/\mu)},\qquad P_0(x,r)=\frac{\exp(u_0/\mu)}{\sum_{j\in S(x)}\exp((a_j-r_j)/\mu)+\exp(u_0/\mu)}.$$

Let $\pi_t(x)$ be the maximum expected revenue from state $x$ with $t$ periods remaining and zero terminal value $\pi_0(x)=0$. A sale of variate $i$ moves the inventory to $x-e^i$. Its marginal inventory value is $\Delta^i\pi_t(x)=\pi_t(x)-\pi_t(x-e^i)$ when $i\in S(x)$. For a continuation value $V$, the one-period objective is current expected sales revenue plus the expected continuation revenue after a sale or no sale. The Bellman value takes its supremum over all finite nonnegative price vectors. Equation (5) rewrites that objective as $\xi_V(x,r)+V(x)$, where $\xi_V$ is the probability-weighted marginal revenue.

Formalization targets

Optimal dynamic prices

Theorem 1 asks for a unique common margin $m_t(x)$ satisfying

$$\left(\frac{m_t(x)}{\mu}-1\right)\exp\left(\frac{m_t(x)+u_0}{\mu}\right) =\sum_{i\in S(x)}\exp\left(\frac{a_i-\Delta^i\pi_{t-1}(x)}{\mu}\right).$$

For every in-stock variate, the price $r_i^*=\Delta^i\pi_{t-1}(x)+m_t(x)$ must be feasible and attain the Bellman maximum. The margin also satisfies $m_t(x)P_0(x,r^*)=\mu$. These claims hold for every inventory state, including an empty in-stock set. They are the main target of Theorem 1, equations (9)–(10).

Total expected revenue

For each $s=1,\ldots,t$, let $m_s(x)$ be the unique margin equation root at the same inventory state $x$, with $s$ periods remaining. The remaining clause of Theorem 1 states

$$\pi_t(x)=\lambda\sum_{s=1}^{t}\bigl[m_s(x)-\mu\bigr].$$

The milestones track the paper's equation (5) and Steps 1–5 of its Appendix A argument: marginal inventory value, the mapping between prices and choice probabilities, concavity in probability coordinates, existence of the margin, optimal choice probabilities, and the one-period value identity.

Significance

The result turns a coupled dynamic program into a precise pricing characterization. It says that differences in optimal prices across products reflect differences in their marginal inventory values; the remaining margin is common. The value identity quantifies the expected revenue earned over the remaining horizon, and the explicit maximizer removes ambiguity about whether the Bellman supremum is attained. These conclusions support the paper's comparisons with restricted pricing policies and its later discussion of how quality and inventory scarcity affect prices Dong, Kouvelis, and Tian (2009).

The result is proved in the article. This mission contributes a Lean statement of the full theorem, its model, and seven named intermediate targets. The draft declarations compile against the pinned Mathlib environment; their proofs remain open. A complete formalization would provide reusable finite MNL choice probabilities, inverse price and probability identities, and a Bellman model for substitute-product inventory. The paper's economic conclusions should be recovered from those formal statements, rather than from a weakened existence claim.

Difficulty

The direct one-period objective in the price vector is not quasiconcave, as the paper notes on p. 323, so a local condition on prices alone does not establish global optimality. The price vector also ranges over an unbounded set, and a supremum could conceal a boundary or attainment issue. Finally, one extra unit of stock changes future probabilities across all products, not just the revenue of that product. These interactions make nonnegative marginal inventory value and the global optimality assertion substantive parts of the result. The probability-space objective is concave on its positive domain, but the printed Appendix A claim of strict concavity on the full domain is stronger than that function permits; uniqueness concerns the normalized choice-probability slice.

Formalization scope

Lean represents products by Fin n, inventories by functions Fin n → ℕ, and time by a natural number counting remaining periods. The model assumes $\mu>0$ and $0<\lambda\leq1$. The set $S(x)$ filters positive inventory coordinates; an out-of-stock variate is removed from every choice-probability sum, so its null price need not be encoded as a finite real. The objective's no-sale continuation term is counted once, following equations (5) and (22), despite the ambiguous bracket placement in printed equation (3). In-stock prices are finite and nonnegative. Off-stock coordinates of the displayed candidate vector are set to zero and do not affect demand.

Lean's natural-number subtraction in $x-e^i$ is used only for $i\in S(x)$, where it subtracts exactly one unit. The Bellman value uses a real sSup, whose default on a badly bounded set could otherwise obscure the theorem. The goal and final milestone therefore require an explicit maximizing price vector and equality between the value and its objective. The margin root is stated as unique and every root is covered; it is not hidden behind a choice operator. Equation (11) quantifies over all roots for $s=1,\ldots,t$ at one fixed $x$, not along a sample path. No assumption that $n>0$ or $S(x)$ is nonempty is added to the goal. The price–probability mapping and interior optimality milestones assume $S(x)$ nonempty where the paper's positive-simplex argument requires it.

A complete development needs finite-sum algebra, real exponential and logarithm facts, concavity on products of real function spaces, and boundedness and attainment facts for the Bellman objective. The MNL probability and inverse-map facts can serve later pricing models; the dynamic value and marginal-stock lemmas serve inventory-control formalizations. Contributions that prove these statements or isolate reusable analytic lemmas are within scope. The statement must retain both the Bellman maximizer and the value identity, so a default sSup value cannot turn the goal into a trivial equality.

Selected references

• Lingxiu Dong, Panos Kouvelis, and Zhongjun Tian, Dynamic Pricing and Inventory Control of Substitute Products, Manufacturing & Service Operations Management 11(2), 317–339, 2009. DOI: 10.1287/msom.1080.0221.

Motivation

Cryptographic keys must be uniformly random and reproducible exactly. Many secrets people actually possess are neither: a biometric reading (an iris code, a fingerprint template), a long passphrase recalled with typos, or the correlated bits two parties obtain from a quantum channel are noisy, so two readings of the same secret differ in a few positions, and they are not uniform. Fuzzy extractors, introduced by Dodis, Ostrovsky, Reyzin and Smith (arXiv:cs/0602007; SIAM J. Comput. 38(1), 2008), turn such a secret into a nearly uniform key that can be regenerated from any sufficiently close reading, using public helper data that does not compromise the key.

The construction for the Hamming metric is the one most used in practice and in later work on biometric key derivation and physically unclonable functions. Its history is short. Juels and Wattenberg's fuzzy commitment (CCS 1999) shifted an error-correcting code onto the secret but was analysed only for uniform inputs. The syndrome of a linear code had been used for information reconciliation in quantum key agreement (Bennett, Bessette, Brassard, Salvail and Smolin, J. Cryptology 1992). Dodis et al. defined secure sketches and fuzzy extractors for arbitrary entropy distributions, introduced average min-entropy to handle side information, and proved the bound formalized here. This mission is the first of four drawn from that paper.

Setting

All logarithms are base 2. A random variable is identified with its law. For a random variable $A$, the min-entropy is $\mathbf H_\infty(A) = -\log \max_a \Pr[A=a]$. For a pair $(A,B)$, the average min-entropy of $A$ given $B$ is

$$\tilde{\mathbf H}_\infty(A\mid B) = -\log \mathbb E_{b\leftarrow B}\big[\max_a \Pr[A=a\mid B=b]\big],$$

the adversary's chance of guessing $A$ after seeing $B$, on a log scale. The statistical distance is $\mathbf{SD}(A,B)=\tfrac12\sum_v|\Pr(A=v)-\Pr(B=v)|$, and $U_\ell$ is uniform on $\{0,1\}^\ell$.

The space is $\mathcal M=\mathcal F^n$, where $\mathcal F$ is a finite additive group with $F$ elements, $f=\log F$, and $\mathrm{dis}(w,w')$ is the Hamming distance, the number of positions where $w$ and $w'$ differ. A code $C\subseteq\mathcal F^n$ with $K$ codewords is an $[n,k,2t+1]_{\mathcal F}$ code if distinct codewords are at distance at least $2t+1$; its dimension is $k=\log_F K$, so $kf=\log K$.

A secure sketch $(\mathsf{SS},\mathsf{Rec})$ is a pair of randomized procedures with $\mathsf{Rec}(w',\mathsf{SS}(w))=w$ whenever $\mathrm{dis}(w,w')\le t$. It is an average-case $(\mathcal M,m,\tilde m,t)$-secure sketch if $\tilde{\mathbf H}_\infty(W\mid(\mathsf{SS}(W),I))\ge\tilde m$ for every pair $(W,I)$ with $\tilde{\mathbf H}_\infty(W\mid I)\ge m$. A fuzzy extractor $(\mathsf{Gen},\mathsf{Rep})$ has $\mathsf{Gen}(w)=(R,P)$ with $R\in\{0,1\}^\ell$, and $\mathsf{Rep}(w',P)=R$ whenever $\mathrm{dis}(w,w')\le t$. It is an average-case $(\mathcal M,m,\ell,t,\varepsilon)$-fuzzy extractor if

$$\mathbf{SD}\big((R,P,I),(U_\ell,P,I)\big)\le\varepsilon \quad\text{whenever}\quad \tilde{\mathbf H}_\infty(W\mid I)\ge m .$$

A family $\{H_x\}_{x\in X}$ of functions into $\{0,1\}^\ell$ is universal if $\Pr_{x}[H_x(a)=H_x(b)]=2^{-\ell}$ for all $a\ne b$.

Formalization targets

Goal: Theorem 5.2 (p. 17)

For every $[n,k,2t+1]_{\mathcal F}$ code, every $m$, every $\varepsilon>0$ and every natural number

$$\ell\;\le\;m+kf-nf-2\log(1/\varepsilon)+2,$$

there is an average-case $(\mathcal F^n,m,\ell,t,\varepsilon)$-fuzzy extractor.

The sketch branch

• Lemma 2.2(b): publishing a value with at most $2^\lambda$ possibilities lowers average min-entropy by at most $\lambda$.
• Lemma 3.1: a correct sketch with at most $2^\lambda$ outputs is an average-case secure sketch with entropy loss $\lambda$.
• Lemma 4.5: the sketch for transitive metric spaces (Construction 1) loses at most $\log|\Pi|-\log\Gamma-\log K$.
• §5, p. 17: at most one word within distance $t$ of $w'$ has a given syndrome.
• Theorem 5.1: the code-offset sketch is an average-case $(\mathcal F^n,m,m-(n-k)f,t)$-secure sketch; for a linear code, the syndrome sketch is deterministic, $n-k$ symbols long, with the same loss.

The extractor branch

• Lemma 2.1 and Lemma 2.4: the leftover hash lemma and its average-case generalization, $\mathbf{SD}\big((H_X(W),X,I),(U_\ell,X,I)\big)\le\frac12\sqrt{2^{-\tilde{\mathbf H}_\infty(W\mid I)}2^\ell}$.
• Lemma 4.1 (average-case form): an average-case sketch plus an average-case strong extractor gives an average-case fuzzy extractor.
• Lemma 4.3 (average-case form): with universal hashing, any $\ell\le\tilde m-2\log(1/\varepsilon)+2$ is achievable.

Significance

Theorem 5.2 says that the only costs of tolerating $t$ Hamming errors are the redundancy of the code, $(n-k)f$ bits, and the $2\log(1/\varepsilon)$ bits that any extractor loses. Appendix C of the paper shows the redundancy term cannot be avoided for uniform inputs, so for optimal codes the construction is optimal there. The average-case form matters for composition: it remains valid when the adversary holds side information correlated with the secret, which is the situation of every protocol that uses the key afterwards or reuses the reading.

Formalizing it produces machine-checked versions of the leftover hash lemma in its average-case form, the basic calculus of average min-entropy, and the code-offset and syndrome sketches. These are the standard tools of information-theoretic cryptography, used well beyond fuzzy extraction (privacy amplification, randomness extraction, information reconciliation). All results are proved in the paper; as far as is known, none of them has a formal proof in Lean or on this platform.

Difficulty

The obvious route bounds the leakage of the sketch with min-entropy and then applies an extractor to $W$ conditioned on each sketch value. That fails: conditioned on a particular sketch value, $W$ may have far less min-entropy than average, so a worst-case extractor has nothing to work with on some values, and paying for those bad values costs an extra error term (Corollary 4.2). The average-case notions exist to avoid this loss, and the chain must be kept average-case at every step. In Lean the work is in the probability bookkeeping: computing laws of pairs and triples formed by independent coin flips, rearranging them, and bounding sums of maxima over possibly infinite auxiliary types, together with the leftover hash lemma itself, which Mathlib does not provide.

Formalization scope

Random variables are their laws, Mathlib PMFs; pairs are joint laws and randomized procedures are kernels whose coins are independent of everything else. Average min-entropy is written in the equivalent joint form $-\log\sum_b\max_a\Pr[A=a\wedge B=b]$, which needs no conditioning on null events. The auxiliary variable $I$ ranges over every type, not only finite ones. Logarithms are Real.logb 2; $\{0,1\}^\ell$ is Fin ℓ → Bool; $\mathcal F^n$ is Fin n → F with Mathlib's hammingDist.

Explicit choices:

• Efficiency is dropped. Every "efficient" and polynomial-time clause (Definitions 1–5, Lemma 4.5, Theorems 5.1 and 5.2) is omitted; there is no complexity substrate, and no vacuous predicate stands in for it.
• $\ell$ is a natural number with $\ell\le m+kf-nf-2\log(1/\varepsilon)+2$ as a real inequality; the printed $\ell$ is a real expression.
• $\varepsilon>0$ is stated wherever $\log(1/\varepsilon)$ appears.
• "Min-entropy $m$" means $\mathbf H_\infty(W)\ge m$; minimum distance $2t+1$ means at least $2t+1$; $kf=\log K$, so non-linear codes are covered.
• $\mathcal F$ is any finite additive commutative group (the paper's additive cyclic group is a special case); the syndrome is any linear map onto $\mathcal F^{n-k}$ with kernel $C$.
• Extractor domains are arbitrary finite sets with arbitrary finite nonempty seed sets, instead of $\{0,1\}^n$ and $\{0,1\}^r$.
• $\Gamma$ in Lemma 4.5 is read as "for each $w$ and $b$ there are at least $\Gamma\ge1$ permutations with $\pi(w)=b$"; symmetry of the distance is an explicit hypothesis there.
• Theorem 5.1 is stated for the code-offset and syndrome constructions themselves, not as a bare existence claim.

A trivializing formalization is ruled out: the security clause quantifies over every auxiliary type and every joint law meeting the entropy bound, $\varepsilon$ and $\ell$ are constrained exactly as in the paper, and the universal hash family is constructed inside the goal (a supporting item states that universal families exist), never assumed.

Contributions welcome: proofs of any milestone; general lemmas on PMF marginals, statistical distance and average min-entropy, which are reusable across all four missions of this paper and in other information-theoretic cryptography; and the leftover hash lemma as a standalone result.

Selected references

• Y. Dodis, R. Ostrovsky, L. Reyzin, A. Smith, Fuzzy Extractors: How to Generate Strong Keys from Biometrics and Other Noisy Data, SIAM J. Comput. 38(1):97–139, 2008. arXiv:cs/0602007v4. https://arxiv.org/abs/cs/0602007 , https://doi.org/10.1137/060651380
• A. Juels, M. Wattenberg, A Fuzzy Commitment Scheme, ACM CCS 1999. https://doi.org/10.1145/319709.319714
• J. L. Carter, M. N. Wegman, Universal Classes of Hash Functions, J. Comput. System Sci. 18(2):143–154, 1979. https://doi.org/10.1016/0022-0000(79)90044-8
• J. Håstad, R. Impagliazzo, L. Levin, M. Luby, A Pseudorandom Generator from any One-way Function, SIAM J. Comput. 28(4):1364–1396, 1999. https://doi.org/10.1137/S0097539793244708
• C. H. Bennett, F. Bessette, G. Brassard, L. Salvail, J. Smolin, Experimental Quantum Cryptography, J. Cryptology 5(1):3–28, 1992. https://doi.org/10.1007/BF00191318

Motivation

Retailers often sell several variates of one product (colours, sizes or flavours of an otherwise identical item) from a fixed stock over a short season, with no replenishment. Customers substitute among the variates and the no-purchase option, so the price of one variate changes the demand for all of them, and the stock of each variate changes the value of selling the others. Dong, Kouvelis and Tian (M&SOM 2009) model this joint pricing and inventory problem with multinomial logit (MNL) choice and characterize optimal dynamic prices in closed form up to a scalar equation.

Many sellers do not price variates individually: apparel, sporting goods and airline examples are cited in the paper (Liu and Milner 2006) of unified dynamic pricing, where one price is charged for all variates and changed over time. Proposition 1 of the paper gives the optimal unified price and the optimal revenue in the same form as the paper's main result for variate-specific prices. Comparing the two quantifies how much revenue is lost by restricting to a common price, which is the purpose of the paper's §5.

Setting

There are $n$ variates, $\mathfrak n=\{1,\dots,n\}$. Variate $i$ has quality index $a_i\in\mathbb R$, the no-purchase option has utility $u_0\in\mathbb R$, $\mu>0$ is the MNL scale parameter, and in each period one customer arrives with probability $\lambda\in(0,1]$. Time $t$ counts the remaining periods, so the season runs $t=T,T-1,\dots,1$ and ends at $t=0$.

An inventory level is $x\in\mathbb N^n$. The in-stock set is $S(x)=\{i:x^i>0\}$, and $x-e^i$ is the inventory after one sale of variate $i\in S(x)$. Out-of-stock variates are not offered. At the price vector $r$, an arriving customer buys variate $i\in S(x)$ or nothing with the MNL probabilities

$$P^i(r)=\frac{e^{(a_i-r^i)/\mu}}{\sum_{j\in S(x)}e^{(a_j-r^j)/\mu}+e^{u_0/\mu}},\qquad P^0(r)=\frac{e^{u_0/\mu}}{\sum_{j\in S(x)}e^{(a_j-r^j)/\mu}+e^{u_0/\mu}}.$$

Under unified pricing the decision in each period is one price $r\ge0$ charged for every in-stock variate. The unified value function $\pi_t(x)$, the maximal expected revenue from $t$ remaining periods, satisfies $\pi_0\equiv0$ and

$$\pi_t(x)=\max_{r\ge0}\Bigl\{\lambda\sum_{i\in S(x)}rP^i+\lambda\sum_{i\in S(x)}P^i\pi_{t-1}(x-e^i)+(\lambda P^0+1-\lambda)\pi_{t-1}(x)\Bigr\},$$

with $P^i,P^0$ evaluated at $(r,\dots,r)$. Write $\Delta^i\pi_{t-1}(x)=\pi_{t-1}(x)-\pi_{t-1}(x-e^i)$ for the marginal value of a unit of variate $i$, and

$$\Delta^w\pi_{t-1}(x)=\frac{\sum_{i\in S(x)}e^{a_i/\mu}\Delta^i\pi_{t-1}(x)}{\sum_{i\in S(x)}e^{a_i/\mu}},\qquad a_w=\mu\ln\sum_{i\in S(x)}e^{a_i/\mu}.$$

Formalization targets

Goal: Proposition 1

For $t\ge1$ and $S(x)\neq\emptyset$, the equation

$$\Bigl(\frac{m}{\mu}-1\Bigr)\exp\Bigl(\frac{m+u_0}{\mu}\Bigr)=\exp\Bigl(\frac{a_w-\Delta^w\pi_{t-1}(x)}{\mu}\Bigr)$$

has a unique solution $m_t(x)$; the price

$$r^*_t(x)=\Delta^w\pi_{t-1}(x)+m_t(x)$$

is nonnegative and optimal, with $m_t(x)P^0(r^*_t)=\mu$; and

$$\pi_t(x)=\lambda\sum_{s=1}^{t}\bigl[m_s(x)-\mu\bigr],$$

where $m_s(x)$ solves the equation of period $s$ at the same inventory $x$. The statement asserts attainment of the maximum, not only a value for $\pi_t$.

Milestones

The proof in Appendix A proceeds through a one-variable problem. For marginal values $\delta_i$ let $\xi(r)=\sum_{i\in S(x)}\lambda P^i(r)(r-\delta_i)$. The milestones are: the rewriting (23)–(24) of the optimality equation as an attained $\max_{r\ge0}\xi^u_t+\pi_{t-1}(x)$; the derivatives of $P^i$, $P^0$ and $\xi$ in the common price; the first-order conditions (25)–(26) with $\xi>0$ and $0<P^0<1$ at a stationary point; the second-order condition, giving exactly one stationary point, which is the global maximizer of $\xi$ on $\mathbb R$; the formula $r=\delta_w+m$ with $m=\mu/P^0$ and the equation for $m$; uniqueness of the root of the margin equation, with root $>\mu$; and the displayed revenue sum $\pi_t(x)=\lambda\sum_{s=1}^{t}[m_s(x)-\mu]$ at the same inventory.

Significance

Proposition 1 reduces a dynamic program over a high-dimensional inventory state to a scalar root-finding problem per state and period, and gives the optimal revenue as a sum of margins. It shows that the full dynamic pricing result (Theorem 1 of the paper) survives the restriction to a common price, with the individual marginal values $\Delta^i\pi_{t-1}$ replaced by their quality-weighted average $\Delta^w\pi_{t-1}$, and the qualities replaced by the aggregate $a_w$. This is what makes the paper's numerical comparison of unified, static and full dynamic pricing in §5 computable.

The result is proved in the paper; it has not been formalized. A formalization produces a checked version of the MNL derivative calculus, of the quasiconcavity argument for the common-price objective, and of the backward induction, and it closes a step the printed proof leaves implicit: that the maximizer over all real prices is nonnegative, so that it is feasible for the constrained problem.

Difficulty

The one-period objective is not concave in the price, so neither a concavity argument nor a direct appeal to a compactness theorem gives a unique maximizer. Negativity of the second derivative at stationary points is a local statement; the existence of a stationary point and its being the global maximum on all of $\mathbb R$ do not follow from it alone.

The second difficulty is the constraint $r\ge0$. The paper solves the unconstrained problem. Showing that $\Delta^w\pi_{t-1}(x)+m_t(x)\ge0$ needs a property of the unified value function, nonnegativity of the weighted marginal value, which the paper does not state. The obvious argument, $\pi_{t-1}$ increasing in inventory term by term, does not apply verbatim when a variate leaves the in-stock set, because the choice set itself changes.

Finally, a supremum in Lean is a real number even when not attained; the value identity is only meaningful together with attainment, which the goal states explicitly.

Formalization scope

The model is one definition file, SubstitutePricing.Unified.Model: a structure with $n$, $a:\mathrm{Fin}\,n\to\mathbb R$, $u_0$, $\mu$, $\lambda$; assumptions $\mu>0$, $0<\lambda\le1$; inventories $x:\mathrm{Fin}\,n\to\mathbb N$; the in-stock set as a Finset; MNL probabilities with sums over $S(x)$ only (the paper's null price $r^i=\infty$ is modelled by removal from the choice set); and the unified value function by recursion on $t$, as a real sSup over $r\in[0,\infty)$. The equation (3) is read with the no-purchase term outside the sum over variates, as the paper's (5) and (22) use it.

Committed conventions and restrictions:

• $t\ge1$ in Proposition 1 (the printed "$t=T,\dots,0$" includes $t=0$, where $\pi_{t-1}$ does not exist).
• $S(x)\neq\emptyset$ in every statement of the dynamic program and in the static milestones that use it: for an empty in-stock set $a_w$ and $\Delta^w\pi$ involve $\ln0$ and $0/0$, and the revenue formula fails.
• The optimal margin is quantified as the unique root of its equation, and the revenue formula takes the roots of all periods $s\le t$ at the same inventory $x$.
• The goal asserts nonnegativity of $r^*_t$; the paper's proof uses but does not prove it.
• The paper's intermediate display (27) is misprinted and is not formalized; its correct consequences are.
• Milestones 2–6 concern a static objective with arbitrary marginal values $\delta$; only the goal and the recursion milestone refer to the value function.

A statement about $\pi_t$ alone, without the attainment and feasibility of $r^*_t$, would be trivially satisfiable by a junk supremum and is ruled out by the goal's form.

Infrastructure needed: derivatives of MNL probabilities, a quasiconcavity or unique-critical-point lemma for one-variable functions, a root lemma for $(m/\mu-1)e^{(m+u_0)/\mu}$, and a monotonicity property of the unified value function. The MNL derivative calculus and the root lemma are reusable for the companion missions on full dynamic pricing and mixed pricing from the same paper. Contributions on any milestone, and on the nonnegativity of $\Delta^w\pi_{t-1}$, are welcome.

Selected references

• L. Dong, P. Kouvelis, Z. Tian, Dynamic Pricing and Inventory Control of Substitute Products, Manufacturing & Service Operations Management 11(2), 317–339, 2009. https://doi.org/10.1287/msom.1080.0221
• G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1), 24–41, 1997. https://doi.org/10.1287/opre.45.1.24
• Q. Liu, J. Milner, Multiple-item dynamic pricing under a common pricing constraint, working paper, University of Toronto, 2006 (cited in the source as the motivation for unified pricing).
• S. P. Anderson, A. de Palma, J.-F. Thisse, Discrete Choice Theory of Product Differentiation, MIT Press, 1992.

Motivation

A controller of a finite Markov chain often cares about more than one long-run quantity: an inventory manager wants a high average profit while keeping the long-run fraction of stock-outs below a target; a communication network maximizes throughput subject to bounds on average delay or power. Such problems are constrained Markov decision problems: maximize one average reward while other averages, all linear in the long-run frequencies of state-action pairs, are kept below given bounds. Unlike unconstrained problems, they need not have a pure stationary optimal policy, and in general not even a stationary one.

Derman (Finite State Markovian Decision Processes, 1970, Ch. 7) treated the case in which every stationary policy induces a chain with one ergodic class, and solved it by linear programming. Derman and Veinott (1972) proposed a decomposition algorithm for the general multichain case, remarking that until the faces of the relevant polytope are known, routine use of the simplex method is not possible. Section 4.7 of Kallenberg's 1983 monograph (CWI repository) describes that polytope explicitly for the multichain case and derives from one linear program an optimal Markov policy, with conditions under which a stationary optimal policy can be read off. Kallenberg notes that Veinott knew the characterization of the polytope by 1973.

Setting

A finite Markov decision model has a finite state set $E$, for each state $i$ a finite nonempty set $A(i)$ of actions, rewards $r_{ia}$ and transition probabilities $p_{iaj}\ge0$ with $\sum_j p_{iaj}=1$. A policy $R$ chooses, at each time $t=1,2,\dots$, an action in $A(i_t)$ at random, with probabilities that may depend on the entire history $(i_1,a_1,\dots,a_{t-1},i_t)$. Special classes are the Markov policies $C_M$ (the rule at time $t$ ignores the past), the stationary policies $C_S$, written $\pi^\infty$ (one rule $\pi$, with $\pi_{ia}\ge0$ and $\sum_a\pi_{ia}=1$, at every time), and the pure stationary policies $C_D$, written $f^\infty$ with $f(i)\in A(i)$. All policies form the class $C$.

Fix an initial distribution $\beta$: $\beta_j\ge0$ and $\sum_j\beta_j=1$, with zeros allowed. The expected state-action frequencies in the first $T$ periods are

$$x^T_{ja}(R)=\frac1T\sum_{t=1}^T\sum_i\beta_i\,\mathbb P_R(X_t=j,\ Y_t=a\mid X_1=i).$$

$X(R)$ is the set of limit points of $\{x^T(R)\}_{T\ge1}$, and $C_1$ the class of policies with exactly one limit point $x(R)$. For a class $C'$, $L(C')$ collects the limit points of all $R\in C'$, giving $L$, $L(M)$, $L(C)$ (for $C_1$), $L(S)$ and $L(D)$. For a stationary $\pi$, $P(\pi)_{ij}=\sum_a p_{iaj}\pi_{ia}$, $P^*(\pi)$ is its Cesàro limit, and $x_{ja}(\pi)=[\beta^TP^*(\pi)]_j\pi_{ja}$.

The polytope $X$ is the set of $x$ for which some $y$ satisfies

$$\sum_i\sum_a(\delta_{ij}-p_{iaj})x_{ia}=0,\qquad\sum_a x_{ja}+\sum_i\sum_a(\delta_{ij}-p_{iaj})y_{ia}=\beta_j\quad(j\in E),\qquad x,y\ge0.$$

Given constraint data $q_{iak}$ and $b_k$, the constrained problem (4.7.5) is $\sup_{R\in C_1}\{\phi(\beta,R)\mid\sum_i\sum_aq_{iak}x_{ia}(R)\le b_k,\ k=1,\dots,m\}$, with $\phi(\beta,R)$ the lim inf of the average expected reward, and the linear program (4.7.6) maximizes $\sum_i\sum_ar_{ia}x_{ia}$ over $X$'s constraints together with $\sum_i\sum_aq_{iak}x_{ia}\le b_k$.

Formalization targets

Goal: Theorem 4.7.2

$$L=X.$$

Every limit point of the expected state-action frequencies of any policy lies in the polytope $X$, and every point of $X$ is such a limit point.

Milestones

• Theorem 4.7.1. $\overline{L(D)}=\overline{L(S)}=L(C)=L(M)=L$, the bar being the closed convex hull.
• Lemma 4.7.1. For $R\in C_1$, $x_{ja}(R)=\lim_{\alpha\uparrow1}(1-\alpha)\sum_{t\ge1}\alpha^{t-1}\sum_i\beta_i\mathbb P_R(X_t=j,Y_t=a\mid X_1=i)$.
• Theorem 4.7.3. Problems (4.7.5) and (4.7.6) have the same feasibility and the same optimum; an optimal policy yields an optimal $x(R)$; a Markov policy reproducing a mixture of pure stationary policies with the optimal $x$ is optimal.
• Theorems 4.7.4–4.7.5. If the stationary rule $\pi^*$ built from an optimal $(x^*,y^*)$ by (4.7.14) satisfies $x^*=x(\pi^*)$, then $(\pi^*)^\infty$ is optimal; two sufficient conditions for $x^*=x(\pi^*)$.
• Theorem 4.7.9. If $\pi\mapsto x(\pi)$ is continuous, then $X=L(S)$.
• Lemma 4.6.1 and Theorem 4.7.10. If every pure stationary policy is unichain, so is every stationary one, and then $X=L(S)$.

Significance

The goal identifies the set of achievable long-run behaviours of a multichain Markov decision process with a polytope given by $2|E|$ linear equations. Any objective and any constraints that are linear in the frequencies then become one linear program (Theorem 4.7.3), and optimal policies are recovered from its solution. This is the basis of the linear programming approach to constrained average-reward control, later developed by Altman (Constrained Markov Decision Processes, 1999) and others.

The results of this section are proved in the monograph; none has a machine-checked proof. The mission produces a formal account of state-action frequencies under history-dependent policies on a finite model, their limit points, and the multichain LP polytope. The unichain special case is related to Derman's statements posed on the platform (DermanSeqDecisions.LinProg.*, completely ergodic models); the multichain statements here are not posed elsewhere.

Difficulty

The inclusion $L\subseteq X$ needs a limit point of a history-dependent policy to satisfy the second family of equations, which involves the auxiliary vector $y$; for stationary policies $y$ comes from the deviation matrix, but a general policy has no such matrix. The reverse inclusion cannot be obtained by realizing each $x\in X$ with a stationary policy: Example 4.7.1 of the book exhibits a model where $L(S)\neq X$, and a point of $L(D)$ that is not an extreme point of $X$. The natural candidate, the stationary rule $x_{ia}/\sum_ax_{ia}$, is not defined on states with $\sum_a x_{ia}=0$, and filling in $y$ there does not in general reproduce $x$ (Theorem 4.7.5 gives conditions under which it does). In the converse direction, frequencies of general policies need not converge, so arguments must work with all limit points, not with a limit.

Formalization scope

• The model is the platform definition MarkovDecisionProcesses_AverageReward (reference item): StationaryMDP S A with finite state type S, a common finite action type A, a nonempty admissible Finset per state, rewards, and transition rows that sum to one; policies are its AvgHRPolicy, history-dependent and randomized. Frequency vectors are indexed by the admissible pairs.
• $\mathbb P_R(X_t=j,Y_t=a\mid X_1=i)$ is a finite recursive sum over histories; no measure theory is used. Lean's time index starts at $0$ (the book's $t-1$).
• $X(R)$ is the set of limits of convergent subsequences of $x^T(R)$. Policy classes are predicates that constrain only the weights of admissible actions.
• $P^*$ is the limUnder of the Cesàro means $\frac1n\sum_{k=1}^nP^k$; its existence is the book's Theorem 2.4.1(i) and is not assumed as a hypothesis.
• $\beta$ is a probability vector with zeros allowed; $\beta\gg0$ is never assumed.
• The optima in Theorem 4.7.3 are compared in the extended reals, so the infeasible case reads $-\infty=-\infty$.
• "One ergodic set" is the platform's IsUnichainMatrix (any two recurrent states communicate); Assumption 4.7.1 is IsUnichain.
• Trivializing formalization ruled out: $L$ ranges over all history-dependent randomized policies. Restricting it to stationary policies would replace $L$ by $L(S)$, for which $L(S)=X$ fails in general.

A complete development needs Cesàro limits of stochastic matrices (Theorem 2.4.1), the stationary-policy correspondence of §4.3, a separating hyperplane in finite dimension, and the Derman–Strauch construction of a Markov policy matching a mixture of policies (Theorem 2.5.1). The frequency and limit-point infrastructure is reusable for any average-reward model on a finite state space. Proofs of any milestone, and of the auxiliary facts above as separate theorems, are welcome.

Selected references

• L.C.M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. https://ir.cwi.nl/pub/13008
• C. Derman, Finite State Markovian Decision Processes, Academic Press, New York, 1970.
• C. Derman and A.F. Veinott, Constrained Markov decision chains, Management Science 19 (1972), 389–390. https://doi.org/10.1287/mnsc.19.4.389
• C. Derman and R.E. Strauch, A note on memoryless rules for controlling sequential control problems, Annals of Mathematical Statistics 37 (1966), 276–278. https://doi.org/10.1214/aoms/1177699617
• E. Altman, Constrained Markov Decision Processes, Chapman & Hall/CRC, 1999. https://doi.org/10.1201/9781315140223

Motivation

Martingale inequalities compare what a fluctuating process does along a path with how large its successive increments are. Such estimates are used in probability and harmonic analysis because a martingale can represent information revealed step by step, while its square function measures accumulated fluctuation. In his 1973 Wald Memorial Lectures, Burkholder developed distribution function inequalities that cover many choices of size measure at once, extending the power norm comparisons treated earlier in the paper. Burkholder, 1973

The target of this mission is Theorem 15.1 of that paper: a two sided comparison for every convex function of moderate growth. The paper attributes the decomposition of a martingale into small and large jumps to Davis, and cites a convex comparison lemma introduced in earlier work and subsequently treated by Garsia and Neveu. These attributions matter to the scope of the mission: the decomposition and lemma are separate, named milestones, while Burkholder's printed two sided inequality is the goal. Burkholder, 1973, §§14–16

Setting

Work on a probability space $(\Omega,\mathcal A,P)$ with an increasing sequence of sub sigma fields $\mathcal A_0,\mathcal A_1,\ldots$. A real martingale $f=(f_1,f_2,\ldots)$ is observed from time $1$ onward. Following the paper, put $f_0=0$ in the formulas for its differences: $d_1=f_1$ and $d_k=f_k-f_{k-1}$ for $k\ge2$. This convention differs from the index zero value required for a Lean martingale, which is discussed below.

The square function $S(f)$ and maximal function $f^*$ are pathwise quantities:

$$S(f)=\left(\sum_{k=1}^{\infty}d_k^2\right)^{1/2}, \qquad f^*=\sup_{k\ge1}|f_k|.$$

Either quantity can be infinite. Their finite versions stop at $n$: $S_n(f)$ sums the first $n$ squared differences, and $f_n^*$ takes the maximum through time $n$. For a positive exponent $p$, the paper writes $\|f\|_p=\sup_{n\ge1}(E|f_n|^p)^{1/p}$. The notation $E\Phi(Y)$ means the expectation of a nonnegative transform of a nonnegative random variable $Y$.

A function of moderate growth is a nondecreasing continuous $\Phi:[0,\infty]\to[0,\infty]$ with $\Phi(0)=0$ and

$$\Phi(2x)\le c_{(6.1)}\Phi(x)\qquad(x>0)$$

for some nonnegative growth constant $c_{(6.1)}$. The target adds convexity on finite nonnegative arguments. The examples $\Phi(x)=x$ and $\Phi(x)=x^p$ for $p\ge1$ satisfy these conditions. The paper sets aside $\Phi\equiv0$ as trivial; the Lean statements allow it because every displayed comparison still holds.

Formalization targets

The two sided convex comparison

The goal is precisely the form printed as Theorem 15.1:

$$C_1 E\Phi(S(f))\le E\Phi(f^*)\le C_2 E\Phi(S(f)), \qquad C_1,C_2>0.$$

The constants depend only on $c_{(6.1)}$, and are uniform over the probability space, filtration, martingale, and particular choice of $\Phi$ with that growth bound. The statement includes both sides; the paper writes a proof for the right side and says the left side follows by the same pattern. No integrability or boundedness is imposed on $f$ or on the two expectations. Burkholder, 1973, Theorem 15.1, pp. 33–34

Supporting statements

The milestones record the paper's good $\lambda$ lemma, Doob's cited maximal estimate, the predictable jump inequalities of §12, the quasi subadditivity of $\Phi$, Davis's decomposition and its jump bounds, and the convexity lemma of §16. The latter compares a sum of nonnegative random variables with the sum of their conditional expectations. Its two Neveu statements are retained as cited intermediate targets. These results identify distinct mathematical interfaces that a solver can formalize and reuse; the milestone text is transcribed from the indicated pages of the article.

Significance

The theorem lets one replace the expected convex transform of a path's maximum by the expected transform of its quadratic fluctuation, up to constants controlled by a single growth parameter. Choosing $\Phi(x)=x$ recovers the $L^1$ comparison displayed after Davis's decomposition; choosing a convex power gives the $p\ge1$ power cases. The assertion is useful even when one or both expectations are infinite, because it gives a uniform relation across the whole class of admissible martingales and functions. Burkholder, 1973, §§14–15

The result is proved in the paper. This mission asks for a machine checked Lean proof of the known theorem and of the selected statements that support it. The definitions for square and maximal functions, moderate growth, and nonnegative conditional projections can be reused in other martingale comparisons. A previously posed platform theorem about Robbins–Monro noise sums has the shape of one power function instance, but its process and time window differ; it does not supply this general result.

Difficulty

The size of a single martingale increment can dominate both a maximum and a square function. A direct comparison of the two pathwise expressions therefore gives no uniform expectation bound for arbitrary martingales and convex $\Phi$. The §12 estimates require predictable control of jumps, while the target has no such hypothesis. Davis's decomposition exposes the small and large jump contributions as different objects, and the §16 convexity lemma is needed to compare the conditional terms arising from large jumps. Convexity is essential for that lemma and for Theorem 15.1; the §12 good $\lambda$ statements themselves assume only moderate growth. Burkholder, 1973, §§12, 14–16

Formalization scope

Lean uses Mathlib's Martingale f ℱ P for a process indexed by natural numbers. The article begins at $1$ and uses $f_0=0$ only in its difference formulas. The definitions of $d_k$, $S(f)$, $f^*$, and $\|f\|_p$ therefore read positive indices and insert zero in the article's formulas; Lean's actual $f(0)$ is the compatible conditional expectation extension needed by Mathlib. Davis's partial sums also begin at $1$, and the decomposition theorem specifies the index zero extensions for its two martingales.

The square function, maximal function, $L^p$ norm, and all nonnegative expectations take values in $[0,\infty]$. This retains unbounded sample paths and nonintegrable expectations. For a nonnegative variable $z_k$, $E(z_k\mid\mathcal A_{k-1})$ is the extended conditional expectation condLExp, so a nonintegrable $z_k$ cannot silently become zero. Davis's signed $y_k$ is integrable, so its real conditional expectation uses Mathlib's ordinary conditional expectation. Predictable bounds such as $|d_k|\le w_k$ and the resulting claims are stated almost everywhere at each positive index.

The Lean predicate for moderate growth states the doubling law at zero and infinity as well as positive finite $x$; zero is automatic from $\Phi(0)=0$, and the endpoint at infinity follows by continuity in the nontrivial case. Convexity is read from finite real arguments. The zero function is included. A valid formalization must retain both inequalities in the goal and choose its constants before the martingale and $\Phi$; choosing constants after the data would make the goal much weaker.

The development needs finite and infinite square function sums, maximal functions, stopping and tail events, Mathlib martingales, conditional expectations, and convexity on the nonnegative reals. Contributions proving or improving any of the named milestones are welcome, including independent proofs of the cited Doob and Neveu statements. No extra boundedness or integrability assumption should be inserted into the goal to simplify a proof.

Selected references

• D. L. Burkholder, Distribution Function Inequalities for Martingales, The Annals of Probability 1(1), 1973, pp. 19–42. DOI.

Motivation

A probability forecast is useful only when its stated frequencies bear a stable relation to outcomes. If a forecaster repeatedly announces a 70% chance of rain, calibration asks whether rain occurs on about 70% of those days. This is a minimal reliability requirement for probabilistic prediction, even though calibration alone does not rank every pair of forecasts by usefulness. Foster and Vohra study the difficulty of obtaining this property when the weather sequence is chosen in response to a forecaster's past behavior. A deterministic rule can be forced into a persistent calibration error; the article shows how randomized forecasts evade that obstruction when Nature sees past forecasts but cannot see the current random draw. Foster and Vohra, 1998.

The work sits at an intersection of sequential probability forecasting and repeated games. Its opponent can adapt to the whole observed history, including the forecaster's earlier random outcomes. The simultaneity of each round matters: before choosing that round's wet or dry outcome, Nature knows the distribution of the next forecast but not which forecast is realized. The paper's main result is about a specified forecasting rule constructed from regret balances, rather than merely the existence of some successful randomized strategy. Foster and Vohra, 1998, §§3, 5.

Timeline. Dawid (1982) proposed calibration as a criterion for sequential probability forecasts and showed that a coherent Bayesian expects to be calibrated (doi). Oakes (1985), with Dawid's accompanying comment, showed that no deterministic forecaster is calibrated against every outcome sequence: Nature may rain exactly when the forecast is at most $1/2$ (doi). Foster and Vohra circulated the present randomized construction from 1994 (received August 1994, published 1998); their 1997 Games and Economic Behavior paper used a calibrated forecaster built on the same pairwise-regret flow equations to reach correlated equilibria (doi). Hart and Mas-Colell (2000) later turned the same internal-regret quantities into regret matching (doi).

Setting

At round $s$, the outcome $X_s$ is $1$ for wet and $0$ for dry. The forecaster selects a probability from the finite grid $G_k=\{0,1/k,\ldots,1\}$, where $k$ is a positive integer. A forecast $p$ is represented by the binary probability vector $(1-p,p)$; the second coordinate is the forecast chance of rain. The forecaster chooses $i/k$ with probability $\mu_s^i$. The Brier loss of that possible forecast is $L_s^i=(X_s-i/k)^2$.

After $t$ rounds, $n_t(p)$ counts the realized forecasts equal to $p$, and $\rho_t(p)$ is the observed fraction of wet outcomes on those rounds. The quadratic calibration score is

$$C_t=\sum_{p\in G_k}\frac{n_t(p)}{t}\bigl(\rho_t(p)-p\bigr)^2.$$

A forecast never issued has zero count and contributes zero. The paper also uses a weighted calibration score $\widetilde C_t$, in which the realized indicator that $i/k$ was chosen is replaced by its conditional probability $\mu_s^i$. Its weighted count is $\widetilde n_t(i/k)=\sum_{s<t}\mu_s^i$, and its weighted wet frequency is $\widetilde\rho_t(i/k)=\sum_{s<t}\mu_s^i X_s/\widetilde n_t(i/k)$ when the denominator is positive.

For grid points $i/k$ and $j/k$, the pairwise regret $R_t^{i\to j}$ is the positive part of the cumulative weighted reduction in Brier loss that would result from replacing $i/k$ by $j/k$ on rounds weighted by $\mu_s^i$. The algorithm chooses its next distribution so that the regret flow out of each $i$ equals the flow into $i$:

$$\mu_s^i\sum_j R_{s-1}^{i\to j} =\sum_j\mu_s^j R_{s-1}^{j\to i}.$$

These equations use only regret from previous rounds. They specify a distribution after every possible history, including histories created by Nature's adaptive choices. Foster and Vohra, 1998, §5.

Formalization targets

Main theorem

The target is Theorem 1: for every $\varepsilon>0$, choose $k\ge1/\varepsilon^2$ and let the forecaster follow the regret-flow equations. Against every adaptive Nature, the realized score eventually satisfies

$$\Pr\{C_t<\varepsilon\}>1-\varepsilon.$$

The time after which the inequality holds may depend on the forecaster, Nature, and $\varepsilon$. The statement fixes the algorithm and the grid scale; a general existence theorem would leave out its central content. Foster and Vohra, 1998, Theorem 1 and §6 Corollary.

Supporting targets

The milestones record the source's attack path: solvability of the flow equations, a history-adapted forecaster satisfying them, the counting-process bounds and convergence of $C_t-\widetilde C_t$ in probability, the algebraic link between calibration and regret, the bound on the smoothed regret potential, and the deterministic bound on $\widetilde C_t$. Theorem 3's last constant is written as $(k+1)/(2\delta)$ and the corollary's horizon as $8k^2/\varepsilon^2$; the printed constants are inconsistent with the paper's $k+1$ grid points and its derived rate, respectively. The provenance and corrections are recorded with those milestones. Foster and Vohra, 1998, §6.

Significance

The result gives a concrete randomized forecaster whose realized empirical frequencies remain reliable even when outcomes react to past forecasts. The game model includes fixed outcome sequences as a special case, but its adaptive Nature can condition future choices on every earlier realized forecast and outcome. The theorem therefore identifies a particular sequential rule, its finite forecast grid, and the information boundary under which its guarantee holds. Foster and Vohra, 1998, §§3, 5–6.

The published Foster–Vohra 1997 formalization already supplies reusable definitions of finite probability vectors, history laws, pairwise regret, and calibration scores, together with a proved finite flow-conservation theorem. This mission extends that substrate to the 1998 paper's Brier-loss grid algorithm. Theorem 1 and its supporting results are proved on paper but not yet formalized; the earlier formal existence theorem for some calibrated forecaster does not establish this algorithm's guarantee, which is the content of the goal.

Difficulty

The weighted score $\widetilde C_t$ is controlled by quantities known from the chosen mixtures, while $C_t$ depends on the actual random draws. A direct deterministic bound on $C_t$ therefore does not follow from the regret equations. The gap requires a quantitative comparison of realized counts and weighted counts under an adaptive history law, followed by a passage from those count errors to the nonlinear calibration score. The regret itself has a positive-part kink, so its aggregate bound is stated through the paper's smoothed potential. Foster and Vohra, 1998, §6.

Formalization scope

The Lean model uses binary outcomes, $k+1$ grid indices Fin (k + 1), and histories ordered from oldest to newest. Rounds start at index $0$: the paper's $R_{s-1}$ in round $s$ is the regret over the preceding $s$ indices. Forecast and outcome are drawn independently conditional on the past by the published histLaw; Nature is any map from complete past histories to a probability distribution on the two outcomes. The forecast rule is likewise a map from histories to grid distributions. For each earlier round it reads only that round's prefix, so the current outcome cannot influence its mixture.

The goal uses the realized quadratic score calibScore2Hj h 1, whose second vector coordinate is the wet probability. The map $i\mapsto(1-i/k,i/k)$ is injective for $k>0$. The weighted score is a separate definition used in supporting results. A forecaster satisfying the flow equations is shown to exist by a milestone, so the goal's algorithm hypothesis has content. The statement covers adaptive Nature; replacing Nature by a fixed sequence or replacing $C_t$ by $\widetilde C_t$ would change the claim.

Every theorem requiring the grid has the explicit $k>0$ condition. Deterministic calibration bounds assume binary outcomes and probability-vector weights; the history-law theorems obtain these properties from Fin 2 and PMF. When a weighted count is zero, Lean's division convention gives weighted wet frequency $0$; nonnegative weights make its numerator zero as well. At horizon $0$, the weighted calibration score is $0$. The probability event is measured with the history law's outer measure in $\mathbb R_{\ge0}\cup\{\infty\}$. Reusable work includes finite-history martingale estimates, weighted calibration comparisons, and finite regret-potential bounds.

Selected references

• D. P. Foster and R. V. Vohra, Asymptotic calibration, Biometrika 85(2):379–390, 1998. DOI: 10.1093/biomet/85.2.379.
• A. P. Dawid, The well-calibrated Bayesian, Journal of the American Statistical Association 77:605–613, 1982. DOI: 10.1080/01621459.1982.10477856.
• D. Oakes, Self-calibrating priors do not exist, Journal of the American Statistical Association 80:339, 1985, with comments by A. P. Dawid (pp. 340–341) and M. Schervish (pp. 341–342). DOI: 10.1080/01621459.1985.10478117.
• D. P. Foster and R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21:40–55, 1997. DOI: 10.1006/game.1997.0595.
• D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific Journal of Mathematics 6:1–8, 1956. DOI: 10.2140/pjm.1956.6.1.
• S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68:1127–1150, 2000. DOI: 10.1111/1468-0262.00153.