All missions

Motivation

The residual life time of a lifetime $X$ at age $t$ is the excess $X - t$ given survival, $X > t$. How it behaves at great ages is a question in reliability (remaining life of an item that has already lasted long), in insurance and demography (remaining life at old age), and in the peaks-over-threshold method of extreme value statistics, where exceedances over a high threshold are modelled by a generalized Pareto law.

Balkema and de Haan (Residual Life Time at Great Age, Ann. Probab. 2 (1974) 792–804) determined every possible limit law of the suitably normed residual life as $t \to \infty$, and their domains of attraction. For continuous limits, the classical sufficient conditions are von Mises' conditions (1936) on the derivative of $(1 - F)/F'$. Section 4 of the paper goes further: it gives inequalities that hold at every finite age $t \ge t_0$, not only in the limit. This mission formalizes that finite-$t$ result, the Corollary to Theorem 7.

Timeline: von Mises (1936) gives sufficient conditions for domains of attraction of extreme value laws; Balkema and de Haan (1974) prove the limit theorems for residual life and the finite-$t$ bounds formalized here; Pickands (1975, Ann. Statist. 3, 119–131) proves the corresponding approximation by the generalized Pareto law for excesses, the result now known as the Pickands–Balkema–de Haan theorem.

Setting

Let $X$ be a real random variable with distribution function $F$. The residual life distribution function at age $t$ is

$$F_t(x) = P\{X - t \le x \mid X > t\}.$$

Assume $F$ has a positive, differentiable density $F'$ for $t \ge t_0$, and define the norming function

$$a(t) = \frac{1 - F(t)}{F'(t)} \qquad (t \ge t_0),$$

the reciprocal of the hazard rate. The normed residual life is $(X - t)/a(t)$ given $X > t$, with distribution function $P\{(X - t)/a(t) \le x \mid X > t\} = F_t(x\,a(t))$.

The comparison laws are the distribution functions $\Pi_{0,c}$, $c \in \mathbb R$, all vanishing for $x < 0$:

• for $c > 0$, $\Pi_{0,c}(x) = 1 - (1 + cx)^{-1/c}$ for $x \ge 0$ (a generalized Pareto law);
• for $c = 0$, $\Pi_{0,0}(x) = \Pi(x) = 1 - e^{-x}$ for $x \ge 0$ (the exponential law);
• for $c < 0$, $\Pi_{0,c}(x) = 1 - (1 + cx)^{-1/c}$ for $0 \le x \le |c|^{-1}$, and $1$ beyond (bounded support).

Formalization targets

Goal: the Corollary to Theorem 7

If $c \ge 0$ and $\varepsilon \ge 0$ satisfy $|c - a'(t)| \le \varepsilon$ for $t \ge t_0$, then

$$\left|\Pi_{0,c}(x) - P\left\{\frac{X - t}{a(t)} \le x \,\middle|\, X > t\right\}\right| \le \varepsilon \qquad \text{for all } x \text{ and all } t \ge t_0 .$$

Milestones

1. The bounds (13): if $c_1 \le a' \le c_2$ on $[t_0, \infty)$, then $1 + c_1 x \le a(t + x a(t))/a(t) \le 1 + c_2 x$ for $t \ge t_0$, $x \ge 0$.
2. The exponential representation

$$P\left\{\frac{X - t}{a(t)} > x \,\middle|\, X > t\right\} = \frac{1 - F(t + x a(t))}{1 - F(t)} = \exp\left(-\int_0^x \frac{a(t)}{a(t + s a(t))}\, ds\right).$$

3. Theorem 7: if $c_1 \le a'(t) \le c_2$ for $t \ge t_0$, then

$$\Pi_{0,c_2}(x) \le P\left\{\frac{X - t}{a(t)} \le x \,\middle|\, X > t\right\} \le \Pi_{0,c_1}(x) \qquad (t \ge t_0,\ x \in \mathbb R).$$

4. $\sigma(u) = u^{-2}(e^{-u} - 1 + u) = \int_0^1\int_0^t e^{-us}\,ds\,dt$ is positive and decreasing.
5. Lemma 4: $0 \le -(\partial/\partial c)\Pi_{0,c}(x) < 1$ for $c > -1$, $x \ne 0$, $cx \ne -1$.
6. $|\Pi_{0,c}(x) - \Pi_{0,c_0}(x)| \le |c - c_0|$ for $c \ge 0$ and all real $c_0$, $x$.

The goal is the Corollary because it is the paper's final statement of Section 4: a single parameter $c$ and a single error $\varepsilon$, with no limit taken. Theorem 7 is the stronger two-parameter sandwich it rests on.

Significance

The result. Theorem 7 and its Corollary are a quantitative, non-asymptotic form of the von Mises condition $\frac{d}{dt}\frac{1-F(t)}{F'(t)} \to c$. If the derivative of the reciprocal hazard stays within $\varepsilon$ of $c$ from age $t_0$ on, then at every such age the normed excess distribution is uniformly within $\varepsilon$ of the generalized Pareto (or exponential) law $\Pi_{0,c}$. Letting $\varepsilon \to 0$ along $t_0 \to \infty$ recovers convergence to $\Pi_{0,c}$, and the bound itself quantifies the error of the generalized Pareto approximation used in threshold-exceedance modelling.

Formalizing it. The result is proved in the paper (1974), with short proofs. To our knowledge no part of it has a machine-checked proof. The mission produces checked versions of the theorem, the corollary and the elementary lemmas about the family $\Pi_{0,c}$: its monotonicity and Lipschitz dependence on the parameter $c$, including across the case change at $c = 0$. Those facts about the generalized Pareto family are reusable in any formal development of extreme value statistics.

Difficulty

The analytic content is elementary, but several steps hide case analysis. The Lipschitz bound in $c$ requires the derivative of $\Pi_{0,c}(x)$ in $c$ across $c = 0$, where the formula changes from $1 - (1+cx)^{-1/c}$ to $1 - e^{-x}$, and across the boundary $cx = -1$ of the support when $c < 0$, where the function is not differentiable. The bound $-\partial_c \Pi_{0,c} < 1$ is not a crude estimate: it reduces to the comparison $\sigma(u) < \sigma(-\psi)$ for the function $\sigma(u) = u^{-2}(e^{-u} - 1 + u)$, which needs its strict monotonicity on all of $\mathbb R$, including $u = 0$ where the closed form is undefined. In Theorem 7 the lower bound $1 + c_1 x$ in (13) becomes negative for $c_1 < 0$ and large $x$; this is exactly where the comparison law $\Pi_{0,c_1}$ reaches $1$, and the argument must handle it. The orientation is easy to get wrong: the upper bound $c_2$ on the derivative gives the lower bound $\Pi_{0,c_2}$, since $\Pi_{0,c}(x)$ decreases in $c$.

Formalization scope

The source is the published Annals of Probability article (DOI 10.1214/aop/1176996548); page numbers are the journal's.

• The law of $X$ is a probability measure μ on ℝ, $F$ is Mathlib's cdf μ, and $F_t(x) = \mu((t, t+x]) / \mu((t, \infty))$. The normed probability $P\{(X-t)/a(t) \le x \mid X > t\}$ is $F_t(x\,a(t))$.
• "Positive, differentiable density for $t \ge t_0$" is: for $t \ge t_0$, cdf μ has derivative $f(t) > 0$ and $f$ has derivative $f'(t)$, both within $[t_0, \infty)$; nothing is assumed to the left of $t_0$.
• The derivative $\frac{d}{dt}a(t)$ is a named function $a'$ with HasDerivWithinAt on $[t_0, \infty)$; it is the derivative the density hypothesis already provides, so this adds no assumption. Bare deriv is not used.
• Completion of $\Pi_{0,c}$ for $c < 0$. The paper (p. 801) prints the formula only for $0 \le x \le |c|^{-1}$. The formalization sets $\Pi_{0,c}(x) = 1$ for $x > |c|^{-1}$, as "distribution function" requires and as the proof of Lemma 4 uses ("$\Pi_{0,c}(x)$ is constant on both components of $\{c > -1\}\setminus R$"). The formula gives $1$ at $x = |c|^{-1}$, so the completion is continuous.
• $\Pi_{0,0}$ is a separate branch ($1 - e^{-x}$), not the formula with $1/0$.
• $\sigma$ is defined as $\int_0^1\int_0^t e^{-us}\,ds\,dt$, and the closed form $u^{-2}(e^{-u} - 1 + u)$ for $u \ne 0$ is part of milestone 4. "Decreasing" is stated as strictly decreasing, which is what the proof of Lemma 4 uses ($\sigma(u) < \sigma(-\psi)$).
• Lemma 4 states the differentiability of $c \mapsto \Pi_{0,c}(x)$ at $c$ together with the bound $0 \le -d < 1$ on its derivative $d$.
• The bounds (13) are stated in both printed forms.
• No sign condition is added on $c_1, c_2$ in Theorem 7; $c_1$ may be any real number, and $c - \varepsilon$ in the Corollary may be negative.

A trivializing formalization is ruled out: the conclusion is a bound at every real $x$ and every $t \ge t_0$ with $a(t) > 0$, the conditional probability divides by $\mu((t,\infty)) > 0$ (which the density hypothesis implies), and the hypotheses are satisfied by, for example, the exponential law ($a \equiv 1$, $c = 0$) and the Pareto law $1 - (1+x)^{-\alpha}$ ($a(t) = (1+t)/\alpha$, $c = 1/\alpha$).

A complete development needs the fundamental theorem of calculus with one-sided derivatives, a change of variables in interval integrals, and calculus of Real.rpow in the exponent parameter. The lemmas on $\Pi_{0,c}$ and $\sigma$ are reusable beyond this mission; proofs of any milestone are welcome independently.

Selected references

• A. A. Balkema, L. de Haan, Residual Life Time at Great Age, The Annals of Probability 2 (1974), no. 5, 792–804. https://doi.org/10.1214/aop/1176996548
• R. von Mises, La distribution de la plus grande de n valeurs, Revue Mathématique de l'Union Interbalkanique 1 (1936), 141–160.
• J. Pickands III, Statistical Inference Using Extreme Order Statistics, The Annals of Statistics 3 (1975), no. 1, 119–131. https://doi.org/10.1214/aos/1176343003
• L. de Haan, On Regular Variation and Its Application to the Weak Convergence of Sample Extremes, Mathematical Centre Tracts 32, Amsterdam, 1970.

Motivation

Many stochastic models produce a stationary quantity $R$ that solves a random equation $R \overset{d}{=} \Psi(R)$, with $\Psi$ a random map independent of $R$. The random difference equation $R \overset{d}{=} Q + MR$ (perpetuities in insurance and finance, the ARCH and GARCH volatility models, random walks in random environments), the Lindley equation $S \overset{d}{=} (X+S)^+$ of queueing theory, and the random recurrences behind probabilistic analyses of algorithms are all of this form. In these models the law of $R$ is rarely explicit, while the decay of its tail $P(R>t)$ is what governs ruin probabilities, extreme values and buffer overflows.

Kesten (1973) showed that the stationary solution of $R \overset{d}{=} Q + MR$ has a power-law tail when $E|M|^\kappa = 1$ for some $\kappa>0$, by a long argument specific to that equation. Goldie (1991) separated the renewal-theoretic core of the phenomenon from the particular equation: the implicit renewal theorem (Theorem 2.3) gives the power-law tail of any random variable $R$ whose tails are comparable to those of $MR$, with an explicit formula for the constant. Kesten's theorem and the tail results for several other random equations then follow by checking one integrability condition. The theorem is the standard entry point to the subject, reproduced in the monograph of Buraczewski, Damek and Mikosch (2016).

Timeline:

• Kesten (1973): power tails for multivariate random difference equations, including the one-dimensional case $R \overset{d}{=} Q+MR$.
• Grincevičius (1975, 1981): limit laws for random walks on the line and the random difference equation $R \overset{d}{=} Q+MR$ in one dimension (Lithuanian Math. J. 15, 21).
• Goldie (1991): the implicit renewal theorem for arbitrary $R$, explicit constants, rates of convergence, and applications to several random equations.

Setting

Let $(\Omega,\mathcal A,P)$ be a probability space and $M$, $R$ two independent real random variables. No equation is assumed for $R$.

A probability law on $\mathbb R$ is arithmetic if it is concentrated on a lattice $\{n\lambda:n\in\mathbb Z\}$ for some $\lambda>0$, and nonarithmetic otherwise. Fix $\kappa>0$. The Cramér-type conditions on $M$ are

$$E|M|^\kappa = 1,\qquad E|M|^\kappa\log^+|M|<\infty,\qquad \text{the law of }\log|M|\text{ given }M\ne0\text{ is nonarithmetic.}$$

Under them, $m := E|M|^\kappa\log|M|$ is finite and positive (Lemma 2.2), with $0^a\log 0 := 0$.

The tails of $R$ enter through two tail-comparison conditions

$$\text{(2.8)}\ \int_0^\infty|P(R>t)-P(MR>t)|\,t^{\kappa-1}dt<\infty,\qquad \text{(2.9)}\ \int_0^\infty|P(R<-t)-P(MR<-t)|\,t^{\kappa-1}dt<\infty ,$$

and the constants

$$C_\pm=\frac1m\int_0^\infty\bigl(P(\pm R>t)-P(\pm MR>t)\bigr)t^{\kappa-1}dt, \qquad C=\frac1{2m}\int_0^\infty\bigl(P(|R|>t)-P(|MR|>t)\bigr)t^{\kappa-1}dt .$$

In the Lean development these are CramerConditions κ (P.map M), cramerMean, TailCondPlus, TailCondMinus, Cplus, Cminus and Ctwo, in the namespace GoldieRenewal.Implicit.

Formalization targets

Goal: Theorem 2.3

Let $M$ satisfy the Cramér-type conditions and let $R$ be independent of $M$.

Case 1 ($M\ge0$ a.s.): (2.8) implies $P(R>t)\sim C_+t^{-\kappa}$, and (2.9) implies $P(R<-t)\sim C_-t^{-\kappa}$, as $t\to\infty$.

Case 2 ($P(M<0)>0$): (2.8) and (2.9) together imply

$$t^\kappa P(R>t)\to C,\qquad t^\kappa P(R<-t)\to C,\qquad t\to\infty .$$

The relation $P(R>t)\sim C_+t^{-\kappa}$ means $t^\kappa P(R>t)\to C_+$, including $C_+=0$.

Milestones

Lemma 2.2 (negative drift of $\log|M|$, $m\in(0,\infty)$); Lemmas 9.1–9.2 (smoothed integrable functions are directly Riemann-integrable); Lemma 9.3 (a Tauberian step from averaged to pointwise tails); the renewal equation (9.8) $\check r=\check g_1*\nu$ and its key-renewal limit in Case 1; the Case 2a step law (9.11) with mean $2m$ and nonarithmetic (9.12)–(9.13), and the renewal identity (9.15); the reduction (9.16) of Case 2b to Case 1.

Significance

The theorem turns a question about an unknown law into a question about integrability. For a random equation $R\overset{d}{=}\Psi(R)$ it suffices to compare $\Psi(R)$ with $MR$, which is often a moment computation; this yields power tails, with constants given by expectations, for perpetuities, Lindley-type equations, random polynomial and maximum equations (Goldie 1991, §§4–8). The explicit constant also decides when the tail is genuinely of order $t^{-\kappa}$: the theorem has content only when $E|R|^\kappa=\infty$, since otherwise $C_++C_-=0$.

The theorem has been proved for thirty years; it is not formalized in any proof assistant known to the mission. A formal development would provide reusable infrastructure absent from Mathlib: direct Riemann integrability, renewal measures of walks on the whole line, the two-sided key renewal theorem (Athreya, McDonald and Ney 1978), and a Tauberian lemma for monotone tails. The sibling missions on Kesten's theorem and on rates of convergence are built on the same setting.

Difficulty

The obvious argument writes $P(R>t)$ as a telescoping sum along the multiplicative walk $\Pi_n=M_1\cdots M_n$ and applies the key renewal theorem to the result. It fails at three points. First, the function the key renewal theorem would be applied to, $g_1(t)=e^{\kappa t}(P(R>e^t)-P(MR>e^t))$, is only integrable under (2.8), not directly Riemann-integrable, and the key renewal theorem is false for general integrable functions; so no conclusion about $P(R>t)$ itself follows directly. Second, when $M$ takes both signs, $\log|\Pi_n|$ alone is not a random walk that controls $P(\Pi_nR>e^t)$: the sign of $\Pi_n$ decides which tail of $R$ is involved, so the walk is Markov-modulated. Third, the walk lives on the whole line and may jump to $-\infty$ (when $P(M=0)>0$), so renewal theory on $[0,\infty)$, the version in most textbooks, does not apply.

Formalization scope

• One probability space with IsProbabilityMeasure P; M, R measurable real random variables; independence is IndepFun R M P. In (9.16) the copy $M'$ lives on the same space, with IdentDistrib M' M P P and iIndepFun of $(R,M,M')$.
• Cramér conditions are stated on the law P.map M; the moments are lower Lebesgue integrals in $[0,\infty]$. The conditional law in (2.5) conditions on $\{x\neq0\}$ before taking $\log|x|$, so Lean's Real.log 0 = 0 never enters; $E\log|M|$ is an extended real with $\log 0=-\infty$.
• Tails are real numbers P.real {ω | t < R ω} with the paper's strict inequalities. (2.8), (2.9) are IntegrableOn … (Set.Ioi 0); the constants are Bochner integrals, used only under the corresponding integrability hypothesis.
• "$\sim$" is Tendsto (fun t => t ^ κ * P.real {…}) atTop (𝓝 C).
• Direct Riemann integrability follows Feller (1971, §XI.1), with suprema in $[0,\infty]$. The smoothing is $\check f(t)=\int_{-\infty}^t e^{-(t-u)}f(u)\,du$.
• The tilted law $\eta$, its renewal measure and the Case 2a laws are defined from the law of $M$; no i.i.d. sequence appears in a statement.

Three formalizations would trivialize the goal and are excluded: reading "$\sim$" as a ratio $P(R>t)/(C_+t^{-\kappa})\to1$ (which is false when $C_+=0$); assuming $E|R|^\kappa<\infty$ (which forces $C_++C_-=0$); and placing a key-renewal-theorem conclusion among the hypotheses.

Contributions welcome: proofs of any milestone; a general two-sided key renewal theorem for nonarithmetic laws with positive mean (reusable beyond this mission); Mathlib-quality lemmas on direct Riemann integrability and renewal measures.

Selected references

• C. M. Goldie, Implicit renewal theory and tails of solutions of random equations, Ann. Appl. Probab. 1(1):126–166, 1991. https://doi.org/10.1214/aoap/1177005985
• H. Kesten, Random difference equations and renewal theory for products of random matrices, Acta Math. 131:207–248, 1973. https://doi.org/10.1007/BF02392040
• K. B. Athreya, D. McDonald, P. Ney, Limit theorems for semi-Markov processes and renewal theory for Markov chains, Ann. Probab. 6(5):788–797, 1978. https://doi.org/10.1214/aop/1176995429
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. II, 2nd ed., Wiley, 1971.
• D. Buraczewski, E. Damek, T. Mikosch, Stochastic Models with Power-Law Tails: The Equation X = AX + B, Springer, 2016. https://doi.org/10.1007/978-3-319-29679-1

Motivation

Many operators of harmonic analysis are bounded on $L^2$ by an orthogonality argument but fail to be bounded on $L^1$; what survives at $p=1$ is a weak-type estimate $\lambda\,P(|Tf|>\lambda)\le c\,\|f\|_1$. For singular integrals the standard route to such an estimate is the Calderón–Zygmund decomposition, which splits a function at height $\lambda$ into a bounded part and a part supported on a small set. Martingale theory has the same need: square functions, martingale transforms and maximal operators of martingales are bounded on $L^2$ for orthogonality reasons, and their behaviour on $L^1$-bounded martingales is the delicate endpoint.

R. F. Gundy (1968) supplied the martingale analogue: an $L^1$-bounded martingale can be written as the sum of three martingales, one bounded in $L^2$, one whose differences are absolutely summable in $L^1$, and one that is non-zero only on an event of small probability (Gundy 1968). Gundy's construction used several stopping times. In his 1971 Wald Memorial Lectures, published as Distribution Function Inequalities for Martingales (Burkholder 1973), D. L. Burkholder gave a simplified version of the decomposition in which only one stopping time is used, with explicit constants $2$, $4$ and $1$. This mission formalizes that version, Theorem 4.1 of the lectures, together with the facts its proof rests on.

Timeline:

• 1953. J. L. Doob's Stochastic Processes establishes almost-everywhere convergence of $L^1$-bounded martingales and the maximal inequality.
• 1966. D. G. Austin proves that the integral of $S^2(f)$ over $\{f^*\le\lambda\}$ is finite for an $L^1$-bounded martingale (Austin 1966).
• 1968. Gundy proves the decomposition theorem for $L^1$-bounded martingales, with applications to weak-type estimates.
• 1973. Burkholder's Lemma 2.1, a refinement of Austin's theorem, yields a one-stopping-time proof of Gundy's decomposition with explicit constants.

Setting

Let $(\Omega,\mathcal A,P)$ be a probability space and $\mathcal A_0\subseteq\mathcal A_1\subseteq\cdots$ a nondecreasing sequence of sub-$\sigma$-fields of $\mathcal A$. A martingale relative to $\mathcal A_1,\mathcal A_2,\dots$ is a sequence $f=(f_1,f_2,\dots)$ of integrable random variables with $f_n$ $\mathcal A_n$-measurable and $E(f_{n+1}\mid\mathcal A_n)=f_n$. Its difference sequence is $d=(d_1,d_2,\dots)$ with $f_n=\sum_{k=1}^n d_k$, i.e. $d_1=f_1$, $d_k=f_k-f_{k-1}$ (the convention is $f_0=0$).

The maximal function is $f^*=\sup_{n\ge1}|f_n|$, the square function is $S(f)=\big[\sum_{k\ge1}d_k^2\big]^{1/2}$, and $S_n(f)$ is its $n$-th partial version. For $0<p<\infty$,

$$\|f\|_p=\sup_{n\ge1}\|f_n\|_p,\qquad \|f_n\|_p=(E|f_n|^p)^{1/p},$$

and $f$ is $L^p$-bounded when $\|f\|_p<\infty$. For $\lambda>0$, the exit time $\mu=\inf\{n\ge1:|f_n|>\lambda\}$ (with $\inf\emptyset=\infty$) is the first index at which $|f_n|$ exceeds $\lambda$; $f_\mu$, $f_{\mu-1}$, $S_{\mu-1}(f)$ denote evaluation at the random index, with $f_\infty=\lim_n f_n$.

The Lean development names these objects dseq ($d$), sqFnN/sqFn ($S_n(f)$, $S(f)$), maxFnN/maxFn ($f_n^*$, $f^*$), pNorm ($\|f\|_p$), exitTime ($\mu$) and valAt/sqFnAt (evaluation at an index in $\{0,1,\dots,\infty\}$), all in the namespace BurkholderDFI.Gundy.

Formalization targets

Goal: Theorem 4.1 (p. 23)

For every $L^1$-bounded martingale $f$ and every $\lambda>0$ there are martingales $X,Y,Z$ relative to the same $\sigma$-fields, with difference sequences $x,y,z$, such that

$$f=X+Y+Z,\qquad \|X\|_2^2\le2\lambda\|f\|_1,\qquad \Big\|\sum_{k=1}^\infty|y_k|\Big\|_1\le4\|f\|_1,\qquad P(Z^*>0)\le\|f\|_1/\lambda.$$

The three bounds hold together; each alone is trivial ($f=0+0+f$ satisfies the first two, $f=0+f+0$ the first and last).

Milestones

1. Doob's facts (cited, §1, p. 20). An $L^1$-bounded martingale or nonnegative submartingale converges almost everywhere, and $\|f_\mu\|_1\le\|f\|_1$ for every stopping time $\mu$.
2. (1.5) (p. 20). $\lambda^pP(f^*>\lambda)\le\|f\|_p^p$ for $1\le p<\infty$.
3. Lemma 2.1 (p. 21). For the exit time $\mu$ above $\lambda$,

$$\|S_{\mu-1}(f)\|_2^2+\|f_{\mu-1}\|_2^2\le2Ef_\mu f_{\mu-1}\le2\lambda\|f\|_1,$$

with equality on the left for martingales.

Significance

The result. The decomposition is the standard device for passing from $L^2$ to weak-type $(1,1)$ estimates for martingale operators: an operator that is bounded on $L^2$, controlled by total variation on the second piece, and local in the sense that it vanishes where the third piece vanishes, is of weak type $(1,1)$. Applications of the decomposition are given in Gundy's papers of 1968 and 1969 (On the class $L\log L$, martingales, and singular integrals, Studia Math. 33), which the lectures cite for this purpose. The explicit constants $2$, $4$, $1$ make every such weak-type constant explicit.

Formalizing it. The theorem is classical and proved; the remaining work is its formalization. As far as is known, no machine-checked proof of Gundy's decomposition, of Lemma 2.1, or of the weak-type maximal inequality in the form (1.5) for real martingales exists in Mathlib or on this platform. Mathlib provides almost-everywhere convergence of $L^1$-bounded submartingales and Doob's maximal inequality for nonnegative submartingales; the stopped-value bound for unbounded stopping times, the square-function identity of Lemma 2.1 and the decomposition itself are new. The milestones are shared with other missions of this series (Lemma 2.1 is also used for Burkholder's weak-type square function inequality and his exponential estimates), so each proof is reused.

Difficulty

The obvious attempt imitates the Calderón–Zygmund cut directly: truncate $f$ at height $\lambda$, or stop it when it first exceeds $\lambda$. Neither produces the required pieces. Truncation destroys the martingale property, and whatever restores it adds terms that must themselves be controlled in the right norm. Stopping at the exit time produces a martingale bounded by $\lambda$ only up to the overshoot at the exit, which is not bounded and lives on an event that is small only in probability. The $L^2$ estimate (4.2) is therefore not a consequence of boundedness; it needs a quantitative square-function bound for the martingale up to the exit, which is the content of Lemma 2.1, and that lemma in turn needs the limit $f_\infty$ and the stopped values $f_\mu$ on $\{\mu=\infty\}$ — so Doob's convergence theorem cannot be avoided.

Formalization scope

Processes are functions f : ℕ → Ω → ℝ with a Mathlib Filtration ℕ and Mathlib's Martingale/Submartingale. The paper indexes from $1$; Lean's index $0$ is never read by any quantity in the statements, which use the paper's convention $f_0=0$. Mathlib's martingale definition additionally constrains $f_0=E(f_1\mid\mathcal A_0)$; this is no restriction, since every martingale indexed from $1$ extends this way. The goal asserts that $X,Y,Z$ are Mathlib martingales for the same filtration as $f$, and the identity $f_n=X_n+Y_n+Z_n$ is required for $n\ge1$.

Further committed conventions:

• $S(f)$, $f^*$, $Z^*$, $\|\cdot\|_p$ and all expectations of nonnegative quantities take values in $[0,\infty]$ (lower Lebesgue integral), so no infinite value is silently replaced by $0$.
• $\|X\|_2=\sup_{n\ge1}\|X_n\|_2$, not the norm of a limit; $Z^*=\sup_{n\ge1}|Z_n|$; $\|\sum_k|y_k|\|_1$ is the integral of the series with $y_1=Y_1$.
• The exit time takes values in $\mathbb N\cup\{\infty\}$ and $\mu-1$ is truncated, with $\infty-1=\infty$; the a.e. limit $f_\infty$ is a function supplied with its convergence hypothesis (Lemma 2.1) or asserted to exist (Doob's facts).
• "Nonnegative submartingale" means $f_n\ge0$ almost surely for $n\ge1$.
• $\Omega$ is an arbitrary measurable space with a probability measure.

A formalization in which the existential could choose its own filtration, or in which the norms were Bochner integrals (which vanish on non-integrable functions), would trivialize the goal; both are excluded by the statement above.

Infrastructure needed: stopped values at unbounded stopping times and their $L^1$ bound; square-function identities for stopped martingales (orthogonality of martingale differences up to a stopping time); conditional-expectation compensators of predictable truncations. The definitions file is shared with the other eight missions of this series and is reusable for any work on discrete-time square and maximal functions. Proofs of the milestones, alternative arguments, and sharper constants are all welcome.

Selected references

• D. L. Burkholder, Distribution function inequalities for martingales, The Annals of Probability 1(1), 19–42, 1973. https://doi.org/10.1214/aop/1176997023
• R. F. Gundy, A decomposition for L¹-bounded martingales, The Annals of Mathematical Statistics 39(1), 134–138, 1968. https://doi.org/10.1214/aoms/1177698510
• D. G. Austin, A sample function property of martingales, The Annals of Mathematical Statistics 37(5), 1396–1397, 1966. https://doi.org/10.1214/aoms/1177699283
• J. L. Doob, Stochastic Processes, Wiley, New York, 1953.

Motivation

Programs often reveal information through the memory locations they touch, even when the contents of those locations are hidden. An oblivious RAM simulation aims to conceal this access pattern. Goldreich and Ostrovsky studied the cost of doing so for arbitrary RAM programs and showed that the access sequence itself imposes a lower bound on simulation overhead. Their 1996 paper gives an upper-bound construction as well as the lower-bound theorem targeted here. The issue matters when a storage observer can see which addresses are accessed but must learn nothing about the program's private requests.

Theorem 6.1 of the paper states that simulating $t$ steps requires at least the initial memory size and, asymptotically, a multiple of $t\log t$ accesses. Its proof introduces a simpler ball-and-cell game that grants the player more information and freedom than the RAM simulation. The mission formalizes that game and its lower bound. This makes the combinatorial content of the published argument a precise theorem about randomized behavior and visible observations. The paper's earlier Theorem 1.2.2 on p. 437 is labeled informal and has a different explicit bound; the target here is Theorem 6.1 on pp. 469–470.

Setting

There are $m$ numbered balls and $m$ numbered cells. Cell $i$ initially contains ball $i$, and a player's hand is empty. Each cell can hold at most one ball and the hand can hold at most $b$ balls. In one access, the player names a cell and secretly takes its ball into a nonfull hand, places one held ball into an empty cell, or leaves the cell unchanged. Taking from an empty cell and placing into an occupied cell are illegal. The observer sees the named cell at each access but not the hidden operation. A run of $q$ accesses is written $a=((v_1,h_1),\ldots,(v_q,h_q))$, and its visible sequence is $V(a)=(v_1,\ldots,v_q)$.

A request sequence $r=(r_1,\ldots,r_t)$ names a ball for each of $t$ rounds. A run satisfies $r$ if it is legal and there are indices $1\le j_1\le\cdots\le j_t=q$ such that ball $r_i$ is in the player's hand after the first $j_i$ accesses. Equal indices are permitted: several rounds may finish after the same access. The player may know the entire request sequence in advance. That assumption is part of the paper's game, and the paper notes that its lower bound does not require an online player.

A randomized player assigns each request sequence a probability distribution over finite runs. It is correct if every run with positive probability satisfies its requests. It is oblivious if the distribution of $V(a)$ is identical for every pair of request sequences of length $t$. Thus the observer cannot infer the requested balls from the accessed cells, even statistically. These conditions quantify over all request sequences, not a selected input or a single deterministic access pattern.

Formalization targets

Theorem 6.1: access lower bound

For every correct oblivious player and every run in the support of its response, the mission targets

$$q\ge m\quad(t\ge1),\qquad q\ge c_b t\log t\quad(m=t,\ t\ge T_b),$$

where $c_b>0$ and $T_b$ depend only on the fixed hand size $b$. This is the paper's $\max\{m,\Omega(t\log t)\}$ form, with $m$ representing the number $|y|$ of initially occupied memory words. It asserts a bound on every possible run, rather than only on average access count. No numerical constant is prescribed by the paper.

Intermediate counting targets

The milestones record the first-round $m$ bound, the at-most-$(b+2)^q$ count of legal hidden action sequences compatible with a visible sequence, and the implication from obliviousness that one visible sequence can serve every request sequence. They then state the corrected finite counting bounds

$$|\{r:a\models r\}|\le\operatorname{multichoose}(q,t)b^t, \qquad m^t\le(b+2)^q\operatorname{multichoose}(q,t)b^t.$$

These preserve the paper's non-strict round ends. The milestone source text records the published formulas, while the formal statements and descriptions identify the corrections.

Significance

The result limits how cheaply a simulator can hide a program's memory access pattern when the observer sees addresses. In the game, a player is even allowed to remember the entire ball placement without cost, know the future requests, and randomize its actions. A lower bound under these permissive conditions applies to the more constrained access-pattern problem that motivated the game, subject to the paper's reduction from simulation to the game. The $m$ term also accounts for the initially occupied memory, independently of the asymptotic term.

The theorem is a published mathematical result, but the mission's Lean declarations are statements with proof holes until solvers supply machine-checked proofs. Formalizing the game creates reusable definitions for legal hidden operations, request satisfaction, randomized players, and visible distributions. Formalizing the corrected counting targets also makes explicit a discrepancy in the printed proof rather than silently relying on an invalid intermediate inequality.

Difficulty

The main difficulty is accounting for requests when several rounds end at the same access. The paper's observation that a fixed $q$-access run serves at most $b^q$ request sequences is false under its own non-strict indices. A run that fetches every ball it can hold may answer many later rounds without making another access. Likewise, the alternative binomial count in footnote 29 assumes distinct completion points and fails when $t>q$. The final asymptotic result still has a valid corrected counting target, but a proof cannot quote the published intermediate formulas literally. Randomized behavior adds another precise requirement: equality of visible distributions must support conclusions about runs with positive probability for each request sequence.

Formalization scope

The Lean carrier is the paper's ball-and-cell game from §6, rather than the interactive RAM machine model of §2. The game relaxes the simulation by giving the player free memory of ball locations and advance knowledge of requests. Balls, cells, and rounds use finite types Fin m and Fin t; these are zero-based encodings of the paper's $[m]$ and round labels. Action steps are counted from one, with the initial state at step zero. PMF represents the player's discrete probability distributions, and equality of PMF.map visible represents observer independence. Every positive-probability run must be legal and satisfy its requests. The visible and hidden sequences have the same finite length $q$.

The two printed estimates $b^q$ and $b^q(b+2)^q>m^t$ are false: with $m=b=q=2$ and $t=7$, taking both balls in two accesses satisfies all $2^7=128$ request sequences, while the printed product is $64$. Footnote 29's $\binom qt b^t$ also vanishes in this example. The formal milestones use Nat.multichoose q t to accommodate repeated round ends; at $q=t=0$ its value is defined directly, so no negative binomial upper index is used. The logarithm in the goal is the natural logarithm, and a threshold $T_b$ handles small $t$.

Correctness and legality are part of the player type, so an unrestricted sequence of cell names cannot satisfy the mission by bypassing the hand and cell rules. Obliviousness uses equality of full distributions, and the goal quantifies over every supported run. The required development includes finite-state transition reasoning, finite combinatorial counts, PMF support and mapping, and real logarithm estimates. These components, especially the game interface and support lemmas, can be reused by later access-pattern formalizations.

Selected references

• Oded Goldreich and Rafail Ostrovsky, Software protection and simulation on oblivious RAMs, Journal of the ACM 43(3):431–473, 1996. DOI: 10.1145/233551.233553. Theorem 6.1 and its proof are on pp. 469–470; the informal Theorem 1.2.2 is on p. 437.

Why cores of games with side payments

A cooperative game with side payments assigns to each coalition of players the total payoff it can secure on its own and share freely among its members. The core is the set of ways of dividing the payoff of the grand coalition that no coalition can improve upon. It is the basic stability notion of cooperative game theory and of its applications in operations research: cost allocation for shared facilities, network design, inventory pooling and linear production games all ask whether a core allocation exists and what it looks like.

The core can be empty, and the question of when it is not was answered independently by Bondareva (1963) and Shapley (1967): the core is nonempty exactly when the game is balanced, a linear-programming condition on weighted families of coalitions. Scarf (1967) extended the existence half to games without side payments, and Billera (1970) recast balancedness for those games.

Aubin's Cooperative Fuzzy Games (Math. Oper. Res. 6(1), 1981) reads these results through fuzzy coalitions, in which each player participates at a rate between 0 and 1. In §6 every game on a family of coalitions is extended to a concave positively homogeneous function of fuzzy coalitions, and the Bondareva–Shapley theorem becomes a statement about that extension. This mission formalizes §2 and §6 of the paper: the core of a fuzzy game with side payments, its superdifferential description, and Proposition 6.1.

Setting

Let $N=\{1,\dots,n\}$ be the set of players. A coalition $A\subseteq N$ is identified with its characteristic vector $\tau^A\in\{0,1\}^n$, and $\tau^N=(1,\dots,1)$. A fuzzy coalition is a vector $\tau\in[0,1]^n$, where $\tau_i$ is the rate at which player $i$ participates.

A fuzzy game with side payments is a worth function $v$ with $v(0)=0$ that is positively homogeneous, $v(t\tau)=t\,v(\tau)$ for $t>0$. Homogeneity extends $v$ from $[0,1]^n$ to the orthant $\mathbb R^n_+$. Its core is

$$\operatorname{core}(v)=\Big\{c\in\mathbb R^n:\ \sum_{i\in N}c_i=v(\tau^N),\ \ \sum_{i\in N}\tau_ic_i\ge v(\tau)\ \text{for all }\tau\in[0,1]^n\Big\},$$

the allocations that no fuzzy coalition blocks. The superdifferential of $v$ at $\tau$ is $\partial v(\tau)=\{c:\ v(\tau)-v(\sigma)\ge\sum_i c_i(\tau_i-\sigma_i)\ \text{for all }\sigma\in\mathbb R^n_+\}$.

A usual game with side payments is given by a family $\mathscr C$ of nonempty coalitions that contains $N$ and every singleton $\{i\}$, and by a worth $v(A)\in\mathbb R$ for each $A\in\mathscr C$. Its core is the set of $c\in\mathbb R^n$ with $\sum_{i\in N}c_i=v(N)$ and $\sum_{i\in A}c_i\ge v(A)$ for every $A\in\mathscr C$. For $\tau\in\mathbb R^n_+$, $\mathscr C(\tau)$ is the set of nonnegative weights $m(A)$, $A\in\mathscr C$, with $\sum_{A\ni i}m(A)=\tau_i$ for each player $i$, and

$$\pi v(\tau)=\sup_{m\in\mathscr C(\tau)}\ \sum_{A\in\mathscr C}m(A)\,v(A).$$

The game is balanced if $\pi v(\tau^N)=v(N)$.

Formalization targets

Goal: Proposition 6.1

$$\operatorname{core}(v)\neq\emptyset\iff \pi v(\tau^N)=v(N),\qquad\text{and then}\qquad \operatorname{core}(v)=\operatorname{core}(\pi v).$$

The first half is the Bondareva–Shapley theorem for an arbitrary family $\mathscr C$. The second identifies the core of the discrete game with the core of the fuzzy game $\pi v$.

Milestones

1. §2 (4)–(5). For a positively homogeneous $v$ with $v(0)=0$, $\operatorname{core}(v)=\partial v(\tau^N)$.
2. Remark 2.1. Such a $v$ is concave on $\mathbb R^n_+$ if and only if it is superadditive, $v(\tau+\sigma)\ge v(\tau)+v(\sigma)$.
3. Proposition 2.1. If $v$ is moreover concave, its core is convex, compact and nonempty; if $v$ is differentiable at $\tau^N$, the core is $\{Dv(\tau^N)\}$.
4. §6 (5). If $m\in\mathscr C(\tau)$ and $m(A)>0$, then $A\subseteq A_\tau=\{i:\tau_i>0\}$.
5. §6 (2). $\pi v$ is the smallest concave positively homogeneous function on $\mathbb R^n_+$ with $\pi v(\tau^A)\ge v(A)$ for every $A\in\mathscr C$.
6. §6, after (6). The core of the fuzzy game $\pi v$ is nonempty, convex and compact, whether or not $v$ is balanced.

Significance

Proposition 6.1 is the standard criterion for the existence of core allocations in transferable-utility games. In operations research it is the tool behind core results for linear production games, flow games, facility location and inventory games: one exhibits a family of balancing weights, or the absence of one, and reads off whether a stable cost or profit allocation exists. Aubin's version adds that a balanced game's core is the superdifferential of a concave function, so it is described by convex analysis and, when $\pi v$ is smooth at $\tau^N$, reduces to a single point given by the gradient.

The result is classical and proved in the literature. To our knowledge, no machine-checked proof of the Bondareva–Shapley theorem exists in Mathlib or on this platform: the platform has results on cores of convex (supermodular) games, which are a different hypothesis. The mission therefore produces a first formal proof of the theorem for a general family $\mathscr C$ of coalitions, the superdifferential description of the fuzzy core, and the minimality of the concave extension $\pi v$. The definitions (fuzzy coalitions, balances, $\pi v$) are reusable by later missions on games without side payments and on values of fuzzy games.

Difficulty

The inclusion $\operatorname{core}(v)\subseteq\operatorname{core}(\pi v)$ and the necessity of balancedness are short computations with the balancing weights. The difficulty is sufficiency: from $\pi v(\tau^N)=v(N)$, a core allocation has to be produced. This is an existence statement for a system of linear inequalities, and it needs a duality or separation argument. Mathlib's finite-dimensional linear programming duality and separation theorems do not apply off the shelf, because $\pi v$ is a supremum over a polytope of weights indexed by coalitions, and its attainment and finiteness must be established first. Proposition 2.1 similarly needs the existence of supergradients of a concave function at an interior point and their compactness, which are not packaged for functions defined only on an orthant.

Formalization scope

Players are Fin n; multiutilities and fuzzy coalitions are Fin n → ℝ with the coordinatewise order, and the cube is Set.Icc 0 1. The commitments are:

• A fuzzy game is a function on $\mathbb R^n$ whose values off the orthant are never used; $v(0)=0$ and homogeneity for every $t>0$ and $\tau\ge0$ are hypotheses of every §2 statement, because §2 states them once for the whole section. Concavity is concavity on $\mathbb R^n_+$.
• In the superdifferential (5), $\sigma$ ranges over $\mathbb R^n_+$, the domain of the extended $v$; the paper leaves this implicit.
• "Differentiable at $\tau^N$" is DifferentiableAt at the interior point $(1,\dots,1)$, and $Dv(\tau^N)$ is the vector of partial derivatives.
• The family $\mathscr C$ contains $N$ and all singletons and excludes $\emptyset$; the core and $\pi v$ use only coalitions in $\mathscr C$, so $v(\emptyset)=0$ plays no role. Because $N\in\mathscr C$ and $\emptyset\notin\mathscr C$, the family exists only for $n\ge1$.
• $\pi v$ is a real supremum. For $\tau\ge0$ the set of values is nonempty and bounded above, so the value is the paper's; off the orthant the set is empty and the value is never used.
• The printed $v(\mathscr C)$ and $\tau^{\mathscr C}$ in §6 (2)–(3) are read as $v(A)$ and $\tau^A$, as §6 (4) settles.

Balancedness is the equation $\pi v(\tau^N)=v(N)$ with $\pi v$ built from the balances of §6 (3)–(4); a formalization that defines "balanced" through the core, or takes $\pi v$ to be an envelope already known to agree with the core, makes the goal empty and is ruled out. Contributions welcome: proofs of the milestones, a general Bondareva–Shapley lemma for finite families of coalitions, and supergradient existence for concave functions on convex sets with nonempty interior.

Selected references

• J.-P. Aubin, Cooperative Fuzzy Games, Mathematics of Operations Research 6(1), 1981, 1–13. https://doi.org/10.1287/moor.6.1.1
• O. N. Bondareva, Some applications of linear programming methods to the theory of cooperative games, Problemy Kibernetiki 10, 1963, 119–139 (in Russian; no stable online copy).
• L. S. Shapley, On balanced sets and cores, Naval Research Logistics Quarterly 14(4), 1967, 453–460. https://doi.org/10.1002/nav.3800140404
• H. E. Scarf, The core of an N person game, Econometrica 35(1), 1967, 50–69. https://doi.org/10.2307/1909703
• L. J. Billera, Some theorems on the core of an n-person game without side-payments, SIAM Journal on Applied Mathematics 18(3), 1970, 567–579. https://doi.org/10.1137/0118007
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

The core of an exchange economy is the set of allocations that no group of consumers can improve upon by trading only among themselves. The Walras equilibria (competitive equilibria) are the allocations supported by a price system at which every consumer maximizes preference on a budget set. Every Walras equilibrium is in the core, but for a fixed finite economy the core is usually much larger. Edgeworth (1881) conjectured that the core shrinks to the competitive allocations as the number of traders grows; Debreu and Scarf (1963) proved this for replica economies, and Aumann (1964) proved exact equality for an atomless continuum of traders.

Jean-Pierre Aubin's Cooperative Fuzzy Games (Math. Oper. Res. 6 (1981) 1–13) gives a third route to the same conclusion, with a fixed finite number of consumers. Coalitions are allowed to be fuzzy: a consumer may join with any rate of participation between 0 and 1. Once all fuzzy coalitions may block, the core of the economy, now called the fuzzy core, is exactly the set of Walras equilibria (Theorem 4.1, p. 6). The paper presents this as a slight modification of the Debreu–Scarf theorem; in Remark 4.2 it observes that Debreu–Scarf's replica coalitions correspond to the rational points of the cube $[0,1]^n$.

This mission formalizes §4 of the paper. It is the fourth mission of a series on the paper; the others treat the cores of fuzzy games with and without side payments and the values of smooth fuzzy games.

Setting

There are $n$ consumers $i \in N = \{1,\dots,n\}$ and $l$ commodities. Consumer $i$ consumes bundles in $\mathbb{R}^l_+$, ranks them by a preference relation $\succcurlyeq_i$ (with strict part $\succ_i$), and owns a set $Y(i) \subset \mathbb{R}^l$ of possible initial endowments. Each $Y(i)$ is closed, convex and comprehensive: whenever $y \in Y(i)$ and $z \ge 0$, also $y - z \in Y(i)$.

A fuzzy coalition is a vector $\tau \in [0,1]^n$; $\tau_i$ is the rate at which consumer $i$ participates, and $A_\tau = \{i : \tau_i > 0\}$ is the set of participants. The coalition $\tau$ disposes of the endowments

$$Y(\tau) = \sum_{i \in N} \tau_i\, Y(i),$$

and its allocations are the families $x_\tau = (x_\tau^i)_{i \in A_\tau}$ of bundles $x_\tau^i \in \mathbb{R}^l_+$ with $\sum_i \tau_i x_\tau^i \in Y(\tau)$; this set is $X(\tau)$. The allocations of the whole economy are $X(N) = X(\tau^N)$, $\tau^N = (1,\dots,1)$.

An allocation $x \in X(N)$ is in the fuzzy core if there is no nonzero fuzzy coalition $\tau$ and allocation $x_\tau \in X(\tau)$ with $x_\tau^i \succ_i x^i$ for every $i \in A_\tau$.

The income of consumer $i$ at prices $p \in \mathbb{R}^l$ is $r_i(p) = \sup_{y \in Y(i)} p\cdot y$, and the budget set is $B_i(p) = \{x \in \mathbb{R}^l_+ : p \cdot x \le r_i(p)\}$. An allocation $\bar x \in X(N)$ is a Walras equilibrium if some price $\bar p \in \mathbb{R}^l$ satisfies, for every $i$,

$$\bar p \cdot \bar x^i = r_i(\bar p) \qquad\text{and}\qquad \bar x^i \succcurlyeq_i x \ \text{ for all } x \in B_i(\bar p).$$

Assumption (1) of §4 requires each preference to be continuous and convex, with $x \succ_i y \Rightarrow \alpha x + (1-\alpha) y \succ_i y$ for $\alpha \in\, ]0,1[$; no consumer to be satiated; and each $Y(i)$ to contain a vector with all coordinates strictly positive.

Formalization targets

Goal: Theorem 4.1

Under assumption (1),

$$\text{fuzzy core} \;=\; \{\text{Walras equilibria}\}.$$

Milestones, from the proof of Theorem 4.1

1. Every Walras equilibrium belongs to the fuzzy core.
2. For an allocation $\bar x \in X(N)$, each set $Q(i) = Y(i) - \{x \in \mathbb{R}^l_+ : x \succ_i \bar x^i\}$ is nonempty.
3. If $\bar x$ belongs to the fuzzy core, then

$$0 \notin \operatorname{co}\Big(\bigcup_{i=1}^n Q(i)\Big).$$

The remaining step of the paper, from milestone 3 to the existence of the equilibrium price, is stated there only as "by known arguments" and is left to the solver as part of the goal.

Significance

The result. Theorem 4.1 is a core equivalence theorem for an economy with finitely many consumers and no replication or continuum of traders. It identifies the competitive allocations as exactly the allocations that are stable against partial coalitions. It also makes visible which coalitions matter: Remark 4.1 attributes the equivalence to the fact that all fuzzy coalitions are allowed to form, so that the set of coalitions is convex. The same fuzzy-coalition device underlies the nonemptiness results for cores of fuzzy games in §5–§7 of the paper.

Formalizing it. The theorem is proved in the paper, in one paragraph that defers its final step to "known arguments". To our knowledge neither the theorem nor the Debreu–Scarf or Aumann core equivalence theorems have been formalized in Lean. A complete development provides a reusable model of an exchange economy with preference relations and comprehensive endowment sets, a checked argument from separation to equilibrium prices, and a template for the classical core equivalence theorems.

Difficulty

The inclusion of the Walras equilibria in the fuzzy core is a budget computation. The converse is the content of the theorem: from the mere absence of improving fuzzy coalitions, a single price vector must be produced that works for all consumers simultaneously. Separating consumer by consumer gives one price per consumer, not a common one, so the coalitional structure has to enter before any price exists. Once a candidate price is available, it still has to be shown nonnegative, each equilibrium bundle has to exhaust its owner's income, and no bundle in a budget set may be strictly preferred; each of these uses a different part of assumption (1), and the paper leaves all three to "known arguments". The incomes $r_i(p)$ may be $+\infty$ for prices with negative coordinates, so finiteness at the equilibrium price is part of the conclusion, not an assumption.

Formalization scope

Consumers are Fin n, commodities Fin l; an allocation is a function Fin n → Fin l → ℝ, a price a vector Fin l → ℝ, and $p \cdot y = \sum_k p_k y_k$. A single definitions file (FuzzyGames.Walras.Basic) holds the economy, its assumptions, $Y(\tau)$, $X(\tau)$, the fuzzy core, incomes, budget sets, Walras equilibria and the sets $Q(i)$.

The formalization commits to the following readings, each recorded in the items' Formalization Notes:

• Complete preferences. The paper's "preference preordering" is read, as in Debreu's usage, as a reflexive, transitive and complete relation on $\mathbb{R}^l_+$. The relation is a predicate on $\mathbb{R}^l$, but every assumption and every use is restricted to $\mathbb{R}^l_+$.
• Continuity means closed upper and lower contour sets in $\mathbb{R}^l_+$; convexity means convex upper contour sets, plus the condition of (1)(i).
• Assumption (1)(i) is printed with $x \succcurlyeq y$ in the premise, which fails at $x = y$; it is stated with $x \succ y$.
• Blocking is strict and by nonzero coalitions. The fuzzy-core definition is printed with $x_\tau^i \succcurlyeq x^i$; the proof uses $\succ$, and the weak version would let every allocation block itself. The coalition $\tau = 0$ is excluded, since its condition over $A_\tau = \emptyset$ is vacuous.
• Dummy coordinates. An allocation of $\tau$ is a full family of $n$ bundles; those with $\tau_i = 0$ are multiplied by $0$, unconstrained and never compared.
• $Y(\tau)$ is Mathlib's pointwise Minkowski sum of scaled sets.
• Incomes take values in the extended reals (EReal), so that $r_i(p) = +\infty$ is represented and never replaced by a default value.

A trivializing formalization is ruled out: the assumptions are satisfiable, and a sorry-free check (one consumer, one commodity, $x \succcurlyeq y \iff x \ge y$, $Y(1) = (-\infty, 1]$) verifies them together with a Walras equilibrium, so neither side of the goal is empty by construction.

Contributions welcome: proofs of the milestones, a separation-to-prices lemma for comprehensive endowment sets, and general facts about complete continuous convex preferences on $\mathbb{R}^l_+$, which are reusable for any general equilibrium development.

Selected references

• J.-P. Aubin, Cooperative fuzzy games, Mathematics of Operations Research 6(1) (1981) 1–13. https://doi.org/10.1287/moor.6.1.1
• G. Debreu, H. Scarf, A limit theorem on the core of an economy, International Economic Review 4(3) (1963) 235–246. https://doi.org/10.2307/2525290
• R. J. Aumann, Markets with a continuum of traders, Econometrica 32 (1964) 39–50. https://doi.org/10.2307/1913732
• G. Debreu, Theory of Value, Cowles Foundation Monograph 17, Yale University Press, 1959.