Completed

Harmonic Analysis Probability·Captain: mikedeng1

Distribution Function Inequalities for Martingales 9: EΦ(f*) Is Controlled by the Conditional Square Function and the Largest Jump, for Every Φ of Moderate GrowthResearch Paper

Motivation

A martingale $f=(f_1,f_2,\dots)$ is a sum of increments $d_k=f_k-f_{k-1}$ each of which has conditional mean zero given the past. Most quantitative statements about martingales compare the size of the maximal function $f^*=\sup_n|f_n|$ with some measure of the size of the increments. Two such measures are classical: the square function $S(f)=(\sum_k d_k^2)^{1/2}$ , which sums the realized squared increments, and the conditional square function $s(f)=(\sum_k E(d_k^2\mid\mathcal A_{k-1}))^{1/2}$ , which sums their predicted conditional variances. The conditional square function is the discrete analogue of the predictable quadratic variation $\langle M\rangle$ of a continuous-time martingale, and it is the quantity that appears in martingale central limit theorems, Freedman- and Bernstein-type exponential bounds, and in the analysis of stochastic approximation algorithms, where the noise is typically described through its conditional variance.

This mission formalizes Theorem 21.1 of D. L. Burkholder's 1971 Wald Memorial Lectures, Distribution Function Inequalities for Martingales (Ann. Probability 1 (1973) 19–42). The theorem bounds $E\Phi(f^*)$ by $E\Phi(s(f))$ and the size of the largest jump, for every $\Phi$ of moderate growth.

Timeline. Rosenthal (1970) proved, for sums of independent mean-zero random variables and $2\le p<\infty$ , that the $p$ -th moment of the sum is comparable to $(\sum_k Ed_k^2)^{p/2}+\sum_k E|d_k|^p$ (Israel J. Math. 8 (1970)). Burkholder and Gundy (1970, [6] in the paper) developed extrapolation methods for martingale operators, including Example 8.2, which shows that $E\Phi(S(f))\le cE\Phi(s(f))$ fails for general $\Phi$ (Acta Math. 124 (1970)). Theorem 21.1 follows from Theorem 3.1 of Burkholder, Davis and Gundy (1972, [5] in the paper), as remarked at the top of p. 553 of Burkholder's 1970 ICM address ([4] in the paper). In the Wald lectures Burkholder gives a direct proof by a distribution function inequality, which this mission formalizes.

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$ . Let $f=(f_1,f_2,\dots)$ be a martingale relative to $\mathcal A_1,\mathcal A_2,\dots$ , and set $f_0=0$ , so that the difference sequence is $d_1=f_1$ and $d_k=f_k-f_{k-1}$ for $k\ge2$ . Define

f^*=\sup_{n\ge1}|f_n|,\qquad d^*=\sup_{k\ge1}|d_k|,\qquad s(f)=\Big[\sum_{k=1}^\infty E\big(d_k^2\mid\mathcal A_{k-1}\big)\Big]^{1/2}.

The first conditional expectation is taken with respect to $\mathcal A_0$ . All three quantities may be infinite.

A function $\Phi:[0,\infty]\to[0,\infty]$ satisfies the conditions of Section 7 if it is nondecreasing and continuous, $\Phi(0)=0$ , and it has moderate growth:

\Phi(2\lambda)\le c\,\Phi(\lambda),\qquad\lambda>0. \tag{6.1}

The constant $c=c_{(6.1)}$ is the growth constant. The powers $\Phi(\lambda)=\lambda^p$ , $0<p<\infty$ , are the basic examples; $\Phi$ need not be convex.

In Lean the shared layer is BurkholderDFI.CondSquare.Martingale: dseq f is $d$ , maxFn f is $f^*$ , maxFn (dseq f) is $d^*$ , condSqFn ℱ P f is $s(f)$ and IsPhi Φ c is the class above.

Formalization targets

Goal: Theorem 21.1

For every growth constant $c_{(6.1)}$ there is a constant $c$ such that for every martingale $f$ and every $\Phi$ satisfying the conditions of Section 7,

E\Phi(f^*)\le c\,E\Phi(s(f))+c\,E\Phi(d^*). \tag{21.1}

The constant depends only on $c_{(6.1)}$ , and no value for it is fixed, so the goal remains valid under any improvement of the constant.

Milestones

Doob's weak-type inequality (1.5): $\lambda^pP(f^*>\lambda)\le\|f\|_p^p$ for $1\le p<\infty$ .
The distribution function inequality (21.2): for $\beta>1$ , $0<\delta<\beta-1$ and $\lambda>0$ ,

P\big(f^*>\beta\lambda,\ s(f)\vee d^*\le\delta\lambda\big)\le\frac{\delta^2}{(\beta-\delta-1)^2}P(f^*>\lambda).

Lemma 7.1, which turns an inequality of the form $P(g>\beta\lambda,\ f\le\delta\lambda)\le\varepsilon P(g>\lambda)$ into $E\Phi(g)\le\frac{\gamma\eta}{1-\gamma\varepsilon}E\Phi(f)$ .

Further statements

Two consequences recorded in §21 are included as draft theorems: (21.5), $E\Phi(f^*)\le cE\Phi(s(f))+c\sum_kE\Phi(|d_k|)$ , and the upper half (21.4) of Rosenthal's inequality for independent mean-zero sums.

Significance

The result. Theorem 21.1 controls the maximal function by predictable information (the conditional variances) plus the single largest jump, for every $\Phi$ of moderate growth, convex or not. The jump term cannot be dropped: the paper notes that an inequality of the form $E\Phi(S(f))\le cE\Phi(s(f))$ fails for general $\Phi$ (Example 8.2 of Burkholder–Gundy 1970), so some account of large individual increments is necessary. Specialized to independent increments, $s(f)$ becomes the deterministic $(\sum_kEd_k^2)^{1/2}$ and the theorem yields the upper half of Rosenthal's inequality. The martingale version applies wherever increments are dependent but their conditional variances are controlled, as in stochastic approximation.

Formalizing it. The result is proved in the paper; to our knowledge neither Theorem 21.1 nor Rosenthal's inequality has a machine-checked proof. Mathlib has Doob's maximal inequality and martingale convergence, but not the conditional square function, good- $\lambda$ inequalities, or $\Phi$ -moment inequalities with moderate growth. A complete development produces all three, together with the stopping-time manipulations (a martingale started at one stopping time and stopped at another) that most of the paper's arguments reuse.

Difficulty

The obvious approach is to use $L^2$ theory: $E f_n^2=E s_n^2(f)$ for a square-integrable martingale, so $f^*$ and $s(f)$ are comparable in $L^2$ . This identity gives nothing for other $\Phi$ , and in particular for $\Phi(\lambda)=\lambda^p$ with $p<2$ or $p>2$ there is no direct comparison of $f^*$ and $s(f)$ : $s(f)$ can be small while one increment is huge. A bound for general $\Phi$ must therefore handle the event where a single increment dominates, and it must work for every level $\lambda$ simultaneously, using nothing about $\Phi$ beyond monotonicity and the growth condition (6.1). Without convexity of $\Phi$ , no Jensen- or duality-type argument applies.

Formalization scope

The Lean conventions committed to are:

$f^*$ , $d^*$ , $s(f)$ , $\|f\|_p$ and every expectation $E\Phi(\cdot)$ take values in $[0,\infty]$ (ℝ≥0∞, lower Lebesgue integrals), so infinite values are meaningful and no junk value $0$ arises.
The conditional expectations $E(d_k^2\mid\mathcal A_{k-1})$ are Mathlib's extended conditional expectations condLExp, which need no integrability of $d_k^2$ . The Bochner conditional expectation or condVar would return $0$ on non-integrable $d_k^2$ and must not be substituted.
The filtration ℱ : Filtration ℕ _ is indexed from $0$ , with ℱ k $=\mathcal A_k$ ; the $k$ -th summand of $s(f)$ pairs $d_{k+1}$ with ℱ k. The paper states that $f$ is a martingale relative to $\mathcal A_1,\mathcal A_2,\dots$ ; the formalization states that $f$ is a Mathlib martingale, which also constrains the index- $0$ term. This is no restriction, since the extension $f_0:=E(f_1\mid\mathcal A_0)$ is always possible, and all definitions use the paper's $f_0=0$ , never Lean's f 0.
IsPhi Φ c imposes (6.1) for every $x\in[0,\infty]$ , which is equivalent to the paper's condition by continuity. The paper's hypothesis that $\Phi$ is not identically zero is dropped, since every inequality is trivial for $\Phi\equiv0$ .
"The choice of $c$ depends only on $c_{(6.1)}$ " is the quantifier order $\forall c\ \exists C>0\ \forall(\Omega,P,\mathcal A,f,\Phi)$ , with $\Omega$ in Type. A constant chosen after $f$ or $\Phi$ would trivialize the goal whenever the right-hand side is positive, and that formalization is ruled out.
Lemma 7.1 takes $[0,\infty]$ -valued $f,g$ and nonnegative $\gamma,\eta$ . Rosenthal's inequality assumes integrable, mutually independent $d_k$ with mean zero.

Needed infrastructure, reusable beyond this mission: the conditional square function and its basic properties for stopped martingales; a good- $\lambda$ lemma for moderate-growth $\Phi$ (Lemma 7.1, shared with the other missions of this series); and the layer-cake formula $E\Phi(h)=\int_0^\infty P(h>\lambda)\,d\Phi(\lambda)$ for a Lebesgue–Stieltjes $\Phi$ . Proofs of the milestones, proofs of (21.5) and Rosenthal's inequality from the goal, and independent proofs of any of them are all welcome.

Selected references

D. L. Burkholder, Distribution Function Inequalities for Martingales, The Annals of Probability 1(1), 1973, 19–42. https://doi.org/10.1214/aop/1176997023
D. L. Burkholder, R. F. Gundy, Extrapolation and interpolation of quasi-linear operators on martingales, Acta Mathematica 124, 1970, 249–304. https://doi.org/10.1007/BF02394573
D. L. Burkholder, Inequalities for operators on martingales, Proc. International Congress of Mathematicians (Nice, 1970), vol. 2, Gauthier-Villars, 1971, 551–557.
D. L. Burkholder, B. J. Davis, R. F. Gundy, Integral inequalities for convex functions of operators on martingales, Proc. Sixth Berkeley Symp. Math. Statist. Probab. 2, 1972, 223–240.
H. P. Rosenthal, On the subspaces of $L^p$ ( $p>2$ ) spanned by sequences of independent random variables, Israel Journal of Mathematics 8, 1970, 273–303. https://doi.org/10.1007/BF02771562
J. L. Doob, Stochastic Processes, Wiley, New York, 1953.

5 thms2 active usersReviewed

Harmonic Analysis Probability Stochastic Systems·Captain: mikedeng1

Distribution Function Inequalities for Martingales 3: For Brownian Motion Stopped at Any Stopping Time τ, EΦ(X*(τ)) and EΦ(τ^{1/2}) Are ComparableResearch Paper

Motivation

The size of a martingale can be measured in two ways: by its maximal function, the largest absolute value it reaches, and by a quadratic quantity that records how much it has moved, the square function in discrete time or the elapsed time in the case of Brownian motion. The Burkholder–Davis–Gundy inequalities say that these two measurements are comparable in every $L^p$ norm and, more generally, under $E\Phi(\cdot)$ for every $\Phi$ of moderate growth. They are a basic tool of stochastic analysis, harmonic analysis and the theory of stochastic integration.

D. L. Burkholder's 1971 Wald Memorial Lectures, published as Distribution Function Inequalities for Martingales (Ann. Probability 1 (1973)), organise these results around one device: a distribution function inequality ("good- $\lambda$ " inequality) between two random variables, which a single lemma then converts into integral inequalities for all $\Phi$ of moderate growth. The paper opens its second chapter with "a particularly easy but important special case": Brownian motion stopped at an arbitrary stopping time. This mission formalizes that case, §§6–8 of the paper.

Timeline. Burkholder proved the $L^p$ square-function inequalities for martingales, $1<p<\infty$ , in 1966 (Ann. Math. Statist. 37); B. Davis extended the comparison of the maximal and square functions to $p=1$ in 1970 (Israel J. Math. 8); Burkholder and R. F. Gundy introduced the extrapolation method for operators on martingales in 1970 (Acta Math. 124); Burkholder, Davis and Gundy proved two-sided $\Phi$ inequalities in 1972 (Proc. Sixth Berkeley Symp. 2, 223–240), the Brownian case being their Theorem 7.2, under the additional assumption that $\Phi$ is the integral of a function that itself satisfies a growth condition. The 1973 paper states Theorem 6.1 below as "Theorem 7.2 of [6] with $\Phi$ more general", that assumption removed.

Setting

Let $(\Omega,\mathcal A,P)$ be a probability space and $X=\{X(t),\,0\le t<\infty\}$ a one-dimensional Brownian motion: a real process with independent increments and continuous sample functions, with $X(t)$ normally distributed, $EX(t)=0$ , $EX^2(t)=t$ . Let $\mathcal B(t)$ be the $\sigma$ -field generated by $\{X(s),\,0\le s\le t\}$ . A stopping time of $X$ is a function $\tau:\Omega\to[0,\infty]$ with $\{\tau<t\}\in\mathcal B(t)$ for every $t>0$ . For $0\le b\le\infty$ put

X^*(b)=\sup_{t\ge0}|X(b\wedge t)| ,

so $X^*(\tau)$ is the maximal function of Brownian motion stopped at $\tau$ .

A function $\Phi:[0,\infty]\to[0,\infty]$ is of moderate growth if it is non-decreasing and continuous, $\Phi(0)=0$ , and

\Phi(2\lambda)\le c_{(6.1)}\,\Phi(\lambda),\qquad\lambda>0. \tag{6.1}

Examples are $\Phi(\lambda)=\lambda^p$ for $0<p<\infty$ . No convexity is assumed. In Lean these are IsBM X P, IsStoppingTimeOf X τ, maxStopped X b ω and IsPhi Φ c.

Formalization targets

Goal: Theorem 6.1

For every stopping time $\tau$ of $X$ ,

c\,E\Phi(\tau^{1/2})\le E\Phi(X^*(\tau))\le C\,E\Phi(\tau^{1/2}), \tag{6.2}

where $c,C>0$ depend only on $c_{(6.1)}$ . Neither $\tau$ nor any moment is assumed finite.

Milestones

(8.1) Wald's identity $EX^2(\tau)=E\tau$ for a bounded stopping time $\tau$ (cited in the paper from Doob).
Theorem 6.2. For $\beta>1$ , $\delta>0$ and every $\lambda>0$ ,

P(\tau^{1/2}>\beta\lambda,\ X^*(\tau)\le\delta\lambda)\le\frac{\delta^2}{\beta^2-1}P(\tau^{1/2}>\lambda), \tag{6.3}

P(X^*(\tau)>\beta\lambda,\ \tau^{1/2}\le\delta\lambda)\le\frac{\delta^2}{(\beta-1)^2}P(X^*(\tau)>\lambda). \tag{6.4}

Lemma 7.1. If nonnegative $f,g$ satisfy $P(g>\beta\lambda,f\le\delta\lambda)\le\varepsilon P(g>\lambda)$ for all $\lambda>0$ , and $\Phi(\beta\lambda)\le\gamma\Phi(\lambda)$ , $\Phi(\delta^{-1}\lambda)\le\eta\Phi(\lambda)$ with $\gamma\varepsilon<1$ , then

E\Phi(g)\le\frac{\gamma\eta}{1-\gamma\varepsilon}E\Phi(f).

Significance

Theorem 6.1 is the Brownian case of the Burkholder–Davis–Gundy inequalities: for Brownian motion the stopping time $\tau$ plays the role of the square function, since $\tau$ is the quadratic variation of $X$ up to time $\tau$ . The result controls the stopped maximum through elapsed quadratic variation without a finite-time or integrability assumption. Lemma 7.1 is reusable: the paper applies it again in §§10–21 to discrete-time martingales.

The results are classical and proved; the mission's Lean statements remain open. Mathlib has Brownian motion as a predicate on processes (IsBrownianReal), while this development still needs optional sampling at the paper's stopping times and maximal inequalities for Brownian motion. A formal proof of this mission would provide Wald's identity at bounded optional times, a general good- $\lambda$ lemma, and the Brownian inequality with explicit dependence of the constants on $c_{(6.1)}$ .

Difficulty

The obvious route, integrating the tail bounds (6.3)–(6.4) against $d\Phi$ , does not close by itself: the right-hand side of each good- $\lambda$ inequality contains the same random variable as the left-hand side, and nothing in the hypotheses says that $E\Phi(\tau^{1/2})$ or $E\Phi(X^*(\tau))$ is finite, nor that $\tau$ is finite. The theorem has to hold in that generality, with constants that see only $c_{(6.1)}$ and not $\Phi$ itself. On the probabilistic side, the stopping times of the paper are defined by the strict events $\{\tau<t\}$ relative to the raw natural filtration $\mathcal B(t)$ , which is not right-continuous, while the one probabilistic input, Wald's identity (8.1), is a statement about optional sampling of the martingale $X^2(t)-t$ in continuous time, for which Mathlib has no theorem yet.

Formalization scope

Probability spaces are (Ω : Type) [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]; time is ℝ≥0 and stopping times are valued in ℝ≥0∞.
Brownian motion IsBM X P is Mathlib's IsBrownianReal X P plus two explicit conjuncts the paper assumes: every sample function is continuous, and each $X(t)$ is measurable (so $\mathcal B(t)\subseteq\mathcal A$ ). $X(0)=0$ holds almost surely.
IsStoppingTimeOf X τ is exactly the paper's condition $\{\tau<t\}\in\mathcal B(t)$ , $t>0$ , with $\mathcal B(t)$ the raw generated $\sigma$ -field; it is weaker than Mathlib's IsStoppingTime, so the theorems are stronger than their Mathlib-stopping-time versions.
$\tau^{1/2}$ , $X^*(\tau)$ , $\Phi$ and all expectations take values in $[0,\infty]$ (ℝ≥0∞, lintegral), with $\infty^{1/2}=\infty$ ; both sides of (6.2) may be infinite. (8.1) is stated with lintegral on both sides.
The growth condition is required for all $\lambda\in[0,\infty]$ , equivalent to (6.1) by continuity. $\Phi\not\equiv0$ , which the paper assumes "to eliminate the trivial case", is dropped: all conclusions hold trivially for $\Phi\equiv0$ .
"The choice of $c$ and $C$ depends only on $c_{(6.1)}$ " is formalized with the quantifier order ∀ c, ∃ C₁ C₂ > 0, ∀ Ω P X τ Φ, IsPhi Φ c → …. A version in which the constants are chosen after $\Phi$ , $X$ or $\tau$ would be trivial whenever the right-hand side is positive and is ruled out by this order.
In Lemma 7.1, $f,g$ may take the value $\infty$ and $\gamma,\eta$ are nonnegative; both choices are harmless (see the item notes).

Contributions welcome: Wald's identity and optional sampling for Brownian motion at optional times, the Lebesgue–Stieltjes layer-cake formula $E\Phi(h)=\int_0^\infty P(h>\lambda)\,d\Phi(\lambda)$ for continuous non-decreasing $\Phi$ (reusable for every $\Phi$ inequality of the series), and the good- $\lambda$ lemma, which the later missions of this series share.

Selected references

D. L. Burkholder, Distribution function inequalities for martingales, Ann. Probability 1 (1973), 19–42. https://doi.org/10.1214/aop/1176997023
D. L. Burkholder, B. J. Davis, R. F. Gundy, Integral inequalities for convex functions of operators on martingales, Proc. Sixth Berkeley Symp. Math. Statist. Probab. 2 (1972), 223–240. https://digicoll.lib.berkeley.edu/record/113227
D. L. Burkholder, R. F. Gundy, Extrapolation and interpolation of quasi-linear operators on martingales, Acta Math. 124 (1970), 249–304. https://doi.org/10.1007/BF02394576
B. Davis, On the integrability of the martingale square function, Israel J. Math. 8 (1970), 187–190. https://doi.org/10.1007/BF02771562
D. L. Burkholder, Martingale transforms, Ann. Math. Statist. 37 (1966), 1494–1504. https://doi.org/10.1214/aoms/1177699141

7 thms2 active usersReviewed

Completed

Harmonic Analysis Probability·Captain: mikedeng1

Distribution Function Inequalities for Martingales 6: For a Nonnegative Martingale, EΦ(S(f)) ≤ c·EΦ(f*) for Every Φ of Moderate GrowthResearch Paper

Motivation

The square function $S(f)=\big(\sum_k d_k^2\big)^{1/2}$ of a martingale $f$ with differences $d_k$ and its maximal function $f^*=\sup_n|f_n|$ are the two basic size measures of a martingale. Inequalities comparing them, $E\Phi(S(f))\le c\,E\Phi(f^*)$ and the reverse, are used throughout probability and harmonic analysis: they control stochastic sums by their quadratic variation, give $L^p$ bounds for martingale transforms, and transfer to singular integrals and area integrals in classical analysis.

D. L. Burkholder's 1971 Wald Memorial Lectures, published as Distribution Function Inequalities for Martingales (Ann. Probability 1 (1973) 19–42), organise these comparisons around distribution function (good- $\lambda$ ) inequalities. Chapter IV of the paper begins with "some of the consequences of nonnegativity". This mission formalizes one of them: for a nonnegative martingale, the square function is controlled by the maximal function in every moment of moderate growth, convex or not.

A short history of the comparison:

1966: Burkholder proves $c_p\|S(f)\|_p\le\|f\|_p\le C_p\|S(f)\|_p$ for $1<p<\infty$ (Martingale transforms, Ann. Math. Statist. 37).
1970: Burkholder and Gundy introduce good- $\lambda$ inequalities and extend the comparison of $S(f)$ and $f^*$ to $0<p<\infty$ under regularity conditions (Acta Math. 124); Davis proves the case $p=1$ for all martingales (Israel J. Math. 8).
1972: Burkholder, Davis and Gundy prove $E\Phi(S(f))\asymp E\Phi(f^*)$ for every convex $\Phi$ of moderate growth and every martingale (Proc. Sixth Berkeley Symp. 2, 223–240). The comparison fails for general martingales when $\Phi(\lambda)=\lambda^p$ with $0<p<1$ , because of large jumps (Example 8.1 of that paper; recalled in §10 of the 1973 paper, p. 29).
1973: Theorem 18.3 of the present paper shows that for nonnegative martingales one direction, $E\Phi(S(f))\le c\,E\Phi(f^*)$ , holds for every $\Phi$ of moderate growth.

Setting

Let $(\Omega,\mathcal A,P)$ be a probability space and $\mathcal A_0\subseteq\mathcal A_1\subseteq\cdots$ a filtration. A nonnegative martingale is a sequence $f=(f_1,f_2,\dots)$ of integrable random variables with $f_n\ge0$ , $f_n$ measurable with respect to $\mathcal A_n$ , and $E(f_{n+1}\mid\mathcal A_n)=f_n$ . With $f_0=0$ , its difference sequence is $d_k=f_k-f_{k-1}$ , $k\ge1$ . The objects compared are

S(f)=\Big(\sum_{k=1}^\infty d_k^2\Big)^{1/2}\in[0,\infty],\qquad f^*=\sup_{n\ge1}|f_n|\in[0,\infty].

In Lean these are sqFn f and maxFn f; the finite versions $S_n(f)$ and $f_n^*$ are sqFnN f n and maxFnN f n.

For $\lambda>0$ , the exit time $\mu=\inf\{n\ge1:|f_n|>\lambda\}$ (with $\inf\emptyset=\infty$ ) is exitTime f λ, and $S_{\mu-1}(f)$ , the square function of $f$ stopped just before it first exceeds $\lambda$ , is sqFnAt f (exitTime f λ - 1), with $S_0(f)=0$ and $S_\infty(f)=S(f)$ .

A function $\Phi:[0,\infty]\to[0,\infty]$ satisfies the conditions of Section 7 (IsPhi Φ c) if it is non-decreasing and continuous, $\Phi(0)=0$ , and it has moderate growth:

\Phi(2\lambda)\le c\,\Phi(\lambda),\qquad\lambda>0.\tag{6.1}

The powers $\Phi(\lambda)=\lambda^p$ , $0<p<\infty$ , are the model examples.

Formalization targets

Goal: Theorem 18.3 (p. 36)

For every growth constant $c_{(6.1)}$ there is $c$ , depending only on $c_{(6.1)}$ , such that for every nonnegative martingale $f$ and every $\Phi$ satisfying the conditions of Section 7,

E\Phi(S(f))\le c\,E\Phi(f^*).

The goal fixes no value of the constant, so it is the statement that survives any later improvement of $c$ .

Milestones

Lemma 2.1 (p. 21): for $f$ a martingale or nonnegative submartingale with $\|f\|_1<\infty$ ,

\|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. 2. (18.5) (p. 37): for a nonnegative martingale and $a>0$ ,

\int_{a+\lambda^2}^\infty P\big(S^2_{\mu-1}(f)>s\big)\,ds\le2\lambda^2P\big(S^2_{\mu-1}(f)>a\big).

The stopped inclusion (proof of Theorem 18.2, p. 37): with $\mu$ the exit time above $\delta\lambda$ ,

P\big(S(f)>\beta\lambda,\ f^*\le\delta\lambda\big)\le P\big(S_{\mu-1}(f)>\beta\lambda\big).

Theorem 18.2 (p. 35): for $\beta>1$ , $0<\delta<(\beta^2-1)^{1/2}$ and a nonnegative martingale,

P\big(S(f)>\beta\lambda,\ f^*\le\delta\lambda\big)\le\frac{2\delta^2}{\beta^2-\delta^2-1}\,P\big(S(f)>\lambda\big),\qquad\lambda>0.

Lemma 7.1 (p. 26): a good- $\lambda$ inequality $P(g>\beta\lambda,f\le\delta\lambda)\le\varepsilon P(g>\lambda)$ , with $\Phi(\beta\lambda)\le\gamma\Phi(\lambda)$ , $\Phi(\delta^{-1}\lambda)\le\eta\Phi(\lambda)$ and $\gamma\varepsilon<1$ , gives $E\Phi(g)\le\frac{\gamma\eta}{1-\gamma\varepsilon}E\Phi(f)$ .

Significance

The result. Theorem 18.3 removes the convexity hypothesis from one half of the Burkholder–Davis–Gundy comparison, at the price of nonnegativity. It covers the concave powers $\lambda^p$ , $0<p<1$ , and every other $\Phi$ of moderate growth, including those that are neither convex nor concave. Nonnegative martingales are the natural objects in likelihood ratios, branching processes and Radon–Nikodym densities. For $\Phi(\lambda)=\lambda^p$ , $1<p<\infty$ , the paper derives from Theorem 18.2 and Lemma 7.1 the bound $\|S(f)\|_p\le cp^{1/2}\|f^*\|_p$ with the order $p^{1/2}$ in the constant (p. 37). Theorem 18.2 is the distribution function inequality behind the theorem and is itself a sharper statement than any moment inequality it yields.

Formalizing it. The result is proved in the paper. As far as is known it has no machine-checked proof, and Mathlib has neither the martingale square function nor any good- $\lambda$ machinery. A formalization produces reusable components: the square function and stopped square function of a discrete martingale, Lemma 2.1, and Lemma 7.1, which is shared by every $\Phi$ inequality in the paper and many outside it.

Difficulty

For general martingales, a good- $\lambda$ inequality bounding $P(S(f)>\beta\lambda,\ f^*\le\delta\lambda)$ by a small multiple of $P(S(f)>\lambda)$ is false: a single large jump $d_k$ can make $S(f)$ large while the martingale is stopped before $f^*$ grows, which is why the general results need convexity or a jump bound. The first idea, transferring the convex case of Burkholder–Davis–Gundy, does not work for concave $\Phi$ : the convex proof uses convexity of $\Phi$ in an essential way (Lemma 16.1 of the paper), and for general martingales the conclusion itself is false for $\lambda^p$ , $p<1$ . A bound on $E S^2_{\mu-1}(f)$ alone, as in Lemma 2.1, is also not enough; the good- $\lambda$ inequality needs control of the tail of $S^2_{\mu-1}(f)$ above every level $a$ , which is where nonnegativity enters. Passing from the distribution inequality to all $\Phi$ at once also requires care with infinite values of $S(f)$ and $f^*$ .

Formalization scope

Martingales. Mathlib's Martingale f ℱ P with f : ℕ → Ω → ℝ and ℱ : Filtration ℕ mΩ, ℱ k = 𝒜_k. Statements read f n only for $n\ge1$ , with the paper's $f_0=0$ ; Mathlib's additional constraint at index $0$ is no restriction, since any martingale relative to $\mathcal A_1,\mathcal A_2,\dots$ extends to one by $f_0:=E(f_1\mid\mathcal A_0)$ . Nonnegativity is "almost surely, for $n\ge1$ ".
Values in $[0,\infty]$ . $S(f)$ , $f^*$ , $S_{\mu-1}(f)$ , $\Phi$ and all expectations $E\Phi(\cdot)$ are ℝ≥0∞-valued (∫⁻), so both sides of the goal may be infinite and no junk value $0$ arises from a non-integrable function.
$\Phi$ . IsPhi Φ c imposes the growth condition at every $x\in[0,\infty]$ , which is equivalent to (6.1) for $\lambda>0$ . The paper's exclusion of $\Phi\equiv0$ is dropped (the inequalities are trivial then). No convexity is assumed anywhere in this mission.
Constants. The goal quantifies ∀ c, ∃ C > 0, ∀ Ω P ℱ f Φ, with $\Omega$ in Type: the constant may depend on $c_{(6.1)}$ only, never on $\Phi$ , $f$ or $P$ . A constant chosen after the data would make the goal trivial whenever its right-hand side is positive; that reading is ruled out by the quantifier order.
Theorem 18.2 states $\delta<(\beta^2-1)^{1/2}$ with Real.sqrt; with $\delta>0$ this is $\beta^2-\delta^2-1>0$ .
Lemma 2.1 takes the almost-everywhere limit $f_\infty$ as a supplied function with a convergence hypothesis; $\mu-1$ is truncated subtraction on $\{1,\dots,\infty\}$ with $\infty-1=\infty$ .
Lemma 7.1 allows $f,g$ to take the value $\infty$ (needed for $g=S(f)$ , $f=f^*$ ) and takes $\gamma,\eta\ge0$ , which loses nothing since (7.2) forces $\gamma,\eta\ge1$ unless $\Phi\equiv0$ .

The shared definitions file declares the series-wide layer (including $s(f)$ , convexity and concavity predicates used by other missions of the series). Proofs of any milestone are welcome, as are auxiliary lemmas on the stopped square function, on the Stieltjes representation $E\Phi(h)=\int_0^\infty P(h>\lambda)\,d\Phi(\lambda)$ , and on the layer-cake formula in ℝ≥0∞.

Selected references

D. L. Burkholder, Distribution function inequalities for martingales, Ann. Probability 1 (1973), 19–42. https://doi.org/10.1214/aop/1176997023
D. L. Burkholder, Martingale transforms, Ann. Math. Statist. 37 (1966), 1494–1504. https://doi.org/10.1214/aoms/1177699141
D. L. Burkholder and R. F. Gundy, Extrapolation and interpolation of quasi-linear operators on martingales, Acta Math. 124 (1970), 249–304. https://doi.org/10.1007/BF02394573
B. Davis, On the integrability of the martingale square function, Israel J. Math. 8 (1970), 187–190. https://doi.org/10.1007/BF02771313
D. L. Burkholder, B. J. Davis and R. F. Gundy, Integral inequalities for convex functions of operators on martingales, Proc. Sixth Berkeley Symp. Math. Statist. Prob. 2 (1972), 223–240. https://doi.org/10.1525/9780520423671-018

7 thms2 active usersReviewed

Completed

Harmonic Analysis Probability·Captain: mikedeng1

Distribution Function Inequalities for Martingales 5: A Nonnegative Martingale's Square Function, Stopped Before |f_n| Exceeds λ, Is Exponentially Square IntegrableResearch Paper

Motivation

Martingale estimates describe how a process built from successive, conditionally fair increments can fluctuate. A basic object is its square function: the square root of the sum of the squared increments along a sample path. Square functions are useful because they record accumulated variation even when positive and negative increments cancel in the martingale itself. Burkholder's 1973 lectures study the distributions of square functions and maximal functions and compare their moments under several kinds of hypotheses (Burkholder 1973, §1).

The present mission concerns a sharper phenomenon for a nonnegative martingale. If the process is stopped just before its absolute value first exceeds a fixed threshold, the resulting square function has an exponential moment of its square. The distinction matters: a second moment controls one scale of variation, while an exponential square moment controls a range of larger deviations. Burkholder states the second-moment stopped estimate in Lemma 2.1 and the exponential estimate in Theorem 18.1 (Burkholder 1973, pp. 21, 35).

Setting

Let $(\Omega,\mathcal A,P)$ be a probability space with an increasing sequence of sub- $\sigma$ -fields $\mathcal A_0,\mathcal A_1,\ldots$ . A martingale $f=(f_n)_{n\ge1}$ is observed relative to $\mathcal A_1,\mathcal A_2,\ldots$ . Burkholder sets $f_0=0$ for the purpose of defining its difference sequence: $d_1=f_1$ and $d_k=f_k-f_{k-1}$ for $k\ge2$ . For each $n\ge0$ let

S_n(f)=\left(\sum_{k=1}^{n}d_k^2\right)^{1/2}, \qquad S(f)=\sup_{n\ge0}S_n(f), \qquad S_0(f)=0.

Fix $\lambda>0$ . The exit time is $\mu=\inf\{n\ge1:|f_n|>\lambda\}$ , with $\mu=\infty$ if the set is empty. The quantity in this mission is $S_{\mu-1}(f)$ . On a path with $\mu=n<\infty$ it includes differences only through $n-1$ ; on a path with $\mu=\infty$ it is $S(f)$ . Nonnegative means $f_n\ge0$ almost surely for every $n\ge1$ . These conventions are those of §§1, 2 and 18 of the paper (Burkholder 1973, pp. 20–21, 35).

Formalization targets

The goal is Theorem 18.1. For every nonnegative martingale and every $\lambda>0$ , $S_{\mu-1}(f)$ is finite almost everywhere and

E\exp\left(tS_{\mu-1}(f)^2\right) \le \frac{1}{1-3t\lambda^2}, \qquad 0<t<\frac{1}{3\lambda^2}.

The constant $3$ and the full range of $t$ are part of the target; replacing the claim by the existence of one positive exponential parameter would lose the paper's quantitative conclusion (Burkholder 1973, Theorem 18.1, p. 35).

The milestone path contains four statements from the paper. Lemma 2.1 bounds the second moment of the stopped square function and stopped value. Display (18.5) bounds an integrated tail past $a+\lambda^2$ by $2\lambda^2$ times the tail at $a$ . The paragraph following it gives the full integrated-tail bound with $3\lambda^2$ . Lemma 18.1 converts an integrated-tail condition for a nonnegative measurable function into an exponential moment estimate. The milestone order follows their role in Theorem 18.1, while the tail-to-moment lemma also stands independently of martingales (Burkholder 1973, pp. 21, 36–37).

Significance

The theorem gives a uniform quantitative bound for the square function accumulated before a nonnegative martingale crosses $\lambda$ . It strengthens the $L^2$ conclusion available from Lemma 2.1 under $L^1$ boundedness. The tail-to-moment lemma has a second use later in the paper: Burkholder invokes it for the square function of a martingale satisfying a bounded conditional-tail condition in Theorem 19.1 (Burkholder 1973, §§18–19).

The mathematical result is proved in the paper. This mission asks for a machine-checked development of its precise statements. That development would make the stopped square function, its exit-time convention, the integrated-tail estimates and the exponential-moment implication available as individually reusable objects. No machine-checked proof of these statements is known on Prove2Me; the related martingale inequalities already there (Doob's $L^p$ maximal inequality, an $L^p$ bound for Robbins–Monro noise sums) have different data and conclusions.

Difficulty

The first obvious estimate, Lemma 2.1, gives a second moment but does not by itself give an exponential moment. The exit time also depends on the same martingale path whose variation is being measured, so a fixed-time estimate does not immediately describe $S_{\mu-1}(f)$ . Nonnegativity is essential to the stronger statement: the paper contrasts the general $L^1$ -bounded case, where it states only $L^2$ control, with the nonnegative case, where it asserts exponential square integrability (Burkholder 1973, pp. 21, 35).

Formalization scope

Lean uses Mathlib's filtration and martingale predicates for a real-valued process indexed by natural numbers. The paper starts at index $1$ and fixes $f_0=0$ only in its difference sequence. Mathlib's martingale predicate also constrains an auxiliary value at index $0$ ; any paper martingale can be extended there by a conditional expectation. Every square function and exit time in this mission ignores that auxiliary value. Nonnegativity is almost everywhere at each positive index. The convergence value $f_\infty$ in Lemma 2.1 is supplied with an almost-everywhere convergence hypothesis, recording explicitly the convergence that follows from the paper's $L^1$ boundedness assumption.

Square functions, norms, tail probabilities and their nonnegative integrals take values in $[0,\infty]$ . This represents a genuinely infinite square function without a default real-valued supremum. At $\mu=\infty$ , subtraction of one in $\mathbb N_\infty$ leaves $\infty$ , as the paper intends. The exponential-moment statements assert almost-everywhere finiteness before converting an extended value to a real exponent; otherwise the conversion of $\infty$ to zero could make a false bound look true. The threshold $\lambda$ is positive, and the same $\lambda$ appears in the stopping time and in every bound.

The shared definition layer also records the paper's maximal function, $L^p$ norm, conditional square function and class of functions $\Phi$ of moderate growth for reuse across this nine-mission series. The conditional square function uses generalized nonnegative conditional expectation. Its $\Phi$ condition includes the endpoints $0$ and $\infty$ ; these add no restriction under the paper's continuity and zero-at-zero conventions. The zero function $\Phi$ is allowed, since the inequalities in which it appears then hold trivially. Contributions establishing the four milestones, the needed stopping-time measurability facts, or the goal theorem are within scope. A version that assumes the desired exponential moment, or replaces $S_{\mu-1}(f)$ by a fixed-time square function, would miss the target.

Selected references

D. L. Burkholder, Distribution Function Inequalities for Martingales, The Annals of Probability 1(1), 1973, pp. 19–42. DOI: 10.1214/aop/1176997023.

6 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Vertical Integration and Antitrust Policy: Integrating Successive Monopolies Lowers the Final Price and Raises Output, Joint Profit and Consumer SurplusResearch Paper

Motivation

In 1950 the United States Supreme Court appeared to be moving toward treating corporate integration, horizontal or vertical, as illegal per se under the antitrust laws. Joseph J. Spengler's note in the Journal of Political Economy argued that this conflates two different things: horizontal integration can suppress competition, but vertical integration, the joining of successive stages of production under one owner, can lower prices when the stages are already imperfectly competitive. The note is the standard origin of what industrial organization now calls double marginalization: when a monopolist upstream sells to a monopolist downstream, each adds its own markup, and the final price is higher than a single integrated monopolist would charge.

The argument underlies the modern economics of vertical mergers and vertical restraints (resale price maintenance, two-part tariffs, franchise fees) and the supply-chain coordination literature in operations research, where a wholesale-price contract between a supplier and a retailer reproduces the same distortion.

A short timeline: Cournot (1838, Chapter IX) analysed complementary monopolists selling inputs to a common product; Spengler (1950) gave the successive-monopoly version and drew the antitrust conclusion; Tirole's textbook (1988, §4.2) made it the canonical example of vertical externalities; Cachon and Lariviere (2005) and the coordination literature studied the same inefficiency in newsvendor supply chains.

Setting

A product passes through three successive stages $A\to B\to C$ before reaching consumers. Production uses fixed proportions: one unit of stage A's product goes into one unit of B's, and one unit of B's into one unit of C's, so all stages handle the same quantity. Each stage has a constant unit variable cost $V_a,V_b,V_c$ (marginal cost equal to average variable cost at every relevant output).

Final demand is a function $D:\mathbb R\to\mathbb R$ : $D(p)$ units of $C$ are bought at price $p$ . A firm with constant unit cost $c$ that sells at price $p$ earns the profit (return above variable outlay)

\pi_c(p)=(p-c)\,D(p),

and $p$ is a profit-maximizing price at cost $c$ when $\pi_c(x)\le\pi_c(p)$ for every $x$ .

Unintegrated chain. Stage A sells to B at a transfer price $P_a$ , B sells to C at $P_b$ . Their per-unit profits are $R_a=P_a-V_a$ and $R_b=P_b-(V_b+P_a)$ ; horizontal integration within each stage lets these be positive "monopolistic surcharges". Stage C's unit cost is $C_c=V_c+P_b$ ; it charges a profit-maximizing price $P_c$ at that cost and sells $Q=D(P_c)$ . The chain's aggregate profit is $R_aQ+R_bQ+R_cQ$ with $R_c=P_c-(V_c+P_b)$ .

Integrated firm. One firm owns all three stages. Its unit cost is $C'_c=V_a+V_b+V_c$ ; it charges a profit-maximizing price $P'_c$ at that cost and sells $Q'=D(P'_c)$ , earning $(P'_c-C'_c)\,Q'$ .

The price elasticity of demand at $p$ is $e(p)=-p\,D'(p)/D(p)$ (positive for a downward-sloping curve) and the marginal revenue is $r(p)=p+D(p)/D'(p)$ . The consumers' surplus gained when the price falls from $P_c$ to $P'_c$ is $\int_{P'_c}^{P_c}D(x)\,dx$ .

Formalization targets

Goal: vertical integration benefits producer and consumer

For every non-increasing demand curve $D$ , all unit costs $V_a,V_b,V_c$ , and all transfer prices with $R_a>0$ , $R_b>0$ , if $P_c$ is profit-maximizing at cost $V_c+P_b$ , $P'_c$ is profit-maximizing at cost $V_a+V_b+V_c$ , $D$ is differentiable at $P_c$ and $Q=D(P_c)>0$ , then

P'_c<P_c,\qquad D(P_c)<D(P'_c),\qquad R_aQ+R_bQ+R_cQ<(P'_c-C'_c)\,Q',

0<\int_{P'_c}^{P_c}D(x)\,dx,\qquad Q\,(P_c-P'_c)\le\int_{P'_c}^{P_c}D(x)\,dx.

The goal fixes no functional form and no numbers; it is the general statement behind the paper's "under all cases conceivable … within the framework here employed".

Milestones

Footnote 6, equilibrium identities. At a profit-maximizing price, $r=c$ , $e=p/(p-r)=p/(p-c)$ , and $p=c\,e/(e-1)$ when $c\ne0$ .
Section III, unitary elasticity. At zero cost, $e=1$ ; at positive cost, $p>c$ and $e>1$ .
Section III, cost raises price. For $c_1<c_2$ , profit-maximizing prices satisfy $D(p_2)\le D(p_1)$ , and $p_1<p_2$ under the goal's regularity hypotheses.
Footnote 6, straight-line demand. For $D(p)=b(a-p)$ : $p^*(c)=(a+c)/2$ , $\Delta r=2\Delta p$ , $e(p^*(c))=(a+c)/(a-c)$ , the elasticity rises relatively more than the price, and the relative rise grows with $c$ .
Figure 1. With $D_c(p)=\tfrac85(140-p)$ and $V_a=V_b=V_c=20$ : $P_c=115$ , $Q=40$ , aggregate profit $2{,}200$ ; $P'_c=100$ , $Q'=64$ , profit $2{,}560$ ; consumers' surplus rises by $780$ .

Significance

The result. The theorem shows that removing an upstream markup can only lower the final price and raise output, so that producers and consumers gain together. This is the economic content of the rule that vertical integration is not anticompetitive as such, and it is the reason modern merger guidelines credit the "elimination of double marginalization" as an efficiency of vertical mergers. Milestone 3, monotonicity of the monopoly price in cost, is the general comparative-statics fact used in tax incidence and cost pass-through.

Formalizing it. The result is classical and proved in every industrial-organization textbook, usually for linear demand. The mission states it for an arbitrary non-increasing demand curve, without concavity, continuity or uniqueness of the profit maximizer, which makes explicit which hypotheses the strict conclusions actually need. Related items on the platform formalize double marginalization in a different model, the newsvendor wholesale-price contract of Cachon and Lariviere, where the supplier-induced order quantity falls short of the integrated one; this mission covers the price-setting, deterministic-demand version.

Difficulty

The weak inequalities ( $P'_c\le P_c$ , $Q\le Q'$ , profit $\le$ ) follow from comparing the two maximization problems (the price comparison also uses $Q>0$ : if $D\equiv 0$ , every price is profit-maximizing). The strict inequalities do not: a demand curve with a kink can have the same profit-maximizing price at two different costs, so integration need not change the price at all. The strict claims therefore need a first-order condition at $P_c$ , and the argument has to combine global optimality (all prices) with local information (a derivative at one point) without assuming the profit function is concave or the maximizer unique. The consumers'-surplus clause requires a lower bound on an integral of a monotone, possibly discontinuous function.

Formalization scope

Prices, costs and quantities are real numbers; maximization is over all prices $p\in\mathbb R$ . Demand is a function $D:\mathbb R\to\mathbb R$ ; the goal assumes only that it is non-increasing (Antitone D).
Profit-maximizing prices are hypotheses (IsProfitMax D c p), never closed forms; the closed form $(a+c)/2$ appears only for straight-line demand.
The transfer prices $P_a,P_b$ are arbitrary data with positive markups; they need not be profit-maximizing for $D_a,D_b$ , which the paper draws only in its figure.
Explicit readings of the paper's prose. "Benefits both producer and consumer" and "will lower the price" become the four strict inequalities of the goal. "Aggregate profit" is the sum over the three stages, $Q[P_c-(V_a+V_b+V_c)]$ , not stage C's profit alone. Consumers' surplus "in the Marshallian sense" is the interval integral of $D$ between the two prices; footnote 5's trapezoid formula is used only for the straight line of Figure 1. Elasticity is a positive number $-pD'(p)/D(p)$ . "Relatively greater increment in the elasticity" is made exact for straight-line demand as $e(p^*(c'))/e(p^*(c))>p^*(c')/p^*(c)$ ; the literal $\Delta e/e>\Delta c/c$ is false for small $c$ . Footnote 6's $e'=(p+\Delta p)/(p-2\Delta p)$ and "approximating $3\Delta p/p$ " are a printed slip; the exact $e(p^*(c))=(a+c)/(a-c)$ is stated instead, and no approximation is formalized. Figure 1's demand line $D_c(p)=\tfrac85(140-p)$ is the line through the three points the text gives.
Added hypotheses. Differentiability of $D$ at $P_c$ and $D(P_c)>0$ , which the paper's marginal-revenue reasoning presupposes. Every statement involving elasticity or marginal revenue carries differentiability and positive demand, because Lean's deriv and division return $0$ on bad input.
Ruled out. Formalizations that hard-code linear demand in the goal, compare the integrated profit with stage C's profit alone, or prove only the weak ( $\le$ ) inequalities do not capture the result.
Sections IV and the policy remarks of Section III (rent evasion, taxes, co-operatives) are not formalized.
Only Mathlib is needed: Fermat's rule (IsLocalMax.hasDerivAt_eq_zero), interval integrals of monotone functions, and real arithmetic. Proofs of the general milestones are reusable for any monopoly-pricing comparative statics.

Selected references

J. J. Spengler, Vertical integration and antitrust policy, Journal of Political Economy 58(4), 1950, 347–352. https://doi.org/10.1086/256964
A. A. Cournot, Recherches sur les principes mathématiques de la théorie des richesses, Hachette, 1838, Chapter IX.
J. Tirole, The Theory of Industrial Organization, MIT Press, 1988, §4.2.
G. P. Cachon and M. A. Lariviere, Supply chain coordination with revenue-sharing contracts: strengths and limitations, Management Science 51(1), 2005, 30–44. https://doi.org/10.1287/mnsc.1040.0215

7 thms2 active usersReviewed

Combinatorics Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces V: The Convex Hull Distance — ∫ exp f_α(A,x) dP ≤ P(A)^{−α}Textbook

Motivation

A product probability space $(\Omega^N, P)$ , $P=\mu^{\otimes N}$ , concentrates its mass: a set $A$ of non-negligible measure is "close" to most points. How closeness is measured decides what the statement can be used for. The Hamming distance (Chapter 2 of the paper) counts coordinates in which a point differs from $A$ ; it gives Gaussian concentration, but only for functions that are Lipschitz for one fixed weighting of the coordinates. Chapter 4 of M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces (Publ. Math. IHÉS 81, 1995), introduces the convex hull distance, which controls every weighted Hamming distance at once with weights chosen after seeing the point. This one inequality is what the second half of the paper uses for the longest increasing subsequence, bin packing, suprema of linear forms, the chromatic number of random graphs, the random assignment problem and the travelling salesman problem, and it is the form in which "Talagrand's inequality" is usually quoted in probability and combinatorics.

History (paper, p. 125). The author first proved the deviation inequality of Theorem 13.2 of the paper for symmetric $\pm1$ variables; W. B. Johnson and G. Schechtman extended it, and their one-dimensional lemma (Lemma 4.1.3 here) led to the abstract setting of Theorem 4.1.1. Section 4.2 sharpens the exponent $1/4$ by replacing $f_c^2/4$ with an exactly optimised penalty $f_\alpha$ .

Setting

Let $(\Omega,\mu)$ be a probability space, $N\ge0$ an integer and $P=\mu^{\otimes N}$ on $\Omega^N$ . For $A\subseteq\Omega^N$ and $x\in\Omega^N$ let

U_A(x)=\{(s_i)_{i\le N}\in\{0,1\}^N;\ \exists y\in A,\ s_i=0\Rightarrow x_i=y_i\},

the set of $0$ – $1$ vectors marking a superset of the coordinates in which $x$ differs from some point of $A$ . Let $V_A(x)$ be its convex hull in $\mathbb R^N$ ; it contains $0$ exactly when $x\in A$ . The convex hull distance $f_c(A,x)$ is the Euclidean distance from $0$ to $V_A(x)$ , and the enlargement of $A$ is

A_t^c=\{x\in\Omega^N;\ f_c(A,x)\le t\}

(the superscript $c$ stands for "convexity", not for a complement). For $\alpha\ge0$ and $u\in[0,1]$ put

\xi(\alpha,u)=\alpha(1-u)\log(1-u)-(\alpha+1-\alpha u)\log\Big(\frac{1+\alpha-\alpha u}{1+\alpha}\Big),

and let $f_\alpha(A,x)=\inf\{\sum_{i\le N}\xi(\alpha,s_i);\ s\in V_A(x)\}$ ; it plays the role of $f_c^2(A,x)$ .

Formalization targets

Goal: Theorem 4.2.4

For $\alpha>0$ and every $A\subseteq\Omega^N$ ,

\int\exp f_\alpha(A,x)\,dP(x)\le\frac{1}{P(A)^{\alpha}}.

The constant is exact (no unspecified constants), and the statement holds for every probability space $\Omega$ and every $N$ .

Milestones

Lemma 4.1.2: $x\in A_t^c$ iff for every real $(\alpha_i)$ some $y\in A$ has $\sum\{\alpha_i;\ x_i\ne y_i\}\le t(\sum\alpha_i^2)^{1/2}$ .
Lemma 4.1.3: $\inf_{0\le\lambda\le1}r^{-\lambda}\exp\frac{(1-\lambda)^2}{4}\le2-r$ for $0\le r\le1$ .
Lemma 4.2.1: $\inf_{0\le\lambda\le1}r^{-\lambda\alpha}\exp\xi(\alpha,1-\lambda)=1+\alpha-\alpha r$ for $0<r<1$ .
Lemma 4.2.2: $\xi(\alpha,\cdot)$ is increasing and convex on $[0,1]$ and $\xi(\alpha,u)\ge\frac{\alpha}{2(\alpha+1)}u^2$ .
Lemma 4.2.3: $1+\alpha-\alpha a\le a^{-\alpha}$ and $a+(1-a)\exp\xi(\alpha,1)\le a^{-\alpha}$ .
Eq. (4.2.6): $P(A_t^c)\ge1-P(A)^{-\alpha}\exp\big(-\frac{\alpha t^2}{2(\alpha+1)}\big)$ .
Corollary 4.2.5: for $t\ge\sqrt{2\log(1/P(A))}$ , $P(A_t^c)\ge1-\exp\big(-\frac12(t-\sqrt{2\log(1/P(A))})^2\big)$ .
Theorem 4.3.1 (two-point space, uniform $\mu$ , $\alpha\ge1$ ): $\int\exp\big(\frac{\alpha}{\alpha+1}f_c^2(A,x)\big)\,dP(x)\le P(A)^{-\alpha}$ .

Significance

The result. At $\alpha=1$ , Lemma 4.2.2 gives $\xi(1,u)\ge u^2/4$ , so the goal contains Theorem 4.1.1,

\int\exp\tfrac14f_c^2(A,x)\,dP(x)\le\frac1{P(A)},\qquad P(A_t^c)\ge1-\frac1{P(A)}e^{-t^2/4},

the convex distance inequality itself. For general $\alpha$ it improves the coefficient of $t^2$ from $1/4$ to the optimal $1/2$ (Corollary 4.2.5), and since $\xi(\alpha,1)=\log(1+\alpha)$ grows with $\alpha$ , it simultaneously controls the number of coordinates in which $x$ must be changed to reach $A$ , recovering features of the $q$ -point inequalities of Chapter 3. Every Part II application of the paper rests on Theorem 4.1.1 or on this sharpening.

Formalizing it. All results here are proved in the paper (the goal's proof is "an obvious adaptation" of that of Theorem 4.1.1, by induction on $N$ ). None of them has a machine-checked proof for a general probability space. Theorem 4.1.1 itself is posed on the platform, still open, for finite alphabets and finite sets (Talagrand.Eexp_mul_mass_le_one, Talagrand.mass_mul_mass_le_exp); it is not posed again here. A proof of the goal settles it for arbitrary $\Omega$ and arbitrary measurable $A$ .

Difficulty

The function $x\mapsto f_\alpha(A,x)$ is not a sum of one-coordinate terms, so no tensorization of a one-dimensional inequality applies directly. Bounding $f_\alpha(A,x)$ pointwise by the distance to a single nearby point of $A$ gives only Hamming-type bounds with a fixed weighting, which is exactly what the convex hull distance is designed to beat; the inequality has to hold for the infimum over the whole hull. The one-coordinate estimate the paper uses is the exact identity of Lemma 4.2.1, which leaves no slack. A further obstacle is analytic: $V_A(x)$ is a convex hull in $\mathbb R^N$ of a set indexed by the possibly uncountable set $A$ , and its infima must be compared across dimensions $N$ and $N+1$ .

Formalization scope

$\Omega^N$ is Fin N → Ω; $P$ is Measure.pi (fun _ : Fin N => μ) with IsProbabilityMeasure μ.
$U_A(x)$ is a set of Fin N → ℝ with values in $\{0,1\}$ ; $V_A(x)$ is convexHull ℝ (U A x). The $\ell^2$ norm is written out as $\sqrt{\sum_i s_i^2}$ : Mathlib's norm on Fin N → ℝ is the sup norm.
$f_c$ and $f_\alpha$ take values in $[0,\infty]$ (ℝ≥0∞); both are $+\infty$ when $A=\varnothing$ . $\exp(+\infty)=+\infty$ (EReal.exp), $P(A)^{-\alpha}=+\infty$ when $P(A)=0$ . No real-valued infimum or Bochner integral is used, so no junk value can make a bound hold for free.
$\xi(\alpha,1)=\log(1+\alpha)$ relies on $0\cdot\log0=0$ , which Mathlib's Real.log 0 = 0 provides.
Measurability. The paper ignores measurability (pp. 81–82). Here $A$ and $x\mapsto f_\alpha(A,x)$ are assumed measurable (explicit hypotheses), integrals are ∫⁻, and $P(A_t^c)$ is the measure of an arbitrary set, i.e. its outer probability, as the paper prescribes.
$\alpha>0$ in the goal; $t\ge0$ for the enlargement; $P(A)>0$ in Corollary 4.2.5, where the paper's hypothesis on $t$ is otherwise unsatisfiable. In §4.3, $\Omega=\{0,1\}$ is Bool with PMF.uniformOfFintype.
A trivializing formalization is ruled out: restricting $\Omega$ to a finite type or $A$ to a finite set would give a strictly weaker statement (and the finite case of Theorem 4.1.1 is already posed elsewhere).
Needed infrastructure: convex hulls of $0$ – $1$ vectors and their behaviour under adding a coordinate, Hölder's inequality for ∫⁻, Fubini for Measure.pi on Fin (N+1), and the one-variable calculus of $\xi$ . The definitions module is the substrate the Part II chapters of the paper use; proofs of the one-variable lemmas and of the induction step are welcome independently.
Corollary 4.3.2 is not included: the paper derives it from Theorem 4.3.1 by optimising over $\alpha\ge1$ , which only covers $t\ge2\sqrt{\log(1/P(A))}$ , and the printed range $t\ge\sqrt{\log(1/P(A))}$ is not established on the page.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. https://doi.org/10.1007/BF02699376

10 thms2 active usersReviewed

Completed

Combinatorics Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces I: Control by One Point — ∫ e^{t f(A,x)} dP ≤ P(A)^{−α} exp(Nt²(1+1/α)/8) for the Hamming Distance to ATextbook

Motivation

Concentration of measure is the observation that, on a high-dimensional product probability space, any set that is not too small already contains most of the space within a small neighbourhood. For functions of many independent random variables this yields Gaussian-type tail bounds without any explicit computation of the distribution, and these bounds are the working tool behind the analysis of random combinatorial optimisation problems (bin packing, the travelling salesman problem, the longest increasing subsequence, the assignment problem), random graphs, and empirical processes.

M. Talagrand's 1995 memoir Talagrand 1995 develops a family of such inequalities that hold on an arbitrary product of probability spaces and are proved by induction on the number of coordinates. Chapter 2 opens with the simplest instance, control by one point: the distance from $x$ to a set $A$ is measured by the number of coordinates in which $x$ differs from the best single point $y \in A$ . The method of this chapter is the template for every later chapter of the memoir.

Timeline. Bounds of the form (2.2.7) for the Hamming distance were first obtained with martingale (bounded differences) methods, collected in McDiarmid's survey McDiarmid 1989. Talagrand's 1995 memoir gives the induction proof reproduced here, with exponent $-\tfrac2N(k-\sqrt{\tfrac N2\log\tfrac1{P(A)}})^2$ , which the paper notes is exactly the best bound obtained by martingales. Earlier, the isoperimetric inequality on the discrete cube (Harper, 1966) settles the case of the uniform measure on $\{0,1\}^N$ .

Setting

Let $(\Omega,\Sigma,\mu)$ be a probability space and $N \ge 0$ an integer. Points of the product $\Omega^N$ are written $x=(x_1,\dots,x_N)$ , and $P=\mu^N$ denotes the product probability. For a set $A \subseteq \Omega^N$ and a point $x$ , the Hamming distance to $A$ is

f(A,x)=\min\big\{\operatorname{card}\{i\le N:\ x_i\ne y_i\}\ :\ y\in A\big\},

the least number of coordinates that must be changed to move $x$ into $A$ ; it is $+\infty$ when $A$ is empty. Given positive weights $(a_i)_{i\le N}$ , the weighted Hamming distance replaces the count by $\sum\{a_i: x_i\neq y_i\}$ .

Two families of constants appear. The first is

a(t)=\frac12+\frac{e^t+e^{-t}}4 ,

and the second, for $\alpha>0$ and $t>0$ ,

a(\alpha,t)=\frac{\alpha^{\alpha}}{(\alpha+1)^{\alpha+1}}\,\frac{(e^t-e^{-t/\alpha})^{1+\alpha}}{(1-e^{-t/\alpha})(e^t-1)^{\alpha}},

extended by its limit $a(\alpha,0)=1$ ; one checks $a(1,t)=a(t)$ .

Formalization targets

Goal: Corollary 2.2.3

For every measurable $A\subseteq\Omega^N$ , every $\alpha>0$ and every $t\ge0$ ,

\int e^{t f(A,x)}\,dP(x)\ \le\ \frac{1}{P(A)^{\alpha}}\exp\Big(N\frac{t^2}{8}\Big(1+\frac1\alpha\Big)\Big), \tag{2.2.6}

and, when $P(A)>0$ , for every $k\ge\sqrt{\tfrac N2\log\tfrac1{P(A)}}$ ,

P\big(\{f(A,\cdot)\ge k\}\big)\ \le\ \exp\Big(-\frac2N\Big(k-\sqrt{\tfrac N2\log\tfrac1{P(A)}}\Big)^2\Big). \tag{2.2.7}

Milestones, in attack order

Lemma 2.1.2 — for measurable $0\le g\le1$ on $\Omega$ : $\int\min(e^t,1/g)\,d\mu\int g\,d\mu\le a(t)$ .
Proposition 2.1.1 — $\int e^{tf(A,x)}dP\le a(t)^N/P(A)\le e^{t^2N/4}/P(A)$ for $t>0$ , and $P(f(A,\cdot)\ge k)\le e^{-k^2/N}/P(A)$ .
Remark 2.1.3 — the same with the weighted Hamming distance and $\sum a_i^2$ in place of $N$ .
Eq. (2.2.3) — $a(\alpha,t)=\sup_{0\le u\le1}(1+u(e^t-1))(1-u(1-e^{-t/\alpha}))^{\alpha}$ .
Proposition 2.2.1 — $\int e^{tf(A,x)}dP\le a(\alpha,t)^N/P(A)^{\alpha}$ for $t\ge0$ .
Lemma 2.2.2 — $a(\alpha,t)\le\exp\frac{t^2}8(1+\frac1\alpha)$ .

The goal is the weakest statement of the section that is stated with fully explicit, closed-form constants; the milestones are the steps the paper's proof passes through.

Significance

The result. Inequality (2.2.7) shows that if $P(A)$ is bounded below, the set of points at Hamming distance at least $\sqrt{N/2\cdot\log(1/P(A))}+s$ from $A$ has probability at most $e^{-2s^2/N}$ , with no assumption on $\Omega$ or $\mu$ . Applied to $A=\{F\le M\}$ for a function $F$ that changes by at most one when a coordinate changes, it gives concentration of $F$ around its median at scale $\sqrt N$ . The exponential moment bound (2.2.6) is the form that composes with other estimates, and the free parameter $\alpha$ is what makes the constant $2/N$ in (2.2.7) attainable rather than $1/N$ as in (2.1.3).

Formalizing it. The results are classical and fully proved in the paper; they are not available in Mathlib, and no machine-checked proof of them is known. A formalization supplies the one-coordinate inequalities (Lemma 2.1.2 and its $\alpha$ -version) and the induction over $\Omega^{N+1}=\Omega^N\times\Omega$ as reusable components: every later chapter of the memoir (two-point space, penalties, $q$ points, convex hull distance) follows the same induction with a different one-coordinate lemma.

Difficulty

The bound does not follow from a union bound or from independence of coordinates, because $f(A,\cdot)$ depends on all coordinates jointly through an arbitrary set $A$ : changing one coordinate of $x$ changes $f(A,x)$ by at most one, but which point of $A$ is nearest can change completely. A naive coordinate-by-coordinate estimate loses either the dependence on $P(A)$ or a constant factor in the exponent, and the constant $2/N$ in (2.2.7) is the sharp one, so no slack is available. The one-dimensional inequalities (Lemma 2.1.2 and its $\alpha$ -version) are extremal problems over all measurable functions $0\le g\le1$ rather than over numbers, and Lemma 2.2.2 is a two-parameter inequality in which the closed form (2.2.2) is not convenient. On the measure-theoretic side, all integrands take values in $[0,\infty]$ and $f(A,\cdot)$ need not be measurable in general.

Formalization scope

Space. $(\Omega,\Sigma,\mu)$ is an arbitrary measurable space with a probability measure; $\Omega^N$ is Fin N → Ω (0-based coordinates) and $P$ is Measure.pi (fun _ => μ). $\Omega$ is never restricted to a finite or countable set.
Measurability. The paper ignores measurability and states Proposition 2.1.1 with an upper integral and outer probability. Here $A$ carries MeasurableSet A and the map $x\mapsto f(A,x)$ carries an explicit Measurable hypothesis; probabilities of arbitrary sets are Mathlib's outer measure.
Values. Distances are in $[0,\infty]$ (ℝ≥0∞), so $f(\emptyset,x)=+\infty$ ; integrals are lower Lebesgue integrals ∫⁻ in $[0,\infty]$ ; $e^{tz}$ is EReal.exp; $P(A)^{-1}$ and $P(A)^{-\alpha}$ are computed in $[0,\infty]$ , so $P(A)=0$ makes the right-hand sides $+\infty$ .
Constants. $a(\alpha,t)$ is formula (2.2.2) for $t\ne0$ and $1$ at $t=0$ . Every constant ( $1/4$ , $1/8$ , $2/N$ ) is the paper's.
Ruled out. Defining $f$ through a real infimum (whose junk value on $\emptyset$ is $0$ ), or letting $a(\alpha,0)=0/0=0$ , would make several statements false or trivial; neither is done.

Needed infrastructure: Fubini/Tonelli for Measure.pi split as $\Omega^N\times\Omega$ , Chebyshev–Markov for ∫⁻, and one-variable calculus for (2.2.3)–(2.2.5). The one-coordinate lemmas and the induction scheme are reusable in the later missions of this series. Proofs of individual milestones and alternative proofs (for example via martingales for (2.2.7)) are welcome.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. https://doi.org/10.1007/bf02699376
C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, LMS Lecture Note Ser. 141 (1989), 148–188. https://doi.org/10.1017/CBO9781107359949.008
L. H. Harper, Optimal numberings and isoperimetric problems on graphs, J. Combin. Theory 1 (1966), 385–393. https://doi.org/10.1016/S0021-9800(66)80059-5

8 thms2 active usersReviewed

Completed

Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces III: Penalties — Exponential Moments of the Penalized Distance f_h(A, x)Textbook

Motivation

Concentration of measure in a product space $\Omega^N$ asks how much of the space lies close to a set $A$ of non-negligible probability. In the simplest setting closeness is the Hamming distance: the number of coordinates of $x$ that cannot be matched by a point of $A$ . Talagrand's 1995 memoir in Publications Mathématiques de l'IHÉS develops a family of such inequalities with one method, induction over the number of coordinates, and applies them to combinatorial optimization, random graphs, spin glasses and sums of Banach-space-valued random vectors.

Counting a missed coordinate as $1$ ignores how far apart the two coordinate values are. Sections 2.4 and 2.5 of the memoir replace the unit cost by a penalty $h(x_i, y_i)$ that depends on the values being matched. The resulting bounds have the shape of Bernstein's inequality: a Gaussian tail for moderate deviations, governed by the $L^2$ size of the penalty, and an exponential tail for large ones, governed by its sup norm. Theorem 2.4.1 is used again in Chapter 11 of the memoir, Corollary 2.4.4 in the study of the Sherrington–Kirkpatrick model in Chapter 12, and Theorem 2.5.1 in Section 11.5.

Setting

Let $(\Omega, \mu)$ be a probability space, $N \ge 0$ an integer, and $P = \mu^{\otimes N}$ the product probability on $\Omega^N$ . A penalty is a measurable function $h : \Omega \times \Omega \to [0, \infty)$ with $h(\omega, \omega) = 0$ for every $\omega$ (the paper's standing assumption (2.4.2)). For $A \subseteq \Omega^N$ and $x \in \Omega^N$ the penalized distance is

f_h(A, x) = \inf\Big\{ \sum_{i \le N} h(x_i, y_i)\,\mathbf 1_{\{x_i \ne y_i\}} \;;\; y \in A \Big\},

with $f_h(\emptyset, x) = +\infty$ . For $h = 1$ off the diagonal this is the Hamming distance. Theorem 2.4.1 also uses the symmetrized penalty $v(\omega, \omega') = \max(h(\omega, \omega'), h(\omega', \omega))$ .

Section 2.5 measures the penalty against sets: for $B \subseteq \Omega$ ,

h(\omega, B) = \inf\{ h(\omega, \omega') \;;\; \omega' \in B \},

the infimum being over the second variable, as in $f_h$ . The one-coordinate steps of the two inductions use the transforms $\hat g(x) = \inf_{y}(g(y) + t\,h(x,y))$ (2.4.5) and $\hat g(x) = \inf_{s>0} s + t\,h(x, B_s)$ with $B_s = \{g \le s\}$ (2.5.7), for a function $g \ge 0$ on $\Omega$ .

Formalization targets

Goal: Theorem 2.4.1

For each measurable $A \subseteq \Omega^N$ and each $t > 0$ with $\iint \exp t h(x,y)\, d\mu(x)\, d\mu(y) < \infty$ ,

\int_{\Omega^N} e^{t f_h(A,x)}\, dP(x) \le \frac{1}{P(A)} \Big( \frac12 \int_{\Omega^2} \big(e^{t v(\omega,\omega')} + e^{-t v(\omega,\omega')}\big)\, d\mu(\omega)\, d\mu(\omega') \Big)^N.

It is the most general exponential-moment bound of the section; every tail bound of Section 2.4 is derived from it.

Milestones

Proposition 2.4.2, the one-coordinate inequality $\int e^{\hat g}\, d\mu \int e^{-g}\, d\mu \le \frac12 \iint (e^{tv} + e^{-tv})\, d\mu\, d\mu$ for $g \ge 0$ .
Theorem 2.4.3: if $\iint e^{h} < \infty$ , then for $0 \le t \le 1$

\int e^{t f_h(A,x)}\, dP(x) \le \frac{1}{P(A)} \exp\Big( N t^2 \iint (e^{h} + e^{-h} - 2)\, d\mu\, d\mu \Big).

Corollary 2.4.4: if $\iint e^{h} \le 2$ , then $P(f_h(A,\cdot) \ge u) \le P(A)^{-1} e^{-u^2/4N}$ for $0 \le u \le 2N$ .
Corollary 2.4.5: if $\|h\|_\infty = \sup h < \infty$ , then

P(f_h(A,\cdot) \ge u) \le \frac{1}{P(A)} \exp\Big( -\min\Big( \frac{u^2}{8N\|h\|_2^2},\ \frac{u}{2\|h\|_\infty} \Big) \Big).

Proposition 2.5.2, the one-coordinate inequality $\int e^{\hat g}\, d\mu \int e^{-g}\, d\mu \le e^{3t^2}$ for the transform (2.5.7), under condition (2.5.2) below.
Theorem 2.5.1: if $\int_\Omega \exp 2h(x, B)\, d\mu(x) \le e/\mu(B)$ for each $B \subseteq \Omega$ (condition (2.5.2)), then for $0 \le t \le 1$

\int e^{t f_h(A,x)}\, dP(x) \le \frac{e^{3t^2 N}}{P(A)}.

Significance

The results. Theorem 2.4.1 turns a single integrability condition on the penalty into a bound on the exponential moment of the distance to any set, uniform over all sets of a given probability and factorized over coordinates. Chebyshev's inequality then gives the Bernstein-type tails of Corollaries 2.4.4 and 2.4.5, which hold for every set $A$ , not only for half-spaces or for sums of independent variables. Theorem 2.5.1 replaces exponential integrability of $h$ by condition (2.5.2) on the set functional $h(x, B)$ , which is much weaker: when $\Omega$ is itself a product of $m$ spaces, $m^{-1/2}$ times the Hamming distance on $\Omega$ satisfies (2.5.2) but not (2.4.12). Applied to blocks of coordinates, it shows that the coordinates a typical point misses in $A$ are concentrated in few blocks.

Formalizing them. All six results are proved in the memoir with short arguments. None of them has a machine-checked proof. A complete development would give a general-alphabet version of Talagrand's induction on product measures, written once for a cost function, that later chapters (the $q$ -point control, the convex-hull distance) also rely on.

Difficulty

The induction over $N$ requires a one-coordinate inequality whose right-hand side does not depend on the set. The difficulty is that the natural one-coordinate quantity, a section measure $P(A(\omega))$ , can vanish on part of $\Omega$ , so the function $g = -\log P(A(\omega))$ takes the value $+\infty$ , and a statement proved for finite $g$ must be extended by truncation. The other subtle point is measure theoretic: $f_h(A, \cdot)$ need not be measurable even when $A$ is, and the paper's convention of ignoring measurability has to be matched by explicit hypotheses. In Section 2.5 the integrand $x \mapsto h(x, B)$ in condition (2.5.2) may be non-measurable for the sets the proof uses, and Fubini's theorem is applied to the function $(x, y) \mapsto h(x, B_{g(y)})$ .

Formalization scope

Points of $\Omega^N$ are functions Fin N → Ω (coordinates indexed from $0$ ), $P$ is Measure.pi (fun _ => μ) for a probability measure μ, and double integrals are over μ.prod μ. The penalty is a real function h : Ω → Ω → ℝ with explicit hypotheses $h \ge 0$ , $h(\omega,\omega) = 0$ and joint measurability, in every statement. The distance $f_h$ is defined by (2.4.1) with the indicator and takes values in $[0,\infty]$ , so $f_h(\emptyset, x) = +\infty$ ; likewise $h(\omega, B)$ and the transform (2.5.7). All integrals are Lebesgue integrals of $[0,\infty]$ -valued functions, $e^{+\infty} = +\infty$ , and $1/P(A) = +\infty$ when $P(A) = 0$ .

Measurability follows the paper's convention (pp. 81–82) as explicit hypotheses: $A$ is measurable and $x \mapsto f_h(A, x)$ is measurable; in the propositions, $g$ and $\hat g$ are measurable. Condition (2.5.2) is stated for every subset $B$ with the upper integral $\int^*$ , which the paper prescribes when measurability fails. In Corollary 2.4.5, the quotients are computed in $[0,\infty]$ , so a quotient by $\|h\|_2 = 0$ , $\|h\|_\infty = 0$ or $N = 0$ is $+\infty$ when its numerator is positive. The bound is $+\infty$ when $P(A)=0$ , as the printed factor $1/P(A)$ intends. No statement is restricted to a finite or countable $\Omega$ : restricting it would turn the general theorems into their finite-alphabet special cases. Dropping $h(x,x) = 0$ or defining the distance by a real infimum (whose value on the empty set is $0$ ) would change the theorems and is ruled out.

A complete development needs product measures on Fin (N+1) → Ω split as $\Omega^N \times \Omega$ , sections of measurable sets, Tonelli's theorem, and the elementary convexity inequalities used in the proofs; the induction scaffold is reusable for the other distance functionals of the memoir. Proofs of any milestone are welcome, as are proofs of the extension of Proposition 2.4.2 to $g$ with values in $[0,\infty]$ , which the paper states without number on p. 92.

Selected references

M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publications Mathématiques de l'IHÉS 81 (1995), 73–205. https://doi.org/10.1007/BF02699376
M. Talagrand, A new look at independence, Annals of Probability 24 (1996), 1–34. https://doi.org/10.1214/aop/1042644705
M. Ledoux, The Concentration of Measure Phenomenon, Mathematical Surveys and Monographs 89, AMS, 2001. https://doi.org/10.1090/surv/089

8 thms2 active usersReviewed

Completed

Functional Analysis Operations Research Optimization·Captain: mikedeng1

An Implicit-Function Theorem for a Class of Nonsmooth Functions: Strong Approximation by a Function with Lipschitzian Inverse Yields a Unique Lipschitzian Implicit FunctionResearch Paper

Why a nonsmooth implicit-function theorem

The classical implicit-function theorem solves an equation $F(x, y) = 0$ for $x$ as a function of a parameter $y$ near a known solution $(x_0, y_0)$ , provided $F$ is (strongly) Fréchet differentiable in $x$ with an invertible partial derivative. Much of optimization does not meet that hypothesis. Optimality conditions of constrained problems, complementarity problems and variational inequalities are routinely rewritten as equations involving the projection onto a convex set, the componentwise $\min$ , or the normal map of a polyhedron. These maps are Lipschitzian and piecewise smooth, but not differentiable. Sensitivity analysis asks whether the solution of such a system moves Lipschitz-continuously with the problem data, and the classical theorem cannot answer it.

Stephen M. Robinson, An Implicit-Function Theorem for a Class of Nonsmooth Functions, Mathematics of Operations Research 16(2), 1991, pp. 292–309, gives a theorem with the same shape as the classical one, in which differentiability is replaced by strong approximation by a function whose inverse is Lipschitzian. The paper's §4 applies it to parametric variational inequalities over polyhedral sets through the normal map.

Timeline. Robinson's Strongly regular generalized equations (Math. Oper. Res. 5, 1980) proved an implicit-function theorem for generalized equations under a linearization hypothesis called strong regularity. The 1991 paper reformulates that idea for single-valued nonsmooth equations: the approximating function $f$ need not be linear. Lemma 3.1 extends the Banach perturbation lemma for linear operators (Kantorovich–Akilov, Functional Analysis, Th. 4(2.V)) to Lipschitzian functions; after acceptance, A. Ioffe pointed the author to closely related results of Dmitruk, Milyutin and Osmolovskii (Lyusternik's theorem and the theory of extrema, Russian Math. Surveys, 1980, Theorems 1.2, 1.3), credited in the paper's footnote.

Setting

Let $X$ , $Y$ , $Z$ be real normed linear spaces, with $X$ complete. Fix $x_0 \in X$ , $y_0 \in Y$ , a neighborhood $\Xi$ of $x_0$ and a neighborhood $H$ of $y_0$ . Let $F$ map $\Xi \times H$ to $Z$ , with $F(x_0, y_0) = 0$ , and let $f$ map $\Xi$ to $Z$ , with $f(x_0) = 0$ . $B(x, \rho)$ denotes the closed ball of radius $\rho$ about $x$ .

Expansion modulus. For a map $f$ between metric spaces and a set $S$ ,

\delta(f, S) = \inf\left\{ \frac{\|f(x_1) - f(x_2)\|}{\|x_1 - x_2\|} : x_1 \ne x_2,\ x_1, x_2 \in S \right\}.

If $\delta(f,S) > 0$ , then $f$ is one-to-one on $S$ and its inverse is Lipschitzian with modulus $\delta(f,S)^{-1}$ . In Lean the mission works with lower bounds: ExpansionAtLeast f S d says $d\,\|x_1 - x_2\| \le \|f(x_1) - f(x_2)\|$ on $S$ , i.e. $d \le \delta(f,S)$ .

Strong approximation (Definition 2.4). $f$ strongly approximates $F$ in $x$ at $(x_0, y_0)$ , written $f \approx_x F$ (Lean: StronglyApproxInX f F x₀ y₀), if for each $\varepsilon > 0$ there are neighborhoods $U$ of $x_0$ and $V$ of $y_0$ with

\big\|[F(x, y) - f(x)] - [F(x', y) - f(x')]\big\| \le \varepsilon \|x - x'\| \qquad (x, x' \in U,\ y \in V).

When $f$ is the partial derivative map $x \mapsto F_x(x_0,y_0)(x - x_0)$ this is strong partial Fréchet differentiability; in general $f$ may be piecewise linear or any map with a Lipschitzian inverse.

Formalization targets

Goal: Theorem 3.2 (p. 299)

Assume (a) $f \approx_x F$ at $(x_0, y_0)$ ; (b) for each $x \in \Xi$ , $F(x, \cdot)$ is Lipschitzian on $H$ with modulus $\varphi$ ; (c) $f(\Xi)$ is a neighborhood of $0$ in $Z$ ; (d) $\delta(f, \Xi) =: d_0 > 0$ . Then for each $\lambda > d_0^{-1}\varphi$ there are neighborhoods $U \subseteq \Xi$ of $x_0$ , $V \subseteq H$ of $y_0$ and a function $x : V \to U$ with

x(y_0) = x_0, \qquad \|x(y_1) - x(y_2)\| \le \lambda \|y_1 - y_2\| \ (y_1, y_2 \in V), \qquad \{\xi \in U : F(\xi, y) = 0\} = \{x(y)\} \ (y \in V).

Every $\lambda$ strictly above $\varphi/d_0$ is claimed; $\lambda = \varphi/d_0$ is not.

Milestones

Lemma 3.1 (p. 298), the Lipschitz perturbation lemma: if $f$ maps $\Omega$ onto a ball $B(y_0, \alpha)$ , $h$ is Lipschitzian with modulus $\eta < \delta := \delta(f, \Omega)$ , $\Omega \supseteq B(x_0, \delta^{-1}\alpha)$ and $\theta := (1 - \eta\delta^{-1})\alpha - \|h(x_0)\| \ge 0$ , then

(f + h)\big(B(x_0, \delta^{-1}\alpha)\big) \supseteq B(y_0, \theta), \qquad \delta(f + h, \Omega) \ge \delta - \eta > 0.

(3.1)–(3.2) in the proof of Theorem 3.2 (p. 300): for every $\varepsilon \in (0, d_0)$ there are $\alpha, \kappa > 0$ and a neighborhood $V \subseteq H$ of $y_0$ with $\Omega = B(x_0, d_0^{-1}\alpha) \subseteq \Xi$ such that for each $y \in V$

\delta(F(\cdot, y), \Omega) \ge d_0 - \varepsilon, \qquad F(\cdot, y)(\Omega) \supseteq B(0, \theta(y)) \supseteq B(0, \kappa),

where $\theta(y) = (1 - \varepsilon d_0^{-1})\alpha - \|F(x_0, y)\|$ .

Significance

The result. Theorem 3.2 yields existence, local uniqueness and Lipschitz dependence of solutions of parametrized nonsmooth equations, with an explicit Lipschitz modulus arbitrarily close to $\varphi/d_0$ . In the paper it underlies Theorem 3.3 and Corollary 3.4 (approximation and B-differentiation of the implicit function) and the sensitivity results of §4 for parametric variational inequalities over polyhedral convex sets. The same template, an equation approximated by a map with Lipschitzian inverse, is the basis of later strong-regularity and semismooth-Newton analyses in nonlinear programming and complementarity.

Formalizing it. The theorem is proved in the paper; it has not been machine-checked. The platform has the smooth implicit-function theorem (FamousTheorems.implicit_function_theorem, Rudin.ch09_implicit_function) and Mathlib has the contraction mapping principle, but there is no Lipschitz-inverse perturbation result and no notion of strong approximation. The mission produces both, together with the formal Theorem 3.2 that a follow-on mission (Theorem 3.3, Corollary 3.4, §4) would reference.

Difficulty

The obvious approach, differentiate and invert, is unavailable: $f$ need not have a derivative anywhere near $x_0$ , so neither Mathlib's implicit-function theorem nor its inverse-function theorem applies. The difficulty is to obtain surjectivity of $F(\cdot, y)$ onto a ball uniformly in $y$ from information about $f$ alone. Injectivity transfers directly from $f$ through the small Lipschitz modulus of $F(\cdot, y) - f$ ; surjectivity does not, because $f$ carries no information about $F(\cdot, y)$ beyond the small Lipschitz modulus of the difference, and the domain ball, the image ball and the parameter neighborhood must be chosen once for all $y$ . Completeness of $X$ is essential (the paper stresses this on p. 306) and is not available for $Y$ and $Z$ .

Formalization scope

All statements live in namespace RobinsonNSIFT.Implicit. Committed conventions:

Scalars are real; $X$ is a complete normed space ([CompleteSpace X]); $Y$ , $Z$ are normed spaces without completeness. Lemma 3.1's domain is a complete metric space, not a normed one.
$\delta(f, S)$ via lower bounds. Every statement takes a real $d$ with ExpansionAtLeast f S d in place of " $d = \delta(f,S)$ ", universally quantified. This is equivalent to the paper's statements and avoids a real infimum that would be $0$ on sets with fewer than two points.
Total functions. $F$ is a curried total function F : X → Y → Z and $f : X \to Z$ ; hypotheses constrain them on $\Xi \times H$ only, and the conclusions keep the implicit function inside the domain: $U \subseteq \Xi$ , $V \subseteq H$ , $x(V) \subseteq U$ . This makes explicit what the paper leaves implicit (its $F$ is only defined on $\Xi \times H$ ). Likewise $\Omega \subseteq \Xi$ , used implicitly in the paper's proof, is a conclusion of milestone 2.
Closed balls (Metric.closedBall), radii $\delta^{-1}\alpha$ written α / δ; neighborhoods are filter members ∈ 𝓝 _, not necessarily open; Lipschitz moduli are ℝ≥0 and Lipschitz conditions are LipschitzOnWith on the stated set.
Lemma 3.1 keeps the paper's hypothesis that $\Omega$ is open, although Theorem 3.2's proof applies it to a closed ball.
Milestone 2 states as an existence claim, for every $\varepsilon \in (0, d_0)$ , the choices the paper makes at the start of its proof.

A formalization in which hypothesis (a) is the weak approximation of Definition 2.1 (only at $y = y_0$ ), in which $V$ may shrink to $\{y_0\}$ , $\lambda$ is existential, or uniqueness is asserted outside $\Xi$ , would be a different and trivial or false statement; the statements here rule these out.

Needed infrastructure: the contraction mapping principle on a closed subset of a complete space (Mathlib's ContractingWith), Lipschitz estimates on sets, and the two definitions of this mission. Lemma 3.1 is reusable for any Lipschitz-perturbation argument. Proofs of either milestone, or a direct proof of the goal, are welcome.

Selected references

S. M. Robinson, An Implicit-Function Theorem for a Class of Nonsmooth Functions, Mathematics of Operations Research 16(2), 1991, 292–309. https://doi.org/10.1287/moor.16.2.292
S. M. Robinson, Strongly Regular Generalized Equations, Mathematics of Operations Research 5(1), 1980, 43–62. https://doi.org/10.1287/moor.5.1.43
A. V. Dmitruk, A. A. Milyutin, N. P. Osmolovskii, Lyusternik's theorem and the theory of extrema, Russian Mathematical Surveys 1980, No. 6, 11–51 (as cited in Robinson 1991, p. 298).
L. V. Kantorovich, G. P. Akilov, Functional Analysis, cited in Robinson 1991 as [17].

4 thms2 active usersReviewed

Harmonic Analysis Probability·Captain: mikedeng1

Distribution Function Inequalities for Martingales 1: The Square Function and the Martingale Have Equivalent L^p Norms for 1 < p < ∞Research Paper

Why the square function of a martingale matters

A martingale $f = (f_1, f_2, \dots)$ is a sum $f_n = d_1 + \cdots + d_n$ of increments that are uncorrelated with the past. For sums of independent random variables, sizes are compared through the sum of squares of the summands; for martingales the corresponding object is the square function

S(f) = \Bigl(\sum_{k=1}^\infty d_k^2\Bigr)^{1/2}.

Comparing the size of $f$ with the size of $S(f)$ is one of the basic tools of probability and of harmonic analysis: it underlies Khintchine-type inequalities, the $L^p$ theory of martingale transforms, the Littlewood–Paley theory of dyadic and Fourier series, and the Burkholder–Davis–Gundy inequalities used throughout stochastic calculus.

Timeline. Paley (1932) proved $L^p$ bounds for the square function of Walsh–Paley series, the dyadic model case. Marcinkiewicz and Zygmund (1937–38) proved the analogous inequalities for sums of independent mean-zero random variables. Burkholder (1966, Ann. Math. Statist. 37) proved them for general martingales, $1 < p < \infty$ , together with the weak-type $(1,1)$ bound for $S(f)$ . Burkholder and Gundy (1970) extended the comparison to functions $\Phi$ of moderate growth by distribution function ("good- $\lambda$ ") inequalities, and Davis (1970) settled $p = 1$ for $f^* = \sup_n |f_n|$ . The 1973 Wald lectures formalized here re-derive the $1 < p < \infty$ inequality from one elementary stopping-time identity (Lemma 2.1), with explicit constants.

Setting

Let $(\Omega, \mathcal A, P)$ be a probability space and $\mathcal A_0 \subseteq \mathcal A_1 \subseteq \cdots$ sub- $\sigma$ -fields of $\mathcal A$ . A martingale relative to $\mathcal A_1, \mathcal A_2, \dots$ is a sequence of integrable random variables $f_n$ , with $f_n$ $\mathcal A_n$ -measurable and $E(f_{n+1} \mid \mathcal A_n) = f_n$ ; a submartingale has $\ge$ in place of $=$ .

With the convention $f_0 = 0$ , the difference sequence is $d_k = f_k - f_{k-1}$ (so $d_1 = f_1$ ). Write

$S_n(f) = (\sum_{k=1}^n d_k^2)^{1/2}$ and $S(f) = \sup_n S_n(f) \in [0, \infty]$ ;
$f_n^* = \max_{1\le k\le n} |f_k|$ and $f^* = \sup_n |f_n|$ ;
$\|Y\|_p = (E|Y|^p)^{1/p}$ for a random variable $Y$ , and $\|f\|_p = \sup_{n\ge1} \|f_n\|_p$ for the process. The process is $L^p$ -bounded when $\|f\|_p < \infty$ .

For $\lambda > 0$ the exit time $\mu = \inf\{n \ge 1 : |f_n| > \lambda\}$ (with $\inf\emptyset = \infty$ ) is a stopping time; $f_\mu$ , $f_{\mu-1}$ , $S_{\mu-1}(f)$ denote evaluation at the random index, with $f_\infty = \lim_n f_n$ and $S_\infty(f) = S(f)$ .

In Lean these are dseq, sqFnN, sqFn, maxFnN, lpNormE, pNorm, exitTime, valAt and sqFnAt in the namespace BurkholderDFI.SquareFnLp.

Formalization targets

Goal: Theorem 3.2

For each $1 < p < \infty$ there are positive constants $c_p, C_p$ , depending only on $p$ , such that every martingale satisfies

c_p \|S(f)\|_p \le \|f\|_p \le C_p \|S(f)\|_p .

The goal asserts only existence of the constants, so that it does not depend on the particular numbers the paper's proof produces.

Milestones

In attack order:

Doob's maximal inequality (1.1): $\lambda P(f_n^* > \lambda) \le \int_{\{f_n^*>\lambda\}} |f_n| \le \|f\|_1$ .
Doob's facts (§1): an $L^1$ -bounded martingale or nonnegative submartingale converges a.e., and $\|f_\mu\|_1 \le \|f\|_1$ for every stopping time $\mu$ .
The classical extrapolation (1.2)–(1.3): $\lambda P(Y > \beta\lambda) \le \alpha\int_{\{Y>\lambda\}} X$ for all $\lambda > 0$ implies $\|Y\|_p \le \alpha\beta^p q \|X\|_p$ .
Lemma 2.1: $\|S_{\mu-1}(f)\|_2^2 + \|f_{\mu-1}\|_2^2 \le 2E f_\mu f_{\mu-1} \le 2\lambda\|f\|_1$ , with equality on the left for martingales.
Theorem 3.1: $\lambda P(S(f) > \lambda) \le 3\|f\|_1$ .
Lemma 3.1, (3.4) and (3.5): for nonnegative submartingales, $\|S_n(f)\|_p \le 9p^{1/2}q\|f_n\|_p$ .
(3.7): for martingales, $\|S_n(f)\|_p \le 18 p^{1/2} q \|f_n\|_p$ .
The duality bound: $\|f_n\|_p \le 18 q^{1/2} p \|S_n(f)\|_p$ .

Here $q$ is the conjugate exponent, $p^{-1} + q^{-1} = 1$ .

Significance

The result. Theorem 3.2 says that a martingale is bounded in $L^p$ exactly when its square function lies in $L^p$ , with comparable norms. It reduces questions about $f$ , whose increments interact, to questions about $\sum d_k^2$ , a sum of nonnegative terms. Immediate consequences include the $L^p$ boundedness of martingale transforms $\sum v_k d_k$ with $|v_k| \le 1$ (unconditionality of martingale differences in $L^p$ ), Marcinkiewicz–Zygmund and Khintchine inequalities, and, by passing through dyadic martingales, Littlewood–Paley inequalities. Theorem 3.1 is the endpoint estimate: at $p = 1$ the strong inequality fails, and weak type $(1,1)$ is what survives.

The formalization. The theorem is classical and proved; the remaining work is to machine-check it. Mathlib at the pinned revision contains no square function inequality for martingales (no occurrence of Burkholder's inequality or of a martingale square function in Mathlib/Probability); it has Doob's maximal inequality for nonnegative submartingales, optional stopping, and a.e. convergence of $L^1$ -bounded submartingales. The mission would add the stopping-time identity of Lemma 2.1, the weak-type bound with constant 3, the explicit $L^p$ constants $18 p^{1/2} q$ and $18 q^{1/2} p$ , and the general extrapolation lemma (1.3), each reusable on its own.

Difficulty

The obvious route, expanding $E S_n(f)^2 = E f_n^2$ by orthogonality, works only at $p = 2$ . For $p \ne 2$ no such identity exists, and interpolation from $p = 2$ needs an endpoint estimate that is itself the hard part: $S(f)$ is not bounded on $L^1$ . The paper obtains the endpoint from Lemma 2.1, whose content is an exact computation at the random time $\mu$ ; turning it into rigorous Lean requires handling evaluation at $\mu = \infty$ (where the a.e. limit $f_\infty$ enters), passage to the limit $n \to \infty$ in stopped identities with only $L^1$ control, and integrability of the products $f_\mu f_{\mu-1}$ . The upper bound is not a formal consequence of the lower one at the same exponent: it requires passing to the conjugate exponent $q$ .

Formalization scope

Processes are f : ℕ → Ω → ℝ; martingales and submartingales are Mathlib's Martingale f ℱ P / Submartingale f ℱ P for a filtration ℱ : Filtration ℕ _ with ℱ k $= \mathcal A_k$ . The paper's $f_0 = 0$ is built into every definition, which never reads Lean's f 0. Mathlib additionally relates f 0 to $f_1$ ; this is no restriction, since any martingale relative to $\mathcal A_1, \mathcal A_2, \dots$ extends by $f_0 := E(f_1 \mid \mathcal A_0)$ .
"Nonnegative submartingale" means $f_n \ge 0$ almost everywhere for $n \ge 1$ .
$S(f)$ , $f^*$ , $\|\cdot\|_p$ and $\|f\|_p$ take values in $[0, \infty]$ . Neither $\|f\|_p$ nor $\|S(f)\|_p$ is assumed finite in Theorem 3.2, which therefore also asserts that one is infinite exactly when the other is. In Theorem 3.1, $\|f\|_1 = \infty$ makes the bound trivial, matching the paper's "we may assume that $f$ is $L^1$ -bounded".
The constants of Theorem 3.2 are quantified before the probability space, the filtration and the martingale. A formalization in which $c_p, C_p$ may depend on $f$ (for instance $C_p = \|f\|_p / \|S(f)\|_p$ ) would be trivially true and is excluded by this quantifier order; so is assuming finiteness of either side.
The a.e. limit $f_\infty$ is a parameter of Lemma 2.1 together with the hypothesis that $f_n \to f_\infty$ a.e.; Doob's §1 facts assert that such a limit exists.
Probability spaces live in Type (universe 0).
The asymptotic remark after Theorem 3.2 ( $c_p^{-1} = O(p^{1/2}q)$ , $C_p = O(q^{1/2}p)$ ) is not formalized; the explicit constants it summarizes are milestones 7 and 8.

Infrastructure that a complete development needs and that is reusable beyond this mission: evaluation of a process at an $\mathbb N \cup \{\infty\}$ -valued stopping time, the layer-cake formula $\|Y\|_p^p = \int_0^\infty p\lambda^{p-1} P(Y > \lambda)\, d\lambda$ for $[0,\infty]$ -valued $Y$ , and conditional-expectation martingales $E(g \mid \mathcal A_k)$ with their difference sequences. Proofs of any milestone, in any order, are welcome.

Selected references

D. L. Burkholder, Distribution function inequalities for martingales, Ann. Probability 1 (1973), 19–42. https://doi.org/10.1214/aop/1176997023
D. L. Burkholder, Martingale transforms, Ann. Math. Statist. 37 (1966), 1494–1504. https://doi.org/10.1214/aoms/1177699141
D. L. Burkholder and R. F. Gundy, Extrapolation and interpolation of quasi-linear operators on martingales, Acta Math. 124 (1970), 249–304. https://doi.org/10.1007/BF02394573
B. Davis, On the integrability of the martingale square function, Israel J. Math. 8 (1970), 187–190. https://doi.org/10.1007/BF02771313
J. L. Doob, Stochastic Processes, Wiley, New York, 1953.
R. E. A. C. Paley, A remarkable series of orthogonal functions (I), Proc. London Math. Soc. (2) 34 (1932), 241–264. https://doi.org/10.1112/plms/s2-34.1.241

11 thms2 active usersReviewed

Operations Research·Captain: mikedeng1

Regret in Decision Making under Uncertainty 1: Under Assumptions 2 and 3, Utility over Final and Foregone Assets Takes the Regret Form u(x, y) = αv(x) + f(v(x) − v(y))Research Paper

Why regret enters the utility function

Expected utility theory predicts that a decision maker's choice between two lotteries depends only on the distribution of final wealth under each. Observed behaviour contradicts this in systematic ways: the Allais paradox, the coexistence of insurance and gambling, and the reflection effect documented by Kahneman and Tversky (1979). David Bell's 1982 paper (Operations Research 30(5), 961–981) explains these patterns by regret: the dissatisfaction of learning that the alternative not chosen would have done better. In the same year Loomes and Sugden (1982) proposed a closely related theory; together the two papers are the origin of regret theory in decision analysis.

Bell's contribution is axiomatic. Instead of postulating a regret term, he derives the shape of a utility function that incorporates regret from three behavioural assumptions about how preferences respond to shifting all outcomes by an equal increment of value. This mission formalizes that derivation, Section 1 of the paper (pp. 965–970), culminating in Theorem 1.

Setting

An endpoint is described by two attributes: the final assets $x$ and the foregone assets $y$ , the asset level the decision maker would have had under the alternative not chosen. Utility is a function $u(x,y)$ , strictly increasing in $x$ and strictly decreasing in $y$ .

A simple comparison is a choice between two alternatives whose uncertainties are resolved by one predetermined joint distribution. With $n$ states, a probability vector $p=(p_1,\dots,p_n)$ and alternatives $A,B\in\mathbb R^n$ ( $A_i$ the final assets of $A$ in state $i$ ), the expected utility of selecting $A$ while $B$ is foregone is

\mathrm{EU}_p(A\,|\,B)=\sum_{i=1}^n p_i\,u(A_i,B_i),

and $A$ is preferred to $B$ when $\mathrm{EU}_p(B\,|\,A)<\mathrm{EU}_p(A\,|\,B)$ (inequality (1) of the paper).

A value function $v:\mathbb R\to\mathbb R$ , strictly increasing and onto $\mathbb R$ , measures incremental value: moving from $a$ to $b$ is worth $v(b)-v(a)$ . An alternative $A'$ is obtained from $A$ by a shift of incremental value $\delta$ if $v(A'_i)=v(A_i)+\delta$ for every state.

Assumption 1. Shifting every outcome of both alternatives by the same incremental value leaves the preferred alternative unchanged.
Assumption 2. If $v(x_2)-v(x_1)=v(x_3)-v(x_2)$ , the decision maker is indifferent between $x_2$ for sure and a 50-50 lottery between $x_1$ and $x_3$ .
Assumption 3. If selecting $L_1$ over $L_2$ is preferred to selecting $L_3$ over $L_4$ , that is $\mathrm{EU}_p(L_3\,|\,L_4)<\mathrm{EU}_p(L_1\,|\,L_2)$ , this persists after all outcomes of all four alternatives are shifted by the same incremental value.

Formalization targets

Goal: the regret form (Theorem 1, p. 969, corrected)

Under Assumptions 2 and 3, there are a constant $\alpha$ and a function $f$ with

u(x,y)=\alpha\,v(x)+f\big(v(x)-v(y)\big)\quad\text{for all }x,y.

Utility separates additively into a term in the value of final assets and a function of the regret $v(x)-v(y)$ . The coefficient $\alpha$ is left free (see Formalization scope).

Milestones, in the order of the paper's argument

Proof of Lemma 1 (p. 967): for $v(x)=x$ , $w(x+h,y+h)=k(h)\,w(x,y)$ with $k(h)>0$ , where $w(x,y)=u(x,y)-u(y,x)$ .
Lemma 1, linear $v$ (p. 967): $u(x,y)-u(y,x)=[u(0,y-x)-u(y-x,0)]\,e^{-cx}$ .
Lemma 1 (p. 967): Assumption 1 implies $u(x,y)-u(y,x)=g(v(x)-v(y))\,e^{-c\,v(x)}$ .
Lemma 2, linear $v$ (p. 968): $u(x,y)-u(y,x)=u(0,y-x)-u(y-x,0)$ .
Lemma 2 (p. 968): Assumptions 1 and 2 imply $u(x,y)-u(y,x)=g(v(x)-v(y))$ .
Assumption 1 is a special case of Assumption 3 (p. 969).
Proof of Theorem 1 (p. 970): for $v(x)=x$ , $u(x+h,y+h)-u(x,y)=j(h)$ .
Theorem 1 for $v(x)=x$ (p. 970): $u(x,y)=\alpha x+u(0,y-x)$ .

Significance

The additive form is the basis of the rest of Bell's paper: Section 2 uses it to show that a single decision maker with $f$ decreasingly concave both buys fair insurance and takes long-odds bets, and to account for the Allais paradox and the reflection effect. The same additive structure, a value term plus a function of the regret difference, is the form in which regret theory has been used since, alongside the parallel proposal of Loomes and Sugden (1982). Lemmas 1 and 2 have independent content: simple comparisons identify only the antisymmetric part $u(x,y)-u(y,x)$ , and the lemmas pin that part down to a function of the regret difference.

The results are published with proofs in prose; none has a machine-checked proof. Formalizing them checks the argument as printed, which turns out to need a correction (the coefficient of $v(x)$ in (4)), and fills in the regularity steps the paper leaves implicit: the solutions of the Cauchy equations that appear, and the passage from $v(x)=x$ to a general value function.

Difficulty

The obvious argument reads each assumption as a functional equation and solves it. Two steps resist this. First, the functional equations $k(x+h)=k(x)k(h)$ and $j(x+h)=j(x)+j(h)$ have non-measurable solutions; excluding them needs boundedness of $k$ and $j$ on intervals, which must be extracted from the monotonicity of $u$ and is never stated on the page. Second, the proof of Theorem 1 compares two 50-50 lotteries that are indifferent and requires $g(a_1-b_1)$ to take an arbitrary value $u(c_1,c_2)-u(a_2,b_2)$ ; when $g$ is bounded no such indifference exists, so the printed step does not cover every case. Passing from $v(x)=x$ to a general $v$ requires transporting all three assumptions along $v^{-1}$ .

Formalization scope

Assets, probabilities and utilities are real numbers; $u$ is u : ℝ → ℝ → ℝ with u x y $=u(x,y)$ . Every theorem assumes $u$ strictly increasing in $x$ and strictly decreasing in $y$ (the paper's "increasing"/"decreasing", p. 965, read strictly).
A simple comparison is a probability vector on Fin n and two alternatives on the same states. Assumption 3 quantifies over four alternatives on one common state space, the setting of the paper's own use of it.
The value function is strictly increasing (p. 968) and, as an added reading, maps $\mathbb R$ onto $\mathbb R$ : Assumptions 1 and 3 shift outcomes by arbitrary equal incremental values, which presupposes that every shifted value is attained. " $v$ linear" (Lemmas 1, 2) is read as $v(x)=ax+b$ with $a>0$ .
Indifference in Assumption 2 is "neither alternative is preferred", equivalent to the first display on p. 969.
Corrected slip. The paper's display (4) and the end of its proof have coefficient $1$ on $v(x)$ (resp. $x$ ). This is false as printed: $v(x)=x$ , $u(x,y)=x-y$ satisfies every hypothesis, but $x-y=x+f(x-y)$ forces $f(0)=0$ at $x=y=0$ and $f(0)=-1$ at $x=y=1$ . The proof derives $j(h)=\alpha h$ and silently sets $\alpha=1$ . The goal and milestone 8 keep $\alpha$ free, with no sign or normalisation imposed; milestone texts stay verbatim.
All existential objects ( $k$ , $c$ , $g$ , $j$ , $\alpha$ , $f$ ) are chosen before the variables $x,y,h$ . The assumptions are statements about preferences between lotteries, never functional equations on $u$ ; a formalization that states an assumption as " $u(x+h,y+h)-u(x,y)$ is independent of $(x,y)$ " would put the conclusion into the hypothesis and is ruled out.
Needed infrastructure: monotone or locally bounded solutions of the Cauchy additive and multiplicative equations on $\mathbb R$ , and transport of the assumptions along an order isomorphism of $\mathbb R$ . Both are reusable; contributions proving either are welcome.

Selected references

D. E. Bell, Regret in Decision Making under Uncertainty, Operations Research 30(5), 961–981, 1982. https://doi.org/10.1287/opre.30.5.961
G. Loomes and R. Sugden, Regret Theory: An Alternative Theory of Rational Choice under Uncertainty, The Economic Journal 92(368), 805–824, 1982. https://doi.org/10.2307/2232669
D. Kahneman and A. Tversky, Prospect Theory: An Analysis of Decision under Risk, Econometrica 47(2), 263–291, 1979. https://doi.org/10.2307/1914185

10 thms2 active usersReviewed

Completed

Differential Geometry Optimization·Captain: mikedeng1

Projection-like Retractions on Matrix Manifolds I: Coming Back to a Submanifold Along a Smooth Field of Transverse Subspaces Defines a RetractionResearch Paper

Motivation

Iterative methods for optimization and equation solving on a smooth constraint set $\mathcal M$ (orthogonal matrices, fixed-rank matrices, spheres, Stiefel and Grassmann manifolds) compute an update vector $u$ in the tangent space at the current iterate $x$ and then have to return to $\mathcal M$ . The Riemannian exponential map does this along geodesics, but computing it means solving an ordinary differential equation. The notion of retraction, introduced by Adler, Dedieu, Margulies, Martens and Shub (IMA J. Numer. Anal., 2002) and developed in the book of Absil, Mahony and Sepulchre (Princeton, 2008), captures what such a return map needs for Newton's method to keep its local quadratic convergence and for gradient methods to converge: smoothness, $R(x,0)=x$ , and first-order agreement with the exponential.

Absil and Malick (SIAM J. Optim., 2012; HAL hal-00651608v2) give a general recipe for building retractions on submanifolds of a Euclidean space: move tangentially from $x$ to $x+u$ , then come back to $\mathcal M$ along a prescribed family of admissible directions. This mission formalizes that recipe, Theorem 4.2 of the paper ("retractors give retractions"), together with the two lemmas its proof rests on.

Setting

Let $\mathcal E$ be a Euclidean space of dimension $n$ (in the paper's examples, $\mathbb R^{n\times m}$ with the Frobenius inner product). A set $\mathcal M\subseteq\mathcal E$ is a $C^k$ submanifold of dimension $d$ if around every $\bar x\in\mathcal M$ it is a coordinate slice: there are an open neighbourhood $\mathcal U$ of $\bar x$ and a $C^k$ diffeomorphism $\phi$ of $\mathcal U$ onto an open subset of $\mathbb R^n$ with $\mathcal M\cap\mathcal U=\{x\in\mathcal U:\phi_{d+1}(x)=\dots=\phi_n(x)=0\}$ . Throughout, $k\ge2$ .

The tangent space $\mathrm T_{\mathcal M}(x)$ is the linear subspace of $\mathcal E$ of tangent directions of $\mathcal M$ at $x$ , the normal space $\mathrm N_{\mathcal M}(x)$ is its orthogonal complement, and the tangent bundle is $\mathrm T\mathcal M=\{(x,u):x\in\mathcal M,\ u\in\mathrm T_{\mathcal M}(x)\}$ .

A map $R$ from $\mathrm T\mathcal M$ to $\mathcal M$ is a retraction around $\bar x$ (Definition 2.1) if, on a neighbourhood $\mathcal U$ of $(\bar x,0)$ in $\mathrm T\mathcal M$ , it is of class $C^{k-1}$ , satisfies $R(x,0)=x$ , and $u\mapsto R(x,u)$ has derivative $\mathrm{id}_{\mathrm T_{\mathcal M}(x)}$ at $u=0$ . It is a retraction on $\mathcal M$ if this holds around every point.

A retractor (Definition 4.1) is a $C^{k-1}$ map $D$ , defined on a neighbourhood of the zero section of $\mathrm T\mathcal M$ , with values in the Grassmann manifold $\mathrm{Gr}(n-d,\mathcal E)$ of $(n-d)$ -dimensional linear subspaces, such that $D(x,0)\cap\mathrm T_{\mathcal M}(x)=\{0\}$ for every $x\in\mathcal M$ . Given $D$ , set $\mathcal D(x,u)=x+u+D(x,u)$ and let

R(x,u)=\{\text{points of }\mathcal M\cap\mathcal D(x,u)\text{ nearest to }x+u\}.

Formalization targets

Goal: Theorem 4.2 (retractors give retractions)

\forall\bar x\in\mathcal M\ \ \exists r:\quad R(x,u)=\{r(x,u)\}\ \text{ for }(x,u)\in\mathrm T\mathcal M\text{ near }(\bar x,0),\quad\text{and } r \text{ is a retraction around } \bar x.

The theorem asserts both that the point-to-set map $R$ is single-valued near the zero section and that it is a retraction there.

Milestone: Lemma 4.7 (the normal case $D(x,u)=\mathrm N_{\mathcal M}(x)$ )

Near $(\bar x,0)$ there is one and only one smallest $v(x,u)\in\mathrm N_{\mathcal M}(x)$ with $x+u+v(x,u)\in\mathcal M$ ; $\mathrm D_u v(x,0)=0$ ; and $R(x,u)=x+u+v(x,u)$ is a retraction around $\bar x$ , hence on $\mathcal M$ .

Milestone: Lemma 4.8 (straightening up)

On a neighbourhood of the zero section, $D(x,u)=\{v+A(x,u)v:\ v\in\mathrm N_{\mathcal M}(x)\}$ for a unique linear $A(x,u):\mathrm N_{\mathcal M}(x)\to\mathrm T_{\mathcal M}(x)$ depending $C^{k-1}$ on $(x,u)$ .

Further: Theorem 4.9 (second order)

If $k\ge3$ and $D(x,0)=\mathrm N_{\mathcal M}(x)$ for all $x\in\mathcal M$ , then $\frac{\mathrm d^2}{\mathrm dt^2}R(x,tu)|_{t=0}\in\mathrm N_{\mathcal M}(x)$ for all $(x,u)\in\mathrm T\mathcal M$ .

Significance

Theorem 4.2 reduces the construction of a retraction to the choice of a smooth field of subspaces transverse to the tangent space at $u=0$ . The orthographic retraction ( $D=\mathrm N_{\mathcal M}(x)$ ) and the projective retraction $R(x,u)=P_{\mathcal M}(x+u)$ ( $D=\mathrm N_{\mathcal M}(P_{\mathcal M}(x+u))$ ) are both instances, as are the gnomonic, orthographic and stereographic projections on the sphere. Theorem 4.9 then certifies, by a check at $u=0$ only, that a retraction agrees with the exponential to second order, which matters for the superlinear convergence of Riemannian trust-region and Newton methods. Lemma 4.7 goes beyond an earlier result on tangential parameterizations (reference [28, Th. 3.4] of the paper) by giving $C^{k-1}$ regularity jointly in $(x,u)$ , not only in $u$ (Remark 4.4 of the paper).

The results are proved in the paper. None of them is machine-checked: Mathlib has the implicit function theorem and smooth manifolds, but no embedded submanifolds of a Euclidean space with their tangent and normal bundles, no retractions, and no smooth Grassmannian-valued maps. The work here is to formalize the known proof and to build this layer, which every later mission of this series (projective, spectral, fixed-rank and Stiefel retractions) also needs.

Difficulty

The statement is an implicit-function argument, but the obvious one does not apply directly. The unknown $v$ lives in the normal space $\mathrm N_{\mathcal M}(x)$ , which moves with $x$ , and $(x,u)$ ranges over the tangent bundle, a $C^{k-1}$ submanifold of $\mathcal E\times\mathcal E$ rather than an open set of a vector space. The equation has to be read in charts of the bundle, which costs one derivative; the uniqueness given by the implicit function theorem holds only locally in $(x,u,v)$ , and turning it into "the smallest $v$ ", or "the nearest point of $\mathcal M\cap\mathcal D(x,u)$ ", requires excluding far-away intersection points. For a general retractor, the subspace $D(x,u)$ also moves, and has to be written as a graph over the normal space with a $C^{k-1}$ dependence before a second implicit-function argument applies.

Formalization scope

$\mathcal E$ is a finite-dimensional real inner product space E, $n$ is Module.finrank ℝ E, and $k,d$ are natural numbers with $2\le k$ and $d\le n$ (the latter inside the submanifold definition). The coordinate slice uses an open partial homeomorphism E → EuclideanSpace ℝ (Fin n), $C^k$ in both directions, with 0-based coordinates. $\mathrm T_{\mathcal M}(x)$ is the span of Mathlib's tangent cone (chart-free), $\mathrm N_{\mathcal M}(x)$ its orthogonal complement. Retractions and retractors are total maps on $\mathcal E\times\mathcal E$ constrained only on $O\cap\mathrm T\mathcal M$ with $O$ open; "of class $C^{k-1}$ on a subset of $\mathrm T\mathcal M$ " is ContDiffOn on that set. A Grassmannian-valued map is $C^{k-1}$ when its orthogonal projector $P_{D(x,u)}$ is, and the dimension $n-d$ of $D(x,u)$ is part of the definition. The set-valued $R$ uses the published nearest-point predicate RandomGradFree.Nonsmooth.IsMetricProjection. In Lemma 4.8, $A(x,u)$ is extended by $0$ on $\mathrm T_{\mathcal M}(x)$ so that it is an operator on $\mathcal E$ . Theorem 4.9 assumes $k\ge3$ , the standing assumption of the definition of second-order retractions (display (2.3)), and reads the page's " $D(\bar x,0)=\mathrm N_{\mathcal M}(x)$ " as $D(x,0)=\mathrm N_{\mathcal M}(x)$ for all $x\in\mathcal M$ .

The goal is not satisfied by exhibiting some retraction: it requires the nearest-point set $R(x,u)$ to equal a singleton $\{r(x,u)\}$ (so it is nonempty) and that very $r$ to be a retraction. Theorem 4.9 requires the curve $t\mapsto R(x,tu)$ to be twice differentiable, so a junk second derivative of $0$ does not satisfy it.

A complete development needs: finite-rank facts for tangent spaces of slices ( $\dim\mathrm T_{\mathcal M}(x)=d$ ), smoothness of $x\mapsto P_{\mathrm N_{\mathcal M}(x)}$ , charts of $\mathrm T\mathcal M$ and of the Whitney sum $\mathrm T\mathcal M\oplus\mathrm N\mathcal M$ , ContDiffOn on submanifolds, and local orthonormal frames of a smooth field of subspaces. All of these are reusable beyond this mission. Contributions to any of them, and proofs of the two lemmas, are welcome.

Selected references

P.-A. Absil, J. Malick, Projection-like retractions on matrix manifolds, SIAM J. Optim. 22(1):135–158, 2012. https://doi.org/10.1137/100802529 (authors' version: https://hal.science/hal-00651608)
P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://press.princeton.edu/absil
R. L. Adler, J.-P. Dedieu, J. Y. Margulies, M. Martens, M. Shub, Newton's method on Riemannian manifolds and a geometric model for the human spine, IMA J. Numer. Anal. 22(3):359–390, 2002. https://doi.org/10.1093/imanum/22.3.359

10 thms2 active usersReviewed

Completed

Functional Analysis Machine Learning·Captain: mikedeng1

Theory of Reproducing Kernels IV: The Kernels of a Decreasing Sequence of Reproducing Kernel Classes Converge to the Kernel of the Limit ClassResearch Paper

Motivation

A reproducing kernel Hilbert space is a Hilbert space of functions on a set in which every point evaluation is continuous; the function $K(x,y)$ that represents evaluation at $y$ is its reproducing kernel. N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404, DOI 10.1090/S0002-9947-1950-0051437-7) gave the general theory of these spaces, which today underlies kernel methods in statistics and machine learning, Gaussian-process regression, and the Bergman and Szegő kernels of complex analysis.

Part I of the paper studies how kernels behave under the basic operations on classes of functions: sums, inclusions, products, restrictions, and limits. §9 treats limits. Its case A concerns a decreasing sequence of classes with increasing norms, defined on an increasing sequence of sets. The application in the paper's Part II is the computation of kernels of a domain by approximation from simpler domains: when a domain is exhausted by an increasing sequence of subdomains, the kernels of the subdomains converge to the kernel of the whole domain. This mission formalizes §9, Theorem I and the steps of its proof.

Setting

Let $X$ be an arbitrary set and $E_1\subset E_2\subset\cdots$ subsets with union $E = E_1+E_2+\cdots = X$ . For each $n$ let $F_n$ be a complex Hilbert space of functions on $E_n$ , with norm $\|\cdot\|_n$ , in which point evaluations are continuous; $K_n(x,y)$ , for $x,y\in E_n$ , is its reproducing kernel, characterized by $K_n(\cdot,y)\in F_n$ and

f(y) = (f, K_n(\cdot,y))_n \qquad (f\in F_n,\ y\in E_n),

with the scalar product $(f,g)_n$ linear in $f$ . For $f_n\in F_n$ and $m\le n$ , $f_{nm}$ denotes the restriction of $f_n$ to $E_m$ . The standing assumptions of §9 A (p. 362) are:

$E_1\subset E_2\subset\cdots$ and $E = \bigcup_n E_n$ ;
the classes decrease: $f_{nm}\in F_m$ for every $f_n\in F_n$ and $m\le n$ ;
the norms increase: $\|f_{nm}\|_m\le\|f_n\|_n$ for every $f_n\in F_n$ and $m\le n$ ;

together with the existence of every kernel $K_n$ . For two kernels on a set $Y$ , $K_1\ll K$ means that $K-K_1$ is a positive matrix: $\sum_{i,j}(K-K_1)(y_i,y_j)\,\bar\xi_i\xi_j\ge 0$ for all finite families $y_i\in Y$ , $\xi_i\in\mathbb C$ . $K_{nm}$ is the restriction of $K_n$ to $E_m\times E_m$ .

The limit class $F_0$ is the set of functions $f_0$ on $E$ such that (1°) every restriction $f_{0n}$ belongs to $F_n$ and (2°) $\lim_n\|f_{0n}\|_n<\infty$ .

Formalization targets

Goal: §9, Theorem I (pp. 362–363)

Under the standing assumptions there is $K_0 : E\times E\to\mathbb C$ such that, whenever $x,y\in E_N$ ,

\lim_{n\to\infty}K_n(x,y)=K_0(x,y),

and $K_0$ is the reproducing kernel of $F_0$ with the norm

\|f_0\|_0=\lim_{n\to\infty}\|f_{0n}\|_n .

Milestones (in the order the proof uses them)

§9, Eq. (4): $K_{nm}\ll K_m$ for $m<n$ .
§9, proof of Theorem I, p. 363: for $y\in E_k$ , $\{K_m(y,y)\}_{m\ge k}$ is a decreasing sequence of non-negative numbers.
§9, Eq. (5): for $y\in E_k$ , $k\le m\le n$ , $\|K_{mk}(\cdot,y)-K_{nk}(\cdot,y)\|_k^2\le K_m(y,y)-K_n(y,y)$ .
§9, Eq. (6): with $K_0$ the pointwise limit, $K_{0k}(\cdot,y)\in F_k$ and $\|K_{mk}(\cdot,y)-K_{0k}(\cdot,y)\|_k^2\le K_m(y,y)-K_0(y,y)$ .
§9, Remark after Theorem I: under 1°, $\|f_{0n}\|_n$ is non-decreasing, so its limit exists, possibly infinite.
§9, Eq. (7): if $F_0$ carries the limit norm, then $(f_0,g_0)_0=\lim_n(f_{0n},g_{0n})_n$ .

Significance

The result. Theorem I turns a monotone family of function spaces into a single space and identifies its kernel as the pointwise limit of the kernels. It reduces the computation of a kernel on a large set to kernels on an exhausting sequence of subsets, the method Aronszajn uses in Part II for Bergman-type kernels of plane domains. With $E_n=E$ for all $n$ (explicitly allowed on p. 362) it gives the limit of a decreasing sequence of kernels $K_1\gg K_2\gg\cdots$ on one set as the kernel of the intersection class with the limit norm. The milestones (4)–(6) are quantitative: (5) bounds the distance between restricted kernel sections by the decrease of the diagonal values, which yields strong convergence of $K_m(\cdot,y)$ in every $F_k$ .

Formalizing it. The theorem is classical and proved in the paper; to our knowledge no machine-checked proof exists. Mathlib has the RKHS class, the operator-valued kernel, the positive semidefiniteness of kernels and the Moore–Aronszajn construction RKHS.OfKernel, but nothing about restrictions of an RKHS to a subset, the order $\ll$ between kernels, or limits of sequences of reproducing kernel spaces. This mission produces those statements on Mathlib's RKHS vocabulary over $\mathbb C$ , with kernels on varying domains.

Difficulty

The kernels $K_n$ live on different sets $E_n\times E_n$ , so convergence is not convergence of a sequence of functions on one set: a pair $x,y$ enters the sequence only from the first $E_N$ containing both. The identification of the limit class needs three separate facts: that $F_0$ with the limit norm is a Hilbert space (the limit of norms must be shown to come from a scalar product, and completeness requires passing to the limit in two indices), that $K_0(\cdot,y)\in F_0$ , and that $K_0$ reproduces. The natural first idea, to embed all $F_n$ in one space and take an intersection, fails: the $F_n$ are spaces of functions on different sets, and their norms differ, so there is no common ambient Hilbert space; the comparison goes only through restriction and the inequalities (3). Eq. (4) itself uses §7, Theorem II (a contractively included Hilbert subclass has a dominated kernel) and the restriction theorem of §5, neither of which is in Mathlib.

Formalization scope

Scalars and spaces. Complex scalars throughout (Aronszajn works with complex Hilbert spaces from §1 on). Each $F_n$ is a type H n with [InnerProductSpace ℂ (H n)] [CompleteSpace (H n)] [RKHS ℂ (H n) (E n) ℂ], a space of functions on the subtype E n; the set $E$ is a type X with no topology, measure or nonemptiness assumption.
Kernel. The scalar kernel kernelFn H x y is Mathlib's RKHS.kernel H x y 1. Mathlib's inner product is conjugate-linear in the first slot, so Aronszajn's $(f,g)$ is ⟪g, f⟫_ℂ.
Standing assumptions. (1)–(3) are the structure IsDecreasingRKSequence; every statement takes it as a hypothesis. Restriction is pointwise agreement on $E_m$ . Indexing starts at $0$ .
Order. $K_1\ll K$ is KernelLE K₁ K := (Matrix.of K - Matrix.of K₁).PosSemidef, with Mathlib's positive semidefiniteness over an arbitrary index type (finitely supported vectors).
Comparisons of kernel values ( $K_m(y,y)\ge 0$ , the right-hand sides of (5), (6)) are in Mathlib's ComplexOrder, which also asserts that these values are real.
Convergence of kernels is stated only where the terms are defined: for $x,y\in E_N$ , the sequence $j\mapsto K_{N+j}(x,y)$ converges to $K_0(x,y)$ . Kernels are never extended by $0$ outside $E_n$ .
Condition 2° is convergence of $\|f_{0n}\|_n$ to a real number, not a supremum, and the norm of $F_0$ is stated as a limit (Tendsto).
The goal asserts (a) the convergence, (b) the existence of an RKHS on $X$ with kernel $K_0$ , and (c) that every RKHS on $X$ with kernel $K_0$ has exactly the functions of $F_0$ as its elements and the limit norm. A formalization that defines $F_0$ as RKHS.OfKernel K₀ and then asserts that its kernel is $K_0$ would be a tautology (RKHS.kernel_ofKernel); the goal instead characterizes the space by its functions and norm, as the paper does.
Eq. (7) is stated for an inner product space of functions whose norm is assumed to be the limit norm; the paper's derivation that the limit norm is a quadratic form is the content of the goal.
Non-vacuity. The constant sequence $E_n=E$ , $F_n=F$ satisfies the standing assumptions (checked in Lean), and the one-point example $F_n=\mathbb C$ with norms $c_n|f|$ , $c_n$ increasing, satisfies them with $K_n=c_n^{-2}$ .

Needed infrastructure, reusable beyond this mission: restriction of an RKHS to a subset (§5), the dominated-kernel theorem for contractive inclusions (§7, Theorem II), and the passage from a convergent sequence of norms to a convergent sequence of scalar products. Proofs of any milestone, and of these general facts as separate lemmas, are welcome.

Selected references

N. Aronszajn, Theory of Reproducing Kernels, Trans. Amer. Math. Soc. 68 (1950), no. 3, 337–404. https://doi.org/10.1090/S0002-9947-1950-0051437-7
E. H. Moore, General Analysis, Part I, Memoirs of the American Philosophical Society 1 (1935). (Positive matrices.)
Mathlib, Mathlib/Analysis/InnerProductSpace/Reproducing.lean (the RKHS class, RKHS.kernel, RKHS.OfKernel). https://github.com/leanprover-community/mathlib4

11 thms2 active usersReviewed

Completed

Functional Analysis Machine Learning·Captain: mikedeng1

Theory of Reproducing Kernels V: A Hermitian Kernel Represents a Bounded Symmetric Operator with Bounds m and M iff mK ≪ Λ ≪ MKResearch Paper

Motivation

Reproducing kernel Hilbert spaces are the function spaces of kernel methods in statistics and machine learning (Gaussian-process regression, support vector machines, kernel mean embeddings), of the Bergman and Szegő spaces of complex analysis, and of the theory of positive-definite functions. In all of these, bounded operators on the space (covariance operators, integral operators, projections onto subspaces, multiplication operators) are handled through functions of two points rather than through abstract operators. N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404) gives, in its §11, the dictionary between bounded operators on a space with a reproducing kernel and their kernels, and characterizes the kernels of bounded symmetric operators with prescribed bounds. Aronszajn credits the ideas of the section to E. H. Moore.

Setting

Let $E$ be an arbitrary set and let $F$ be a class of complex-valued functions on $E$ that forms a complex Hilbert space with scalar product $(f, g)$ , linear in $f$ and conjugate-linear in $g$ . A reproducing kernel of $F$ is a function $K : E \times E \to \mathbb{C}$ such that, for every $y \in E$ , the function $K(\cdot, y)$ belongs to $F$ and

f(y) = (f, K(\cdot, y)) \qquad \text{for every } f \in F.

Such a kernel exists exactly when every point evaluation $f \mapsto f(y)$ is continuous.

For a bounded linear operator $L$ on $F$ , with adjoint $L^*$ defined by $(Lf, g) = (f, L^* g)$ , the kernel of $L$ is

\Lambda(x, y) = L^*_x K(x, y),

the value at $x$ of the element $L^*(K(\cdot, y))$ of $F$ . By the reproducing property, $Lf(y) = (f, \Lambda(\cdot, y))$ for every $f \in F$ and $y \in E$ , so $L$ is determined by $\Lambda$ .

A function $P : E \times E \to \mathbb{C}$ is a positive matrix if $\sum_{i,j} \overline{\xi_i}\, P(y_i, y_j)\, \xi_j \ge 0$ for every finite family of points $y_i \in E$ and complex numbers $\xi_i$ . For two arbitrary functions $\Lambda_1, \Lambda_2$ on $E \times E$ , one writes $\Lambda_1 \ll \Lambda_2$ if $\Lambda_2 - \Lambda_1$ is a positive matrix. A bounded operator $L$ is symmetric if $L = L^*$ , and positive if $(Lf, f) \ge 0$ for every $f$ . A symmetric $L$ has lower bound $\ge m$ and upper bound $\le M$ if

m\,(f, f) \le (Lf, f) \le M\,(f, f) \qquad \text{for every } f \in F.

A kernel $\Lambda$ is hermitian symmetric if $\Lambda(x, y) = \overline{\Lambda(y, x)}$ .

Formalization targets

Goal: §11, Theorem I (p. 373)

For an arbitrary hermitian symmetric function $\Lambda : E \times E \to \mathbb{C}$ and real numbers $m, M$ :

\exists\, L \text{ bounded, symmetric, with } \Lambda = L^*_x K(x,y) \text{ and } m(f,f) \le (Lf,f) \le M(f,f)\ \ \forall f \quad\Longleftrightarrow\quad mK \ll \Lambda \ll MK .

The function $\Lambda$ is not assumed to have $\Lambda(\cdot, y) \in F$ ; that membership is part of what the condition yields.

Milestones

§11, (3): the kernel of the adjoint, $\Lambda^*(y, z) = \overline{\Lambda(z, y)}$ .
§11, (6): $L$ is symmetric if and only if $\Lambda$ is hermitian symmetric.
§11, (7): $L$ is positive if and only if $\Lambda$ is a positive matrix.
§11, (4): the kernel of a composition, $\Lambda(y, z) = (\Lambda_1(x, z), \overline{\Lambda_2(y, x)})_x$ for $L = L_1 L_2$ .
§11, Theorem II: if $L_n u \to L u$ weakly for every $u$ , then $\Lambda_n \to \Lambda$ pointwise; if $\|L_n - L\| \to 0$ , then $\Lambda_n \to \Lambda$ uniformly on every set of couples $(x, y)$ on which $K(x, x)$ and $K(y, y)$ are uniformly bounded.
§11, Theorem III, first sentence: for complete orthonormal systems $\{g'_m\}$ , $\{g''_n\}$ and $\alpha_{mn} = (g''_n, L g'_m)$ ,

\Lambda(x, y) = \lim_{p, q \to \infty} \sum_{m=1}^{p} \sum_{n=1}^{q} \alpha_{mn}\, g'_m(x)\, \overline{g''_n(y)} .

Significance

Theorem I identifies, by finite quadratic-form inequalities alone, which functions of two points are kernels of bounded symmetric operators and with which spectral bounds. It reduces statements about operators (boundedness, positivity, operator inequalities $mI \le L \le MI$ ) to statements about finitely many evaluations of kernels, the form in which they are checked in practice, for instance when a covariance or integral operator is shown to be bounded and positive from its kernel. The milestones make the correspondence $L \mapsto \Lambda$ a usable calculus: adjoints become conjugate transposes, composition becomes a scalar product in the middle variable, and limits of operators become limits of kernels.

All of these results are proved in the paper. None is formalized: Mathlib has reproducing kernel Hilbert spaces (RKHS), adjoints, positive operators and positive semidefinite matrices over arbitrary index types, but no kernel of an operator and none of the statements above. The mission produces machine-checked proofs of the §11 dictionary and of Theorem I.

Difficulty

The necessity half of Theorem I and milestones (3), (6), (4) follow from the reproducing property. The sufficiency half is where the work is: $\Lambda$ is an arbitrary function, and the hypothesis $mK \ll \Lambda \ll MK$ is only about finite families of points. One has to produce an operator on all of $F$ . The obvious attempt, defining $L$ on the dense span of the functions $K(\cdot, y)$ by the kernel and extending by continuity, needs the bound $|(\,L f, g)| \le C\|f\|\|g\|$ on that span, which does not follow directly from the two one-sided inequalities on the diagonal forms. The positivity of $\Lambda - mK$ and $MK - \Lambda$ does not by itself give the membership $\Lambda(\cdot, y) \in F$ , which the definition of the kernel of an operator requires. In milestone (7), positivity of an operator is a statement about all of $F$ , while positivity of the kernel only sees finite combinations of kernel functions; the passage between them uses density of these combinations.

Formalization scope

The space is Mathlib's RKHS ℂ H X ℂ: a complex Hilbert space H whose elements are functions X → ℂ on an arbitrary type X (no topology, no measure, not assumed nonempty), with continuous evaluations. The scalar kernel is the series' shared definition AronszajnRK.Sum.kernelFn H x y := RKHS.kernel H x y 1; the function $K(\cdot, y)$ is the element RKHS.kerFun H y 1.
The kernel of L : H →L[ℂ] H is opKernel L x y := (adjoint L) (kerFun H y 1) x. Mathlib's ⟪u, v⟫_ℂ is conjugate-linear in u, so the paper's $(f, g)$ is ⟪g, f⟫_ℂ, and every formula with a scalar product or a bar has been rewritten in that order. On a one-point $E$ with $F = \mathbb{C}$ , $K = 1$ and $L = cI$ , the kernel is $\bar c$ .
Positive matrices and $\ll$ are Matrix.PosSemidef of Matrix.of Λ over the index type X (finitely supported test vectors, ComplexOrder on ℂ); no finiteness of X is assumed.
Symmetric is IsSelfAdjoint L. "Positive" in (7) is ∀ f, 0 ≤ ⟪f, L f⟫_ℂ in ComplexOrder (real and nonnegative), without assuming self-adjointness, as in the paper. The bounds in Theorem I are bounds of the quadratic form, m‖f‖² ≤ Re⟪f, L f⟫ ≤ M‖f‖², not of the operator norm. The paper does not assume $m \le M$ and neither does the statement: for $m > M$ both sides hold exactly when $F = \{0\}$ and $\Lambda = 0$ .
In (4) the statement asserts that the functions $x \mapsto \Lambda_1(x, z)$ and $x \mapsto \overline{\Lambda_2(y, x)}$ are elements of H, and that the kernel of L₁ ∘L L₂ is their scalar product.
Weak convergence in Theorem II is ⟪v, Lₙ u⟫ → ⟪v, L u⟫ for all u, v; uniform convergence is ‖Lₙ − L‖ → 0 in operator norm.
In Theorem III the orthonormal systems are HilbertBasis with arbitrary index types, and the double limit is taken along growing finite sets of indices in both variables. For systems indexed by $\mathbb{N}$ this contains the paper's $\lim_{p,q}$ over $\{1..p\}\times\{1..q\}$ ; the general form also covers finite-dimensional spaces. The second sentence of Theorem III (kernels in $F \otimes \overline{F}$ correspond to operators of finite norm) needs the direct product $F \otimes \overline F$ and is not stated.
A trivializing formalization is ruled out: Theorem I quantifies over every hermitian function $\Lambda$ , not over functions already known to be kernels of operators, and the right-hand side is the finite-matrix condition, not a statement about an operator built from $\Lambda$ .
Not stated: the decomposition (8)–(9) into hermitian parts and the remark on general bounded operators (p. 374), and formula (5). Available substrate: RKHS, RKHS.kerFun_inner, RKHS.kerFun_dense, RKHS.posSemidef_kernel, ContinuousLinearMap.adjoint, ContinuousLinearMap.IsPositive and isPositive_iff_complex, HilbertBasis, Matrix.PosSemidef. Contributions welcome: a general lemma that a function $\Lambda$ with $0 \ll \Lambda \ll K$ is the kernel of an operator $0 \le L \le I$ , and the inclusion theorem $K_1 \ll K \Rightarrow F_1 \subset F$ , both reusable beyond this mission.

Selected references

N. Aronszajn, Theory of Reproducing Kernels, Trans. Amer. Math. Soc. 68 (1950), no. 3, 337–404. https://doi.org/10.1090/S0002-9947-1950-0051437-7
E. H. Moore, General Analysis, Part II, Mem. Amer. Philos. Soc. 1 (1939).
V. I. Paulsen and M. Raghupathi, An Introduction to the Theory of Reproducing Kernel Hilbert Spaces, Cambridge University Press, 2016. https://doi.org/10.1017/CBO9781316219232

10 thms2 active usersReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

The Łojasiewicz Inequality for Nonsmooth Subanalytic Functions with Applications to Subgradient Dynamical Systems II: The Łojasiewicz Inequality for Convex Subanalytic Functions on Bounded SetsResearch Paper

Motivation

The Łojasiewicz inequality states that near a critical point $a$ of a real-analytic function $f$ there are $\theta\in[0,1)$ and $C$ with $|f(x)-f(a)|^{\theta}\le C\,\|\nabla f(x)\|$ . Łojasiewicz used it in the 1960s to prove that every bounded trajectory of the gradient flow $\dot x=-\nabla f(x)$ has finite length and converges to a single critical point, a conclusion that fails for general $C^\infty$ functions. The inequality has since become the standard tool for convergence analysis of descent methods on nonconvex problems.

Optimization problems are, however, rarely smooth: constraints enter through indicator functions, and objectives contain norms, maxima and penalties. Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007) 1205–1223) extended the inequality to nonsmooth subanalytic functions, replacing $\|\nabla f\|$ by a slope built from the limiting subdifferential. Their Section 3.1 treats functions continuous on a closed domain; Section 3.2, the subject of this mission, treats lower semicontinuous convex functions, which may jump to $+\infty$ and whose domain need not be closed. The Kurdyka–Łojasiewicz framework built on this paper (Attouch–Bolte–Svaiter 2013; Bolte–Sabach–Teboulle 2014) underlies the convergence theory of proximal and splitting algorithms used throughout operations research.

Setting

Work in $\mathbb R^n$ with the Euclidean norm, and let $f:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ with domain $\operatorname{dom} f=\{x: f(x)<+\infty\}$ .

A set $A\subseteq\mathbb R^n$ is semianalytic if near every point it is a finite union of finite intersections of sets $\{f_{ij}=0,\ g_{ij}>0\}$ with $f_{ij},g_{ij}$ real-analytic. It is subanalytic if near every point it is the projection of a bounded semianalytic subset of $\mathbb R^n\times\mathbb R^m$ . A function is subanalytic when its graph $\{(x,\lambda): f(x)=\lambda\}$ is. Semialgebraic functions (norms, polynomials, indicators of polyhedra) are subanalytic.

The Fréchet subdifferential $\hat\partial f(x)$ is the set of $x^*$ with $\liminf_{y\to x,\,y\ne x}\big(f(y)-f(x)-\langle x^*,y-x\rangle\big)/\|y-x\|\ge 0$ , for $x\in\operatorname{dom} f$ , and is empty otherwise. The limiting subdifferential $\partial f(x)$ is the set of limits of $x_k^*\in\hat\partial f(x_k)$ with $(x_k,f(x_k))\to(x,f(x))$ . The nonsmooth slope is $m_f(x)=\inf\{\|x^*\|:x^*\in\partial f(x)\}$ , equal to $+\infty$ when $\partial f(x)=\emptyset$ , and $\operatorname{crit} f=\{x: 0\in\partial f(x)\}$ is the set of critical points. For lower semicontinuous convex $f$ , $\partial f$ is the subdifferential of convex analysis and $\operatorname{crit} f$ is the set of minimizers. Write $\min f$ for the minimum value and $d_S(x)$ for the distance from $x$ to $S=\operatorname{crit} f$ . The epigraphical sum $g(x)=\inf_u\{f(u)+\tfrac12\|x-u\|^2\}$ is the Moreau envelope of $f$ .

Ratios follow the paper's conventions $0^0=1$ and $\infty/\infty=0/0=0$ .

Formalization targets

Goal: Theorem 3.3

Let $f$ be lower semicontinuous, convex and subanalytic with $\operatorname{crit} f\ne\emptyset$ . For every bounded set $K$ there is $\theta\in[0,1)$ such that

\frac{|f-\min f|^{\theta}}{m_f}\quad\text{is bounded on }K.

The exponent may depend on $K$ ; neither $\theta$ nor the bound is fixed.

Milestones

Eq. (5): $\partial f=\hat\partial f=$ the convex subdifferential, for lsc convex $f$ .
Section 3.2: $\operatorname{crit} f$ is closed, convex and equal to the set of minimizers.
Inequality (16): $|f(x)-\min f|\le\|x^*\|\,d_S(x)$ for all $x^*\in\partial f(x)$ .
Remark 3.6: $|f-\min f|/m_f$ is bounded around every critical point, without subanalyticity.
Proposition 2.9: the epigraphical sum $g$ is $C^1$ and subanalytic when $\inf f\in\mathbb R$ .
Properties (a)–(c): $g$ is finite and $C^1$ , $g\le f$ , $\operatorname{crit} g=\operatorname{crit} f$ , $\inf g=\inf f$ .
Proposition 2.13(ii): $\operatorname{crit} f$ is subanalytic for subanalytic $f$ that is relatively bounded on its domain.
Section 2.1: the distance to a subanalytic set is subanalytic.
The Łojasiewicz factorization lemma on compact sets (recalled from Bierstone–Milman).
Inequality (15): $d_S(x)\le c^{-1/r}|f(x)-\min f|^{1/r}$ on $K$ , with $r>1$ , $c>0$ .
Remark 3.5: the growth condition $|f-\min f|\ge c\,d_S^{\,r}$ on a compact $K$ alone yields a Łojasiewicz inequality at critical points interior to $K$ .

Significance

Theorem 3.3 gives, for convex subanalytic functions, a Łojasiewicz inequality that is uniform on bounded sets rather than local at one critical point, and it needs neither continuity of $f$ on its domain nor a closed domain. Remark 3.4 of the paper exhibits a convex function covered by Theorem 3.3 but not by the continuous-case Theorem 3.1. Through inequality (20) of Section 4, it yields finite length and convergence rates for the subgradient flow $\dot x\in-\partial f(x)$ of such functions. The intermediate inequality (15) is a Hölderian error bound, $d_S\le C|f-\min f|^{1/r}$ , of the kind that drives linear and sublinear rate analyses of first-order methods.

The result is proved in the paper; no machine-checked version of it, or of the nonsmooth Łojasiewicz inequality in any form, is known. Formalizing it would add to the library: subanalytic sets and functions, the limiting subdifferential of convex functions and its agreement with the classical one, the Moreau envelope with its critical points and infimum, and the passage from a growth condition to a Łojasiewicz inequality. Remarks 3.5 and 3.6 isolate parts that need no subanalytic geometry at all.

Difficulty

The convex-analysis steps (inequality (16), properties of the Moreau envelope) are classical. The obstacle is subanalytic geometry. The natural first idea, applying the Łojasiewicz factorization lemma directly to $f-\min f$ and $d_S$ , fails: $f$ is neither continuous nor finite, and its domain need not be subanalytic even when $f$ is convex and subanalytic (Example 2.5 of the paper). The milestones route through the Moreau envelope, which is continuous and finite, but subanalyticity is not preserved by infima over unbounded sets, so the subanalyticity of the envelope (Proposition 2.9) needs a localization argument. The subanalyticity of $\operatorname{crit} g$ and of $d_S$ rests on the stability theory of subanalytic sets (Gabrielov's complement theorem, the projection theorem for globally subanalytic sets), none of which exists in Mathlib.

Formalization scope

The space is EuclideanSpace ℝ (Fin n). Functions take values in EReal; "lower semicontinuous, convex, somewhere finite and never $-\infty$ " is the published definition MoreauProx.Characterization.GammaZero, whose convexity is convexity of the epigraph. The Fréchet and limiting subdifferentials are the published NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff; the convex subdifferential subgrad appears only in Eq. (5), which proves the agreement and is never assumed. Semianalytic and subanalytic sets are defined from scratch for any finite-dimensional real normed space, so that one definition serves $\mathbb R^n$ and its products; global subanalyticity is not defined. $\min f$ is written $\inf_y f(y)$ in EReal and converted to a real number only where it is finite. The bounded ratio (14) is encoded as " $|f(x)-\min f|^{\theta}\le C\|x^*\|$ for every $x\in K$ and every $x^*\in\partial f(x)$ ", with real powers (Real.rpow, $0^0=1$ ). Inequalities (15) and (17) are imposed only where $f(x)<+\infty$ , since Lean sends $+\infty$ to $0$ under toReal.

Trivializing encodings are ruled out: the goal is stated with the limiting subdifferential rather than an assumed convex subdifferential, the slope is never computed in ℝ≥0∞ where $0\cdot\infty=0$ would make the ratio vacuous, and $\theta$ remains existential in $[0,1)$ with the quantifier order "for every $K$ there is $\theta$ ", so that $\theta=0$ is excluded at critical points in $K$ by $0^0=1$ .

A complete development needs a working theory of subanalytic sets (stability under finite unions, complements, closure, projections of bounded sets, the factorization lemma), the Moreau envelope of a convex function on $\mathbb R^n$ and its $C^1$ property, and the convex-analytic description of the limiting subdifferential. The subanalytic-geometry layer and the Moreau-envelope facts are reusable well beyond this mission; contributions to either, or proofs of the convex-only milestones (Eq. (5), (16), Remarks 3.5–3.6), are welcome independently.

Selected references

J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17(4) (2007) 1205–1223. https://doi.org/10.1137/050644641
E. Bierstone, P. D. Milman, Semianalytic and subanalytic sets, Publ. Math. IHÉS 67 (1988) 5–42. https://doi.org/10.1007/BF02699126
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
S. Łojasiewicz, Une propriété topologique des sous-ensembles analytiques réels, Les Équations aux Dérivées Partielles, Éditions du CNRS, Paris, 1963, 87–89.
H. Attouch, J. Bolte, B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems, Math. Program. 137 (2013) 91–129. https://doi.org/10.1007/s10107-011-0484-9
J. Bolte, S. Sabach, M. Teboulle, Proximal alternating linearized minimization for nonconvex and nonsmooth problems, Math. Program. 146 (2014) 459–494. https://doi.org/10.1007/s10107-013-0701-9

18 thms2 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

The Łojasiewicz Inequality for Nonsmooth Subanalytic Functions with Applications to Subgradient Dynamical Systems I: The Łojasiewicz Inequality at Critical Points of Continuous Subanalytic FunctionsResearch Paper

Motivation

For a real-analytic function $f : U \to \mathbb{R}$ on an open set $U \subseteq \mathbb{R}^n$ and a critical point $a$ (so $\nabla f(a) = 0$ ), the Łojasiewicz gradient inequality says that there is an exponent $\theta \in [0,1)$ such that $|f - f(a)|^{\theta} / \|\nabla f\|$ stays bounded near $a$ . It is the standard tool for proving that bounded gradient trajectories $\dot x = -\nabla f(x)$ have finite length and converge to a single critical point, and, in its descendants (the Kurdyka–Łojasiewicz property), for proving convergence of the whole iterate sequence of nonconvex descent methods: proximal gradient, alternating minimization, PALM, ADMM. Those algorithmic results all assume a nonsmooth version of the inequality, for functions that may take the value $+\infty$ and are not differentiable.

Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007)) supplied that nonsmooth version. This mission formalizes their first main result, Theorem 3.1: the inequality at critical points of subanalytic functions that are continuous on a closed domain.

Timeline.

1963: Łojasiewicz proves the inequality for real-analytic functions (Une propriété topologique des sous-ensembles analytiques réels), and in 1984 derives convergence of bounded analytic gradient trajectories.
1998: Kurdyka (Ann. Inst. Fourier 48) extends it to $C^1$ functions definable in an o-minimal structure, with a desingularizing function in place of the power.
2006: Bolte, Daniilidis and Lewis prove a nonsmooth Sard theorem (J. Math. Anal. Appl. 321): a subanalytic function continuous on its closed domain is constant on each connected component of its critical set.
2007: The present paper proves the nonsmooth inequality for continuous subanalytic functions (Theorem 3.1) and for lower semicontinuous convex ones (Theorem 3.3).
2007: Bolte, Daniilidis, Lewis and Shiota (SIAM J. Optim. 18) extend it to lower semicontinuous functions definable in o-minimal structures (the KL property).

Setting

Write $\mathbb{R}^n$ with its Euclidean norm. A function $f : \mathbb{R}^n \to \mathbb{R} \cup \{+\infty\}$ has domain $\operatorname{dom} f = \{x : f(x) < +\infty\}$ .

Subanalytic sets (Definition 2.1). A set $A \subseteq \mathbb{R}^n$ is semianalytic if every point of $\mathbb{R}^n$ has a neighbourhood $V$ on which $A \cap V = \bigcup_{i=1}^{p}\bigcap_{j=1}^{q}\{x \in V : f_{ij}(x) = 0,\ g_{ij}(x) > 0\}$ with $f_{ij}, g_{ij}$ real-analytic on $V$ . It is subanalytic if every point of $\mathbb{R}^n$ has a neighbourhood $V$ such that $A \cap V$ is the projection onto $\mathbb{R}^n$ of a bounded semianalytic subset of $\mathbb{R}^n \times \mathbb{R}^m$ , $m \ge 1$ . A function $f$ is subanalytic if its graph $\{(x,\lambda) \in \mathbb{R}^n \times \mathbb{R} : f(x) = \lambda\}$ is subanalytic. Semialgebraic functions, and functions locally built from analytic ones by finitely many algebraic operations, max/min and compositions, are subanalytic.

Subdifferentials (Definition 2.10). The Fréchet subdifferential $\hat\partial f(x)$ is the set of $x^*$ with $\liminf_{y \to x,\, y \ne x} \frac{f(y) - f(x) - \langle x^*, y - x\rangle}{\|y - x\|} \ge 0$ (empty off $\operatorname{dom} f$ ). The limiting subdifferential $\partial f(x)$ is the set of limits of $x^*_k \in \hat\partial f(x_k)$ along $x_k \to x$ with $f(x_k) \to f(x)$ .

Slope and critical points. The nonsmooth slope is $m_f(x) = \inf\{\|x^*\| : x^* \in \partial f(x)\}$ , equal to $+\infty$ when $\partial f(x) = \emptyset$ (equation (4)). The critical set is $\operatorname{crit} f = \{x : 0 \in \partial f(x)\}$ (Definition 2.11).

Formalization targets

Goal: Theorem 3.1

Let $f$ be subanalytic with closed domain and $f|_{\operatorname{dom} f}$ continuous, and let $a \in \operatorname{crit} f$ . Then there is $\theta \in [0,1)$ such that

\frac{|f - f(a)|^{\theta}}{m_f} \ \text{ is bounded around } a,

with the conventions $0^0 = 1$ and $\infty/\infty = 0/0 = 0$ . In division-free form: there are $C$ and a neighbourhood $U$ of $a$ with $|f(x) - f(a)|^{\theta} \le C\|x^*\|$ for all $x \in U$ and $x^* \in \partial f(x)$ . The exponent is existential; the goal fixes no value of $\theta$ or $C$ .

Milestones

Remark 2.12, for $f$ continuous on a closed domain: the graph of $\partial f$ is closed; $\operatorname{crit} f$ is closed; $m_f$ is lower semicontinuous; $\operatorname{crit} f = m_f^{-1}(0)$ .
Proposition 2.13(ii), its clause on the critical set: if $f$ is subanalytic and relatively bounded on its domain, then $\operatorname{crit} f$ is subanalytic.
Equation (6), recalled from the nonsmooth Sard theorem: $f$ is constant on the connected component of $\operatorname{crit} f$ containing $a$ .
The curve selection lemma, recalled from Bierstone–Milman: a boundary point of a subanalytic set is the origin of an analytic arc entering the set.

Significance

The result. Theorem 3.1 is the nonsmooth Łojasiewicz inequality at critical points. With the subgradient in place of the gradient, it yields finite length of bounded trajectories of subgradient systems $\dot x \in -\partial f(x)$ (Section 4 of the paper) and is the template for the Kurdyka–Łojasiewicz property that underlies convergence proofs for proximal and splitting methods on nonconvex, nonsmooth problems (e.g. Attouch–Bolte–Redont–Soubeyran 2010, Bolte–Sabach–Teboulle 2014). Those papers assume the KL property and cite this line of results to know it holds for semialgebraic and subanalytic objectives.

Formalizing it. The theorem is proved; this mission produces a machine-checked proof. To our knowledge no proof assistant has a formal definition of subanalytic sets or of the nonsmooth Łojasiewicz inequality. The definitions layer (semianalytic and subanalytic sets, the slope, the inequality) is reusable by any later formalization of KL-based convergence analyses, and the milestones on Remark 2.12 are general facts about limiting subdifferentials that apply well beyond subanalytic geometry.

Difficulty

The obvious argument restricts $f$ and $m_f$ to an analytic curve and compares their Puiseux expansions. That step needs three pieces of subanalytic geometry that no library has: curve selection, the structure of one-variable subanalytic functions (monotonicity and Puiseux expansions), and the fact that the sets built in the proof (sets of points with a subgradient satisfying an inequality, level-wise infima of $m_f$ ) are again subanalytic, which in the paper goes through global subanalyticity and the projection theorem. The second obstacle is that $f$ is not smooth: the classical proof differentiates $f$ along a curve, while here only Fréchet subgradients are available, and the chain rule along an analytic curve holds only almost everywhere. The constancy of $f$ on critical components, equation (6), is itself a nonsmooth Sard-type theorem whose published proof uses stratification. A solver who replaces subanalytic by semialgebraic, or assumes $f$ real-valued and $C^1$ , proves a different and much weaker statement.

Formalization scope

Space and values. The space is EuclideanSpace ℝ (Fin n). The function is f : E → EReal with f x ≠ ⊥ for every x. The domain is {x | f x ≠ ⊤}; it is assumed closed, and f is assumed ContinuousOn it.
Subdifferentials. $\hat\partial f$ and $\partial f$ are the published platform definitions NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff, which match Definition 2.10 for functions never equal to $-\infty$ .
Subanalyticity. It is defined on any finite-dimensional real normed space, so that the same definition covers $\mathbb{R}^n$ , $\mathbb{R}^n \times \mathbb{R}$ and $\mathbb{R}^n \times \mathbb{R}^m$ . Analyticity is AnalyticOnNhd ℝ. The boundedness of the semianalytic set in Definition 2.1(ii) is part of the definition: without it every projection of a semianalytic set would count.
Slope. The slope is valued in $[0,+\infty]$ , with $+\infty$ on points without subgradients.
The inequality. It is the predicate LojIneqAt f a θ: one constant $C$ and one neighbourhood of $a$ , quantified over all limiting subgradients. Under $0^0 = 1$ the value $\theta = 0$ never works at a critical point, as under the paper's conventions.
Not assumed. The goal does not assume lower semicontinuity, real values, global subanalyticity, compactness of the critical set, or $f(a) = 0$ . These are reductions inside the paper's proof. Any formalization that adds them, fixes $\theta$ , or replaces the class of $f$ by semialgebraic or $C^1$ functions trivializes the target.
Infrastructure. A complete proof needs: curve selection; the monotonicity lemma and Puiseux expansions for one-variable globally subanalytic functions; the projection theorem or an equivalent definability argument; the nonsmooth Sard theorem (6); and a chain rule for Fréchet subgradients along analytic curves. Each of these is welcome as a separate contribution, and the subanalytic-geometry results are reusable well beyond this mission.

Selected references

J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17 (2007) 1205–1223. https://doi.org/10.1137/050644641
J. Bolte, A. Daniilidis, A. Lewis, A Sard theorem for non-differentiable functions, J. Math. Anal. Appl. 321 (2006) 729–740.
E. Bierstone, P. Milman, Semianalytic and subanalytic sets, Publ. Math. IHÉS 67 (1988) 5–42. https://doi.org/10.1007/BF02699126
K. Kurdyka, On gradients of functions definable in o-minimal structures, Ann. Inst. Fourier 48 (1998) 769–783. https://doi.org/10.5802/aif.1638
J. Bolte, A. Daniilidis, A. Lewis, M. Shiota, Clarke subgradients of stratifiable functions, SIAM J. Optim. 18 (2007) 556–572. https://doi.org/10.1137/060670080
S. Łojasiewicz, Une propriété topologique des sous-ensembles analytiques réels, in Les Équations aux Dérivées Partielles, CNRS, Paris, 1963, 87–89.
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Grundlehren 317, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

12 thms2 active usersReviewed

Completed

Functional Analysis Numerical Analysis·Captain: mikedeng1

Theory of Reproducing Kernels VI: The Projection onto the Closed Sum of Two Subspaces as a Series in the Two ProjectionsResearch Paper

Motivation

An orthogonal projection onto a closed subspace is straightforward to describe when that subspace is given directly. It is less straightforward when the subspace is specified as the closed sum of two others: a vector can have contributions from both, and the two component projections generally do not commute. In §12 of Aronszajn's 1950 paper, this problem arises while expressing the reproducing kernel of a sum of two closed subspaces of a reproducing-kernel Hilbert space through their individual kernels. The projection formula is the analytic heart of that calculation. It also gives a series whose finite partial sums can be applied without first describing a basis for the closed sum.

Aronszajn states the result for closed subspaces of a complex Hilbert space of functions. The projection identity itself uses only Hilbert-space geometry; evaluation at a point and the reproducing property enter when the operator formula is translated into a kernel formula later in the section. This mission isolates the projection theorem so that the same formal result can be used both in that kernel calculation and in other settings with two closed subspaces.

Setting

Let $E$ be a complex Hilbert space and let $F_1,F_2$ be closed linear subspaces. The algebraic sum $F_1+F_2$ is the set of all $f_1+f_2$ with $f_i\in F_i$ . It need not be closed. Write $F'=\overline{F_1+F_2}$ for its closure and $F_0=F_1\cap F_2$ for the intersection. All four subspaces are closed except possibly the algebraic sum itself. Let $P_1,P_2,P,P_0$ be the orthogonal projections onto $F_1,F_2,F',F_0$ , respectively. Operator products denote composition, with the rightmost factor applied first; $(P_2P_1)^0$ is the identity.

The paper writes $F_1\oplus F_2$ for $F'$ , even when $F_0$ is nonzero, and uses a distinct dotted plus for the algebraic sum. These symbols can look like a direct sum in newer notation. Here the definitions of $F'$ and $F_0$ remove that ambiguity. Aronszajn assumes complex scalars throughout Part I after §1, p. 343; the statements below keep that convention. Neither a topology on an underlying set of functions nor a measure is part of these operator assertions.

Formalization targets

The goal is the strong projection series, §12, Eq. (7). For each $f\in E$ ,

Pf=P_0f+\sum_{k=1}^{\infty}\left[P_1(P_2P_1)^{k-1}+P_2(P_1P_2)^{k-1}-(P_2P_1)^k-(P_1P_2)^k\right]f.

The sum means that its finite partial sums converge in the norm of $E$ for each fixed $f$ . No operator-norm limit is claimed. The first term of the sum, at $k=1$ , includes $P_1+P_2-P_2P_1-P_1P_2$ because both zero powers are identity operators.

Three source statements are milestones. Equation (1) is a finite identity that expresses a power of $(P-P_1)(P-P_2)$ through a partial sum and a power of $P_2P_1$ . The paragraph following Eq. (4) identifies the strong limit of $(P_2P_1)^m$ as $P_0$ . The paragraph before Eq. (7) asserts that $[(P-P_1)(P-P_2)]^m$ tends strongly to zero. Together these statements specify the finite and limiting parts of the displayed target. They require no assumption that $F_0$ is zero.

Significance

The formula describes the orthogonal projection onto a closed sum in terms of projections onto its two constituents. In Aronszajn's application, an orthogonal projection on a closed subspace determines that subspace's reproducing kernel; therefore the operator expansion supplies a kernel expansion without constructing a basis of the sum. It also makes explicit why an intersection term survives when the subspaces overlap. The result is proved in the 1950 paper; this mission asks for a Lean proof of that known result, with its convergence mode and closure convention made explicit.

A machine-checked development would provide a reusable complex-Hilbert-space statement for alternating projections and closed sums. Mathlib already provides closed submodules and their orthogonal projections, so the new contribution is the finite identity and the strong-limit claims connecting them. The resulting theorem can support the paper's later kernel expression, §12, Eq. (18), once the correspondence between bounded operators and kernels from §11 is available. Equation (18) is outside this mission's target list.

Difficulty

The algebraic sum of two closed subspaces can fail to be closed, so projecting onto it directly would leave the target undefined as a Hilbert-space orthogonal projection. Passing to its closure gives the correct target but does not imply the two projections commute or that their product has a uniform contraction factor. In particular, strong convergence of the powers and of the final series does not generally improve to convergence in operator norm. The later special case in §12, where the intersection is zero and the minimal angle is positive, has a stronger uniform-convergence conclusion; that extra angle condition is absent from Eq. (7).

The finite formula also has four terms per summand whose order matters. Reversing $P_1P_2$ and $P_2P_1$ , beginning the power at $k$ rather than $k-1$ , or omitting $P_0$ changes the statement. Even a proof of pointwise convergence of each selected term would not by itself establish the convergence of the bracketed partial sums in the target.

Formalization scope

The Lean representation is an arbitrary complex Hilbert space E with two ClosedSubmodule ℂ E objects. Mathlib's Submodule.starProjection supplies $P_1$ and $P_2$ . Two small definitions name $P$ as projection onto the join of the closed submodules and $P_0$ as projection onto their meet. The closed-submodule join is the closure of the algebraic sum; the meet is the intersection. These definitions are computed from $F_1,F_2$ , not independently quantified projections. The theorem quantifies over every vector $f$ and uses Filter.Tendsto along natural-number partial sums, giving norm convergence of the resulting vectors.

The source's ambient class has a reproducing kernel, but no step in Eqs. (1)–(7) uses point evaluations. The formal statements therefore apply to any complex Hilbert space, including the paper's RKHS. The stronger scope is explicit here and does not assert a new kernel identity. The $m$ -th Lean partial sum uses indices $0,\ldots,m-1$ for the paper's $1,\ldots,m$ ; it has the same terms and is defined at $m=0$ as $P_0f$ . The finite identity is stated only for $m\ge1$ , as its $m=0$ version is false in general.

Eq. (1) on p. 375 is printed without the opening bracket of the summand (only the closing bracket appears); the formalization reads it as in Eq. (4) on p. 376, where both brackets are printed. There are two printing slips on p. 377: a running sentence drops brackets from the power of $(P-P_1)(P-P_2)$ , and it prints $P\ominus P_2$ while discussing the projection $P-P_2$ . The formalization follows the bracketed expression in Eqs. (1) and (4), using ordinary operator subtraction. The corresponding milestone preserves the printed wording. No assumption from the later angle analysis, especially $F_0=\{0\}$ , is imported into these results. The series is stated through actual partial sums; it is not defined by an arbitrary RKHS chosen to have a desired kernel.

Selected references

N. Aronszajn, Theory of Reproducing Kernels, Transactions of the American Mathematical Society 68 (1950), 337–404, §12, pp. 375–380. DOI: 10.1090/S0002-9947-1950-0051437-7.

6 thms2 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Elements of Queueing Theory Ib: Ergodicity and Stochastic IntensityTextbook

Ergodicity and Stochastic Intensity

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory has two halves. The first builds Palm calculus from the Matthes definition of P⁰_N and reaches the Swiss army formula. This mission is the second: §§1.6, 1.8 and 1.9, which supply the two things the rest of the book runs on.

Ergodic theory, quoted

§1.6 states, in its own words, "the ergodic theory results to be used later in this book". Five of them, and the book proves none: Birkhoff's pointwise ergodic theorem in discrete (Theorem 1.6.1) and continuous time (Theorem 1.6.4), Kingman's sub-additive ergodic theorem (Theorem 1.6.2), and the extremal characterizations of ergodicity in both settings (Theorems 1.6.3 and 1.6.5) — ergodicity is exactly the impossibility of splitting an invariant probability into two distinct ones.

They are quoted, but they are not decoration. Kingman's theorem is what produces the asymptotic growth rates of Theorem 2.11.2 and the constant γ(c) on which the saturation rule rests. Birkhoff's theorem is what makes the time average in PASTA's (3.3.2) a well-defined object, and what the fluid Loynes theorem invokes for lim_{u→−∞}(A_{u,0} − C_{u,0}) = −∞.

None of the three analytic ones exists in Mathlib. Analysis/InnerProductSpace/MeanErgodic is the mean (von Neumann, L²) theorem, not almost-everywhere convergence, and there is no sub-additive ergodic theorem at all. The platform has neither.

Predictability, and why PASTA can be stated

§1.8 introduces the stochastic intensity: a point process N admits the (P, F_t)-intensity {λ(t)} when E[N(a,b] 1_A] = E[(∫_a^b λ(t)dt) 1_A] for A ∈ F_a. Around it sits the notion of a predictable process — one measurable with respect to the strict past.

Theorem 1.8.1 is the structural fact that makes predictability usable. For the internal history of a marked point process, every predictable process has the concrete form

Z(t, ω) = v(t, θ_t ω),    v(t, ·) F_{0−}-measurable.                                   (1.8.1)

That is why mission IV can take this form as PASTA's hypothesis rather than constructing a predictable σ-field: Theorem 1.8.1 says nothing is lost.

The goal

Theorem 1.8.2 (p.61), §1.8.4, Watanabe's characterization of Poisson processes. For a history F_t = F_t^N ∨ G and a G-measurable, locally integrable {λ(t)}, if N admits the F_t-intensity {λ(t)} then N is a G-conditional Poisson process:

E[ e^{iuN(a,b]} | G ∨ F^N_a ] = exp{ (e^{iu} − 1) ∫_a^b λ(t) dt } .                    (1.8.12)

A stochastic intensity that carries no information beyond G forces the process to be Poisson conditionally on G, with the compensator as the parameter — and the conditional characteristic function is the exact Poisson one, not an approximation. With G trivial and λ constant this is the ordinary Poisson process, which is the equivalence Remark 3.3.1 of Chapter 3 invokes to explain the name PASTA. The book: "This result plays a role in queueing theory, especially for proving that some streams in a queueing network are or are not Poissonian."

Palm probability meets stochastic intensity

§1.9 asks whether the stochastic intensity is the same under P and under P⁰_N — whether the two probabilities describe the same dynamics. Theorem 1.9.1 says yes, on ℝ₊: the same process {λ(t)} serves both.

Theorem 1.9.2 is Papangelou's theorem, and it is the deepest statement of the section: N admits a stochastic intensity if and only if P⁰_N ≪ P on F_{0−}, and then λ(t) = (μ ∘ θ_t)λ with μ the Radon–Nikodým derivative. A dynamic property and a static one turn out to be the same thing.

Theorem 1.9.3 is Mecke's characterization: N is Poisson exactly when P ≡ P⁰_N on F_{0−}. The view from a point of the process and the view from a deterministic instant agree on the strict past precisely when the process has no memory. It follows in one line from the two theorems before it.

What this mission provides

Four of the five missions in this series import the Chapter 1 substrate; this one adds the two pieces they need from its second half — ergodic theory and the stochastic intensity. Nothing here is on the platform, and Mathlib has filtrations and adapted processes but no predictability in this form, no stochastic intensity, no pointwise ergodic theorem and no Kingman.

Formalization scope

Every result is stated in the book's strength, with the book's standing definitions as binders. A discrete flow is a bijective, measurable, P⁰-preserving map (p.46); a continuous flow is jointly measurable in (t, ω) (p.3, clause (a)). A history compatible with the flow satisfies θ_t F_s = F_{s−t} (p.57), and an F_t-intensity is a non-negative, measurable, locally integrable, adapted process (p.58). The limits of Theorems 1.6.1, 1.6.2 and 1.6.4 are asserted to exist; Kingman's constant h̄ lies in ℝ ∪ {−∞} and is identified with inf_n (1/n) E⁰[h_n], the means being extended reals so that E⁰[h_n] = −∞ is not read as 0. Theorems 1.6.3, 1.6.5, 1.9.2 and 1.9.3 are equivalences, and Theorem 1.9.2 carries the closed form λ(t) = (μ ∘ θ_t)λ with μ = dP⁰_N/dP on F_{0−}. The goal's conclusion is the exact conditional characteristic function (1.8.12); a formalization that only asserted some conditional Poisson law, or conditioned on G alone, would not be this theorem.

13 thms2 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Elements of Queueing Theory I: The Swiss Army Formula of Palm CalculusTextbook

The Swiss Army Formula of Palm Calculus

Background

Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds the calculus that the rest of the book runs on. Its subject is the relation between two ways of looking at the same stationary system: from a clock fixed in time, and from a customer arriving into it. The two are not the same — the interval a random instant falls into is longer than a typical interval, a fact every queueing student meets as the inspection paradox — and the object that makes the difference precise is the Palm probability P⁰_N.

The chapter defines P⁰_N by the Matthes definition in terms of counting,

λ t P⁰_N(A) = E[ Σ_{n ∈ ℤ} 1_A(θ_{T_n}) 1_{(0,t]}(T_n) ],                          (1.2.1)

and everything else is a theorem about it. That ordering is deliberate here too: P⁰_N is carried in the formalization as a predicate satisfying (1.2.1), not as a measure constructed to make Mecke's formula true. If it were the latter, Mecke's formula would be a definition and the inversion formula and the goal theorem would inherit that emptiness.

From (1.2.1) the chapter derives, in order: that P⁰_N is invariant under the point shift (1.2.16); Mecke's formula (1.2.17), which the literature also knows as the generalized Campbell formula; the inversion formula of Ryll-Nardzewski and Slivnyak (1.2.25), which runs back from P⁰_N to P; the mean-value formulas (1.3.2)–(1.3.3); the Neveu exchange formula (1.3.4), which relates two point processes stationary for the same flow; and the Miyazawa rate conservation principle (1.3.10), which balances the drift of a process between its jumps against the rate at which it jumps.

The goal

§1.3.7 then collects all of them into one identity. Its name is the book's own:

Depending on which blade is selected, a Swiss army knife transforms itself into various useful tools. The formula obtained in this subsection is called the Swiss army formula of Palm calculus because it contains the main formulas of this theory, as well as some new ones.

Theorem 1.3.1 (p.29). For arrivals {T_n} with counting measure A and intensity λ_A, departures {τ_n} with counting measure D — not assumed ordered — sojourn times W_n = τ_n − T_n ≥ 0 forming a sequence of marks of A, the number in system {X(t)} with X(b) − X(a) = A((a,b]) − D((a,b]), a non-decreasing corlol integrator {B(t)} and a non-negative process {Z(t)}, all compatible with a measurable flow under which P is invariant:

λ_A E⁰_A [ ∫_(0,W_0] Z(s) dB(s) ] = (1/t) E [ ∫_(0,t] X(s−) Z(s) dB(s) ].              (1.3.28)

Selecting the blade Z ≡ 1, B(t) = t turns it into λ_A E⁰_A[W_0] = E[X(0)] — Little's law, here in its full stationary-ergodic form rather than as a deterministic sample-path identity. Other choices give the inversion formula, the Miyazawa conservation principle and the rate conservation law.

The local meaning of `P⁰_N`

One milestone stands slightly apart. Theorem 1.5.1 (p.45) is what licenses the whole reading of P⁰_N as "what an arriving customer sees":

lim_{t→0} sup_{A ∈ F} | P⁰_N(A) − P(θ_{T_1} ∈ A | T_1 ≤ t) | = 0.                       (1.5.3)

The supremum is inside the limit. The convergence is uniform over every measurable event, which is what Dobrushin's estimate of §1.5.1 buys and what a pointwise limit would not give.

What this mission provides

Nothing in this chapter exists on the platform or in Mathlib: not stationary marked point processes, not Palm probability, not the Campbell measure. Four of the five missions in this series import the vocabulary built here, and the two definition items — the substrate of §§1.1–1.2 and the setting of §1.3.7 — are as much of the deliverable as the theorems are.

Formalization scope

The flow {θ_t} is a one-parameter group with (t, ω) ↦ θ_t ω jointly measurable (p.5 (a)); a point process is its strictly increasing points {T_n}_{n ∈ ℤ} with T_0 ≤ 0 < T_1, infinitely many on each side (Hypothesis 1.1.1), with finite non-null intensity λ = E[N((0,1])].
P⁰_N is characterized by (1.2.1) for every t > 0, which determines it uniquely; nothing is axiomatized. A formalization that introduced P⁰_N as any measure satisfying Mecke's formula would make the milestones and the goal trivial and is ruled out.
Every "for all non-negative measurable" formula (Mecke, inversion, mean-value, Neveu, Wald, the goal) is stated in [0, ∞] with lower Lebesgue integrals, for all such functions, not only bounded or integrable ones.
Three hypotheses the book uses without listing them are explicit: the Swiss army formula assumes the integrator {B(t)} is θ_t-compatible (the proof uses it, and without it the identity fails); it is stated for t > 0, the only values at which 1/t and (0, t] give it content; and the Miyazawa principle assumes Y'(0) ∈ L¹(P), which its E[Y'(0)] presupposes.
Theorem 1.5.1 keeps the supremum over all events inside the limit (one δ for every A).

11 thms2 active usersReviewed

Algebra·Captain: Lucas

Smale's Mean Value ConjectureOpen Problem

Motivation

The mean value problem, also called Smale's mean value conjecture, was posed by Stephen Smale in 1981 in his study of the complexity of root-finding algorithms for polynomials (Smale 1981). For a real differentiable function the mean value theorem produces, between two points, a point where the derivative equals a difference quotient. For a complex polynomial no such point need exist on a segment, and Smale asked for a substitute in which the special point is a critical point of the polynomial (a zero of its derivative). Estimates of this kind control how far Newton-type iterations can move, which is where Smale's original interest came from. The problem appears in lists of unsolved problems in mathematics, including Smale's own list of problems for the next century.

Timeline

1981 — Smale poses the problem and proves the inequality below with constant $K = 4$ (Smale 1981). The example $P(z) = z^d - dz$ shows that the constant cannot be smaller than $\frac{d-1}{d}$ in degree $d$ , so no constant below $1$ works in all degrees.
1989 — Tischler proves the inequality with the optimal constant $K = \frac{d-1}{d}$ when all roots of $P$ are real, and when all roots of $P$ have the same absolute value (Tischler 1989).
2007 — Conte, Fujikawa and Lakic prove $K \le 4\frac{d-1}{d+1}$ (Conte–Fujikawa–Lakic 2007). Crane proves $K < 4 - \frac{2.263}{\sqrt d}$ for $d \ge 8$ (Crane 2007).
2009 — Dubinin and Sugawa prove the reverse (dual) inequality with constant $\frac{1}{d\,4^d}$ (Dubinin–Sugawa 2009); optimizing this lower bound is the dual mean value problem (Ng–Zhang 2016).

No absolute constant $K < 4$ is known that works in every degree.

Setting

Let $P$ be a polynomial with complex coefficients of degree $d \ge 2$ , and write $P'$ for its derivative. A critical point of $P$ is a complex number $c$ with $P'(c) = 0$ ; since $d \ge 2$ , $P'$ is a nonconstant polynomial of degree $d-1$ , so $P$ has at least one and at most $d-1$ distinct critical points. Fix a complex number $z$ that is not a critical point, $P'(z) \ne 0$ . For every critical point $c$ we then have $c \ne z$ , and the difference quotient

\frac{P(z) - P(c)}{z - c}

is well defined. The question is how small this quotient can be made, relative to $|P'(z)|$ , by choosing the critical point $c$ well.

Formalization targets

Goal: Smale's mean value conjecture ( $K = 1$ )

For every complex polynomial $P$ of degree $d \ge 2$ and every $z \in \mathbb C$ with $P'(z) \ne 0$ there is a critical point $c$ of $P$ with

\left| \frac{P(z) - P(c)}{z - c} \right| \le |P'(z)|.

Stronger: the optimal constant

The same with $|P'(z)|$ replaced by $\frac{d-1}{d}\,|P'(z)|$ ; the example $z^d - dz$ shows this constant cannot be lowered.

Known results (milestones)

Smale's inequality with $K = 4$ .
The extremal example $P(z) = z^d - dz$ at $z = 0$ , where every critical point gives exactly $\frac{d-1}{d}|P'(0)|$ , and its consequence that no constant $K < 1$ works in all degrees.
Tischler's optimal inequality for polynomials with only real roots, and for polynomials whose roots all have the same absolute value.
The Conte–Fujikawa–Lakic bound $K \le 4\frac{d-1}{d+1}$ .
Crane's bound $K < 4 - \frac{2.263}{\sqrt d}$ for $d \ge 8$ .
The Dubinin–Sugawa dual inequality $\left|\frac{P(z)-P(c)}{z-c}\right| \ge \frac{|P'(z)|}{d\,4^d}$ for some critical point $c$ .

Significance

The result itself. A positive answer gives a sharp, degree-independent mean value inequality for complex polynomials: for every non-critical point, some critical value is reachable along a chord whose slope is at most the local derivative. Bounds of this type feed into the analysis of Newton's method and of path-following root finders, and into the study of how critical values of a polynomial are distributed relative to its values. The conjecture is part of a family of open extremal problems on the geometry of critical points, alongside Sendov's conjecture.

Formalizing it. The goal and the optimal-constant form are open. The milestones are published theorems, none of which is known to have a machine-checked proof. Formalizing Smale's $K = 4$ bound and Tischler's special cases would put the classical tools of the subject (critical points of polynomials, univalent function estimates, root location) on a formal footing that later attempts can reuse.

Difficulty

The obvious strategies control the quotient through one critical point at a time: for instance, bounding $|P(z) - P(c)|$ by integrating $P'$ along the segment from $c$ to $z$ . Such estimates lose a constant factor that depends on how the critical points are spread out, and the known uniform arguments all pass through distortion theorems for univalent functions, whose constants lead to $K$ close to $4$ . Reaching $K = 1$ requires using all critical points simultaneously, and no argument doing this in every degree is known. The equality case $z^d - dz$ , in which every critical point is equally bad, shows that any successful argument must be sharp for polynomials with maximally symmetric critical configurations.

Formalization scope

Polynomials are elements of ℂ[X] (Mathlib's Polynomial ℂ); the degree is natDegree, the derivative is Polynomial.derivative, evaluation is Polynomial.eval, and the roots of $P$ are the multiset P.roots (counted with multiplicity). A critical point is a c : ℂ with P.derivative.eval c = 0. The absolute value is the norm ‖·‖ on ℂ, and the constants $\frac{d-1}{d}$ and $4\frac{d-1}{d+1}$ are computed in ℝ from the cast of natDegree.

Every statement assumes $P'(z) \ne 0$ . This is the standard normalization and is essential in Lean: division by zero returns $0$ , so without it the choice $c = z$ would make the inequality trivially true whenever $z$ is itself a critical point. With the hypothesis, every critical point $c$ differs from $z$ and the quotient is a genuine difference quotient.

Crane's bound is stated as the existence, for each degree $d \ge 8$ , of a constant strictly below $4 - \frac{2.263}{\sqrt d}$ that works for all polynomials of degree exactly $d$ ; this is equivalent to the best constant in degree $d$ being strictly below that value.

A complete development needs basic facts on critical points of complex polynomials (existence, the Gauss–Lucas theorem), and, for the classical bounds, results from the theory of univalent functions such as the Koebe quarter theorem and coefficient estimates. These are reusable well beyond this mission. Contributions of any milestone, of supporting lemmas, and of partial results in fixed small degree are welcome.

Selected references

S. Smale, The fundamental theorem of algebra and complexity theory, Bull. Amer. Math. Soc. (N.S.) 4 (1981), 1–36. https://doi.org/10.1090/S0273-0979-1981-14858-8
D. Tischler, Critical points and values of complex polynomials, J. Complexity 5 (1989), 438–456. https://doi.org/10.1016/0885-064X(89)90019-8
A. Conte, E. Fujikawa, N. Lakic, Smale's mean value conjecture and the coefficients of univalent functions, Proc. Amer. Math. Soc. 135 (2007), 3295–3300. https://doi.org/10.1090/S0002-9939-07-08861-2
E. Crane, A bound for Smale's mean value conjecture for complex polynomials, Bull. London Math. Soc. 39 (2007), 781–791. https://doi.org/10.1112/blms/bdm063
V. Dubinin, T. Sugawa, Dual mean value problem for complex polynomials, Proc. Japan Acad. Ser. A 85 (2009), 135–137. https://arxiv.org/abs/0906.4605
T.-W. Ng, Y. Zhang, Smale's mean value conjecture for finite Blaschke products, J. Anal. 24 (2016), 331–345. https://arxiv.org/abs/1609.00170
Wikipedia, Mean value problem. https://en.wikipedia.org/w/index.php?title=Mean_value_problem&oldid=1374678764

10 thms2 active usersReviewed

Control Theory Partial Differential Equations·Captain: mikedeng1

Stability and Instability Results of the Wave Equation with a Delay Term in the Boundary or Internal Feedbacks IV: Arbitrarily Small Destabilizing Delays for Internal DampingResearch Paper

Motivation

Feedback laws in engineering are applied with a lag: sensors, actuators and communication channels introduce a time delay $\tau$ between the measurement of a state and the control that reacts to it. For finite-dimensional systems small delays are usually harmless. For distributed systems such as the wave equation they need not be: Datko, Lagnese and Polis (SIAM J. Control Optim. 24, 1986) and Datko (SIAM J. Control Optim. 26, 1988) showed, for one-dimensional examples, that an arbitrarily small delay in a stabilizing feedback can destroy stability. The question matters to anyone who designs boundary or internal controllers for vibrating structures and wants to know whether a stabilizing law is robust to delay.

Nicaise and Pignotti (SIAM J. Control Optim. 45 (2006)) study the wave equation on a bounded domain of $\mathbb R^n$ with a damping term that combines an instantaneous and a delayed velocity feedback, with coefficients $\mu_1$ and $\mu_2$ . They show that the system is exponentially stable when $\mu_2 < \mu_1$ (Theorems 1.1 and 1.3), and that when $\mu_2 \ge \mu_1$ stability can fail (Theorems 1.2 and 1.4). This mission is Theorem 1.4, the internal-damping instability result, in the case the paper proves.

1986–1988: Datko, Lagnese and Polis; Datko — destabilization by small delays in one-dimensional boundary-damped wave equations.
2006: Nicaise and Pignotti — the multi-dimensional dichotomy $\mu_2 < \mu_1$ (stability) versus $\mu_2 \ge \mu_1$ (instability for some delays), for boundary and internal feedback.

Setting

Let $n \ge 1$ and let $\Omega \subset \mathbb R^n$ be a bounded open set with boundary $\Gamma$ of class $C^2$ , split as $\Gamma = \Gamma_D \cup \Gamma_N$ with $\overline{\Gamma_D} \cap \overline{\Gamma_N} = \emptyset$ and $\Gamma_D \neq \emptyset$ . Write $\nu$ for the outer unit normal and $\partial u/\partial\nu$ for the normal derivative. Let $\mu_1 > 0$ , $\mu_2 > 0$ and let $\tau > 0$ be the delay. With damping coefficient $a \equiv 1$ the problem is

u_{tt}(x,t) - \Delta u(x,t) + \mu_1 u_t(x,t) + \mu_2 u_t(x,t-\tau) = 0 \quad \text{in } \Omega \times (0,\infty),

u = 0 \ \text{ on } \Gamma_D \times (0,\infty), \qquad \frac{\partial u}{\partial\nu} = 0 \ \text{ on } \Gamma_N \times (0,\infty),

with initial data $u(\cdot,0) = u_0$ , $u_t(\cdot,0) = u_1$ and a history $u_t = g_0$ on $\Omega \times (-\tau, 0)$ . The standard energy of a solution is

\mathcal E(t) = \frac12 \int_\Omega \big\{ |u_t(x,t)|^2 + |\nabla u(x,t)|^2 \big\}\,dx .

The condition $\mu_2 < \mu_1$ is the paper's assumption (1.8). The paper's problem (1.12)–(1.16) carries a general coefficient $a \in L^\infty(\Omega)$ with $a \ge 0$ and $a > a_0 > 0$ near $\Gamma_N$ ; $a \equiv 1$ is one such coefficient.

Formalization targets

Goal: Theorem 1.4 for $a \equiv 1$

If (1.8) fails, i.e. $0 < \mu_1 \le \mu_2$ , then

\forall \varepsilon > 0\ \exists \tau \in (0,\varepsilon)\ \exists u \text{ solving the problem with delay } \tau:\ \ \mathcal E(t) \not\to 0 \ (t \to \infty),

and the same holds with " $\tau \in (0,\varepsilon)$ " replaced by " $\tau > M$ ", for every $M$ . The goal asserts only non-decay, not a rate of growth or the value of the energy, so it survives any sharpening of the examples.

Milestones

(5.21)–(5.23): if $\varphi$ is an eigenfunction of the mixed Dirichlet–Neumann Laplacian, $\Delta\varphi = -\Lambda^2\varphi$ , and $\lambda \in \mathbb C$ solves $\lambda^2 + (\mu_1 + \mu_2 e^{-\lambda\tau})\lambda = -\Lambda^2$ , then $e^{\lambda t}\varphi(x)$ is a solution.
(5.24)–(5.25): with $\lambda = \alpha + i\beta$ and $\beta\tau = (2l+1)\pi$ , that equation is equivalent to $\alpha^2 + \beta^2 = \Lambda^2$ , $\mu_2 e^{-\alpha\tau} = 2\alpha + \mu_1$ .
Case (a), $\mu_1 = \mu_2$ : the system forces $\alpha = 0$ and $\beta^2 = \Lambda^2$ .
Case (b), $\mu_2 > \mu_1$ , (5.26)–(5.27): for every $\Lambda > 0$ and $l$ there is $\alpha \in (0, (\mu_2-\mu_1)/2)$ with $\tau(\alpha) = \alpha^{-1}\ln(\mu_2/(\mu_1+2\alpha)) > 0$ solving the system.
Energy of separated solutions (p. 1584): $\mathcal E(t) = e^{2\,\mathrm{Re}(\lambda)t}\,\mathcal E(0)$ with $\mathcal E(0) > 0$ .
Delay bounds (p. 1585, corrected): $(2l+1)\pi/\Lambda < \tau < (2l+1)\pi/\sqrt{\Lambda^2 - (\mu_2-\mu_1)^2/4}$ , the second when $\Lambda^2 > (\mu_2-\mu_1)^2/4$ .

Significance

The result shows that the stability threshold $\mu_2 < \mu_1$ of Theorem 1.3 is sharp in the sense that matters for design: at or beyond the threshold there is no delay margin, since delays as small as desired already produce solutions whose energy does not decay. Together with Theorem 1.3 it gives a complete dichotomy in the coefficients $(\mu_1,\mu_2)$ for the internally damped wave equation with delay, in any dimension, and it identifies the mechanism (roots of the characteristic equation on or to the right of the imaginary axis) that later work on delayed stabilization has had to avoid.

The result is proved in the paper; to the best of current knowledge it has not been machine-checked. The mission's product is a formal proof of the $a \equiv 1$ case together with its algebraic core: the reduction of the transcendental characteristic equation, the analysis of both cases, and the two-sided bounds on the delays. The spectral input it needs, an unbounded sequence of eigenvalues of the mixed Dirichlet–Neumann Laplacian with regular eigenfunctions, is reusable well beyond this paper.

Difficulty

The scalar part is elementary. The difficulty is the spectral input. The small delays come from $\tau_{n,l} \approx (2l+1)\pi/\Lambda_n$ with $\Lambda_n \to \infty$ , so the proof needs infinitely many eigenvalues $\Lambda_n^2 \to \infty$ of the Laplacian with mixed Dirichlet–Neumann conditions on a $C^2$ domain, with eigenfunctions that are $C^2$ inside and $C^1$ up to the boundary. This requires compactness of the embedding $H^1_{\Gamma_D}(\Omega) \hookrightarrow L^2(\Omega)$ , the spectral theorem for compact self-adjoint operators, and elliptic regularity for a mixed problem, none of which is available in Mathlib for domains in $\mathbb R^n$ . A single eigenpair gives only the large delays (letting $l \to \infty$ ); it does not give the small ones.

A second point: the paper's own bound $(2l+1)^2\pi^2/\tau_{n,l}^2 \le \Lambda_n^2$ bounds $\tau_{n,l}$ only from below, so it does not by itself give $\tau_{n,l} \to 0$ ; the upper bound of milestone 6 is needed.

Formalization scope

Space: $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with $n \ge 1$ . The $C^2$ boundary is given by a global $C^2$ defining function $\psi$ ( $\Omega = \{\psi < 0\}$ , $\partial\Omega = \{\psi = 0\}$ , $\nabla\psi \ne 0$ on $\partial\Omega$ ); $\nu = \nabla\psi/|\nabla\psi|$ ; the surface measure is pinned by the Gauss–Green formula for all $C^1$ fields.
Solutions are complex valued functions $u(x,t)$ defined for all $t \in \mathbb R$ , $C^2$ on $\Omega \times \mathbb R$ and $C^1$ on $\overline\Omega \times \mathbb R$ ; the equation and boundary conditions hold for $t > 0$ ; initial data and history are the traces of $u$ . The Neumann condition uses the derivative within $\overline\Omega$ . $|\nabla u|^2$ is the sum of the squared moduli of the partial derivatives.
Corrected scope: Theorem 1.4 is printed for a general $a$ satisfying (1.17)–(1.18); §5.2 proves it only for $a \equiv 1$ , which is what is stated.
Corrected slips: (5.22) prints $\Delta\varphi = -\mu^2\varphi$ for $-\Lambda^2\varphi$ ; p. 1584 prints $e^{\alpha+i\beta}\varphi(x)$ for $e^{(\alpha+i\beta)t}\varphi(x)$ ; the p. 1585 bound is supplemented by the upper bound of milestone 6. Milestone texts are quoted verbatim, including the slips.
The standing hypotheses (1.6)–(1.7) and the constant $\xi$ of (1.10) are not used by §5.2 and are omitted, which strengthens the statements.
A trivializing formalization is ruled out: the goal's conclusion $\mathcal E \not\to 0$ excludes $u \equiv 0$ , the energy integrand is continuous on the compact $\overline\Omega$ so the integral is genuine, and the normal derivative is taken within $\overline\Omega$ so the Neumann condition is not satisfied by a junk value.
No statement assumes the existence of eigenvalues; supplying the spectral theory of the mixed Laplacian is part of the goal. Contributions welcome: the spectral theorem for the mixed Dirichlet–Neumann Laplacian on a bounded $C^2$ domain, boundary regularity of its eigenfunctions, and the energy identity for separated solutions.

Selected references

S. Nicaise, C. Pignotti, Stability and instability results of the wave equation with a delay term in the boundary or internal feedbacks, SIAM J. Control Optim. 45(5):1561–1585, 2006. https://doi.org/10.1137/060648891
R. Datko, Not all feedback stabilized hyperbolic systems are robust with respect to small time delays in their feedbacks, SIAM J. Control Optim. 26:697–713, 1988.
R. Datko, J. Lagnese, M. P. Polis, An example on the effect of time delays in boundary feedback stabilization of wave equations, SIAM J. Control Optim. 24:152–156, 1986.
P. Grisvard, Elliptic Problems in Nonsmooth Domains, Pitman, 1985 (regularity of mixed boundary value problems).

10 thms2 active usersReviewed

Control Theory Partial Differential Equations·Captain: mikedeng1

Stability and Instability Results of the Wave Equation with a Delay Term in the Boundary or Internal Feedbacks III: Destabilizing Delays for Boundary FeedbackResearch Paper

Motivation

Boundary feedback stabilization of the wave equation asks whether a damping term placed on part of the boundary drives the energy of every solution to zero. Without delay the answer is classical: the feedback $\partial u/\partial\nu = -\mu_1 u_t$ on a part $\Gamma_N$ of the boundary gives exponential energy decay under geometric conditions (Chen, Lagnese, Lasiecka–Triggiani, Komornik–Zuazua). In practice a feedback is applied with a lag, and a small lag can destroy stability. Datko, Lagnese and Polis (doi:10.1137/0324007) and Datko (doi:10.1137/0326040) showed, in one space dimension, that a purely delayed boundary feedback destabilizes the system for arbitrarily small delays.

Nicaise and Pignotti (doi:10.1137/060648891) study a feedback made of an instantaneous part and a delayed part, with weights $\mu_1$ and $\mu_2$ , in any space dimension. Their Theorem 1.1 gives exponential decay when $\mu_2 < \mu_1$ . This mission formalizes the converse, Theorem 1.2: when $\mu_2 \ge \mu_1$ , some delays admit solutions whose energy does not decay at all.

Timeline.

1986: Datko, Lagnese and Polis, a one-dimensional wave equation whose delayed boundary feedback is unstable.
1988: Datko, instability under arbitrarily small delays for a class of hyperbolic systems.
2006: Xu, Yung and Li (doi:10.1051/cocv:2006021), one space dimension, by spectral analysis: stability for $\mu_2 < \mu_1$ , instability for $\mu_2 > \mu_1$ , possible instabilities for $\mu_1 = \mu_2$ .
2006: Nicaise and Pignotti, the same dichotomy in any dimension $n$ , with explicit destabilizing delays built from eigenfunctions (§5.1).

Setting

Let $n \ge 1$ and let $\Omega \subset \mathbb R^n$ be a bounded open set with boundary $\Gamma$ of class $C^2$ . The boundary is split as $\Gamma = \Gamma_D \cup \Gamma_N$ , with $\overline{\Gamma_D} \cap \overline{\Gamma_N} = \emptyset$ and $\Gamma_D \neq \emptyset$ . Write $\nu$ for the outer unit normal and $d\Gamma$ for the surface measure. Together these data form a mixed domain (MixedDomain n in Lean).

Fix $\mu_1, \mu_2 > 0$ and a delay $\tau > 0$ . The problem (1.1)–(1.3) is

\begin{cases} u_{tt}(x,t) - \Delta u(x,t) = 0 & \text{in } \Omega \times (0,+\infty),\\ u(x,t) = 0 & \text{on } \Gamma_D \times (0,+\infty),\\ \dfrac{\partial u}{\partial\nu}(x,t) = -\mu_1 u_t(x,t) - \mu_2 u_t(x,t-\tau) & \text{on } \Gamma_N \times (0,+\infty), \end{cases}

with initial data $u(\cdot,0)$ , $u_t(\cdot,0)$ and a history $u_t$ on $\Gamma_N \times (-\tau,0)$ (1.4)–(1.5). The standard energy of a solution is (3.7)

\mathcal E(t) = \frac12\int_\Omega \big(|u_t(x,t)|^2 + |\nabla u(x,t)|^2\big)\,dx .

Condition (1.8) of the paper is $\mu_2 < \mu_1$ . This mission concerns the complementary case $\mu_2 \ge \mu_1$ .

For real functions $w$ on $\Omega$ , (5.11) defines $q_0(w) = \int_{\Gamma_N} |w|^2\,d\Gamma$ and $q_1(w) = \int_\Omega |\nabla w|^2\,dx$ .

Formalization targets

Goal: Theorem 1.2 (p. 1563)

If $\mu_2 \ge \mu_1$ , there exist delays $0 < \tau_0 < \tau_1 < \cdots$ and, for each $k$ , a classical solution $u_k$ of (1.1)–(1.3) with delay $\tau_k$ and a constant $c_k > 0$ such that

\mathcal E_k(t) = c_k \qquad \text{for all } t \ge 0 .

The statement fixes no formula for the delays and no value of the energy. It asserts only the existence of infinitely many delays for which the energy does not decay.

Milestones

(5.1)–(5.2), pp. 1579–1580. If $\lambda \in \mathbb C$ and $\varphi$ solves $-\Delta\varphi + \lambda^2\varphi = 0$ in $\Omega$ , $\varphi = 0$ on $\Gamma_D$ and $\partial\varphi/\partial\nu = -(\mu_1 + \mu_2 e^{-\lambda\tau})\lambda\varphi$ on $\Gamma_N$ , then $u = e^{\lambda t}\varphi$ solves (1.1)–(1.3).
(5.5)–(5.7), pp. 1580 and 1582. For $b > 0$ , $l \in \mathbb N$ and $b\tau = \arccos(-\mu_1/\mu_2) + 2l\pi$ :

\cos(b\tau) = -\mu_1/\mu_2,\qquad \mu_2\sin(b\tau) = \sqrt{\mu_2^2-\mu_1^2},\qquad (\mu_1 + \mu_2e^{-ib\tau})\,ib = b\sqrt{\mu_2^2-\mu_1^2}.

Case (a), $\mu_1 = \mu_2$ , p. 1581. For a normalized mixed Dirichlet–Neumann eigenfunction $\varphi$ with $-\Delta\varphi = b^2\varphi$ and $\tau = (2l+1)\pi/b$ , the function $u = e^{ibt}\varphi$ is a solution and

\int_\Omega(|\nabla u|^2 + |u_t|^2)\,dx = 2b^2 \quad (t \ge 0).

Case (b), $\mu_2 > \mu_1$ , pp. 1581–1582. A normalized minimizer $\varphi$ of $s\,q_0(w) + \sqrt{s^2q_0(w)^2 + 4q_1(w)}$ , where $s = \sqrt{\mu_2^2-\mu_1^2}$ , solves the variational problem (5.7) with $2b$ equal to the minimum value.

Significance

The result. Theorem 1.2 shows that the threshold $\mu_2 < \mu_1$ of Theorem 1.1 is sharp in the following sense: once the delayed weight reaches the instantaneous one, no geometric assumption restores asymptotic stability for every delay. Together, Theorems 1.1 and 1.2 separate robust from non-robust boundary feedbacks by a single inequality between the two gains. The explicit delays of case (a), $\tau_{n,l} = (2l+1)\pi/b_n$ , become arbitrarily small or large. So even an arbitrarily short lag in an equally weighted feedback can remove decay.

The formalization. The paper proves the result. It has not been formalized, and Mathlib has no wave equation on domains, no mixed eigenvalue problems and no Sobolev spaces on domains. This mission produces:

a machine-checked statement of the instability half of the paper's dichotomy;
the reduction to a spectral problem as separate, checkable steps;
a precise record of what the paper leaves implicit. In case (b) the existence of the minimizer is assumed ("if the minimum … is attained"), and in case (a) the existence of Dirichlet–Neumann eigenfunctions is quoted.

Difficulty

Milestones 1 and 2 are calculus and trigonometry. The difficulty sits in producing $\varphi$ . The goal needs a nonzero function $\varphi$ that is $C^2$ in $\Omega$ and $C^1$ up to the boundary and solves an eigenvalue problem with mixed Dirichlet and Neumann (case (a)) or Dirichlet and Robin-type (case (b)) boundary conditions. Existence requires compactness of $H^1_{\Gamma_D}(\Omega) \hookrightarrow L^2(\Omega)$ and of the trace into $L^2(\Gamma_N)$ , followed by elliptic regularity up to a $C^2$ boundary. None of these is in Mathlib.

A shortcut does not work: in case (b) the frequency $b$ enters the boundary condition, so $\varphi$ is not an eigenfunction of a fixed self-adjoint operator. The page instead minimizes a non-quadratic functional, and its first-variation computation (5.18)–(5.19) needs care: the functional is not 2-homogeneous, so the normalization by $1 + \varepsilon^2\|v\|^2$ does not literally give $g(\varepsilon) \ge g(0)$ , although the first-order condition is right.

Taking real parts does not give a real-valued solution with constant energy: in case (b) the energy of $\cos(bt)\varphi$ oscillates.

Formalization scope

Solutions are complex-valued, $u : \mathbb R^n \times \mathbb R \to \mathbb C$ , as the page's $e^{\lambda t}\varphi$ with $\lambda \in \mathbb C$ are. $|u_t|^2$ and $|\nabla u|^2 = \sum_i |\partial_i u|^2$ are squared moduli.
Classical solutions. A solution is $C^2$ on $\Omega \times \mathbb R$ and $C^1$ on $\overline\Omega \times \mathbb R$ . It solves the equations for $t > 0$ , and its values at $t \le 0$ are the initial data and history. The normal derivative is the derivative within $\overline\Omega$ applied to $\nu$ . $C^2$ regularity up to the boundary is not required, because eigenfunctions of mixed problems generally lack it.
The domain. The $C^2$ boundary is given by a global defining function $\psi$ with $\Omega = \{\psi < 0\}$ . The surface measure is pinned down by the Gauss–Green formula for all $C^1$ vector fields, which determines it uniquely.
Dropped hypotheses. The geometric hypotheses (1.6)–(1.7) and the parameter $\xi$ of (1.10) are not used in §5.1 and are omitted. This strengthens the statements.
Sobolev spaces. $H^1_{\Gamma_D}(\Omega)$ is replaced in milestone 4 by the class of real functions that are $C^2$ in $\Omega$ , $C^1$ on $\overline\Omega$ and zero on $\Gamma_D$ , both as the minimization class and as the test class.
Non-triviality. The goal requires the constant energy to be positive and the delays to be strictly increasing. Without positivity, the zero solution would satisfy "constant energy". Without strict monotonicity, one delay repeated would count as a sequence.

A complete development needs the following:

Green's first identity on $C^2$ domains for functions that are $C^1$ up to the boundary;
existence and regularity of eigenfunctions of the Laplacian with mixed boundary conditions;
in case (b), existence of the minimizer (Rellich compactness and the trace theorem).

These pieces are reusable well beyond this mission. Contributions of any of them, or of an alternative route to a $\varphi$ with the required properties, are welcome.

Selected references

S. Nicaise, C. Pignotti, Stability and instability results of the wave equation with a delay term in the boundary or internal feedbacks, SIAM J. Control Optim. 45(5):1561–1585, 2006. https://doi.org/10.1137/060648891
R. Datko, J. Lagnese, M. P. Polis, An example on the effect of time delays in boundary feedback stabilization of wave equations, SIAM J. Control Optim. 24:152–156, 1986. https://doi.org/10.1137/0324007
R. Datko, Not all feedback stabilized hyperbolic systems are robust with respect to small time delays in their feedbacks, SIAM J. Control Optim. 26:697–713, 1988. https://doi.org/10.1137/0326040
G. Q. Xu, S. P. Yung, L. K. Li, Stabilization of wave systems with input delay in the boundary control, ESAIM Control Optim. Calc. Var. 12:770–785, 2006. https://doi.org/10.1051/cocv:2006021

7 thms2 active usersReviewed

Functional Analysis Mathematical Physics Partial Differential Equations·Captain: mikedeng1

Mathematical Methods in Quantum Mechanics XII: Self-Adjointness and Essential Spectrum of One-Particle Schrödinger OperatorsTextbook

Motivation

The Hamiltonian of a single nonrelativistic particle in $\mathbb R^n$ moving in a potential $V$ is the Schrödinger operator $H = -\Delta + V$ acting in $L^2(\mathbb R^n)$ . Before anything can be said about the dynamics or the energy levels of such a particle, one must know that $H$ is a genuine observable: a self-adjoint operator on a specified domain. For potentials that decay at infinity one also wants the coarse structure of the spectrum, namely that it is bounded below and that everything below the continuum threshold $0$ consists of isolated eigenvalues of finite multiplicity. The hydrogen atom, with the Coulomb potential $-\gamma/|x|$ in three dimensions, is the central example.

The self-adjointness results go back to T. Kato's 1951 paper on the Hamiltonians of atoms; the identification of the essential spectrum through relatively compact perturbations is due to H. Weyl's theorem and its later extensions. This mission follows Chapter 10 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), Sections 10.1, 10.2, 10.4 and 10.5.

Setting

$L^2(\mathbb R^n)$ is the complex Hilbert space of square integrable functions with respect to Lebesgue measure. The free Schrödinger operator is $H_0 = -\Delta$ with domain the Sobolev space $H^2(\mathbb R^n) = \{ f \in L^2 \mid |p|^2 \hat f(p) \in L^2 \}$ ; equivalently, $H_0$ is the inverse Fourier transform of the maximally defined multiplication by $p^2$ . Units are $\hbar = 1$ and mass $m = 1/2$ .

A real function $V$ acts by the multiplication operator $(Vf)(x) = V(x) f(x)$ on its maximal domain $\{f \in L^2 \mid Vf \in L^2\}$ . The sum $H_0 + V$ is defined on $\mathfrak D(H_0) \cap \mathfrak D(V)$ . $L^\infty_\infty(\mathbb R^n)$ denotes the bounded Borel functions vanishing at infinity, and $C_c^\infty(\mathbb R^n)$ the smooth compactly supported functions.

For a linear operator $A$ , the resolvent $R_A(z) = (A - z)^{-1}$ exists when $A - z$ maps $\mathfrak D(A)$ bijectively onto $L^2$ with bounded inverse; the resolvent set $\rho(A)$ collects such $z$ and $\sigma(A) = \mathbb C \setminus \rho(A)$ . The point spectrum $\sigma_p(A)$ is the set of eigenvalues; the discrete spectrum $\sigma_d(A)$ consists of the eigenvalues that are isolated in $\sigma(A)$ and have finite-dimensional eigenspace; the essential spectrum is $\sigma_{ess}(A) = \sigma(A) \setminus \sigma_d(A)$ . An operator $K$ is relatively compact with respect to $A$ if $\mathfrak D(A) \subseteq \mathfrak D(K)$ and $K R_A(z)$ is compact for one $z \in \rho(A)$ . $A$ is bounded from below if $\langle \psi, A\psi\rangle \ge \gamma\|\psi\|^2$ on $\mathfrak D(A)$ for some real $\gamma$ , and a subspace is a core of a closed operator if the closure of the restriction to it is the operator itself.

The hydrogen Hamiltonian is $H^{(1)} = -\Delta - \gamma/|x|$ on $L^2(\mathbb R^3)$ . A function in $L^2(\mathbb R^n)$ is positive if it is $\ge 0$ a.e. and not a.e. zero, and strictly positive if it is $> 0$ a.e.; a bounded operator is positivity improving if it maps positive functions to strictly positive ones.

Formalization targets

Goal: self-adjointness and essential spectrum (Theorem 10.2)

Let $n \ge 1$ and $V$ real with $V \in L^\infty_\infty(\mathbb R^n)$ if $n > 3$ and $V \in L^\infty_\infty(\mathbb R^n) + L^2(\mathbb R^n)$ if $n \le 3$ . Then $V$ is relatively compact with respect to $H_0$ , and $H = H_0 + V$ has domain $H^2(\mathbb R^n)$ , is self-adjoint and bounded from below, satisfies

\sigma_{ess}(H) = [0,\infty),

and has $C_c^\infty(\mathbb R^n)$ as a core.

Milestones

Sobolev bound (Lemma 10.1). For $n \le 3$ , every $\psi \in H^2(\mathbb R^n)$ is continuous and vanishes at infinity, and for every $a > 0$ there is $b > 0$ with $\|\psi\|_\infty \le a\|H_0\psi\| + b\|\psi\|$ on $H^2(\mathbb R^n)$ .
Virial theorem (Theorem 10.3). If $V$ is homogeneous of degree $-1$ under dilations, every normalized eigenfunction of $H_0 + V$ with eigenvalue $\lambda$ satisfies $\lambda = -\langle\psi, H_0\psi\rangle = \frac12\langle\psi, V\psi\rangle$ ; in particular $\lambda < 0$ .
Hydrogen spectrum (Corollary 10.4). For $\gamma > 0$ , $\sigma_p(H^{(1)}) = \sigma_d(H^{(1)})$ is a strictly increasing sequence of negative numbers converging to $0$ .
Hydrogen eigenvalues (Theorem 10.9, eigenvalue part). For $\gamma > 0$ the eigenvalues of $H^{(1)}$ are $E_n = -(\gamma/(2(n+1)))^2$ , $n \in \mathbb N_0$ .
Perron–Frobenius for positivity improving operators (Theorem 10.11). If $A$ is bounded, self-adjoint, real and positivity improving and $\|A\|$ is an eigenvalue, it is simple with a strictly positive eigenfunction.
Nondegenerate ground state (Theorem 10.12). If $H_0 + V$ is self-adjoint, bounded below, has $C_c^\infty$ as a core, and $E_0 = \min\sigma(H)$ is an eigenvalue, then $E_0$ is simple with a strictly positive eigenfunction.

Significance

The result. Theorem 10.2 is the existence theorem for one-particle quantum mechanics with decaying potentials. It makes $H_0 + V$ an observable on the natural domain $H^2$ , guarantees a lowest energy, and places the continuum exactly at $[0,\infty)$ , so that all spectral information below zero is carried by bound states. Its three-dimensional case covers the Coulomb potential, and the same scheme (relative boundedness, Kato–Rellich, relative compactness, Weyl) is the template for the $N$ -body HVZ theorem. The virial theorem, the qualitative and the explicit hydrogen spectrum, and the nondegeneracy of ground states are the standard first applications.

Formalizing it. None of these statements is formalized. Mathlib has the $L^2$ Fourier transform, tempered distributions and Sobolev spaces on the distribution side, and LinearPMap with adjoints and closures, but no free Schrödinger operator as an unbounded operator on $L^2$ , no resolvent set or essential spectrum for unbounded operators, and no self-adjointness theorem for $-\Delta + V$ . The mission asks for proofs of Teschl's statements and, with them, a reusable definition of $H_0$ on $H^2(\mathbb R^n)$ and of maximally defined multiplication operators.

Difficulty

The goal combines several chapters of the book. A proof needs self-adjointness of $H_0$ on $H^2$ via the Fourier transform, the Sobolev bound of Lemma 10.1 to get $\mathfrak D(H_0) \subseteq \mathfrak D(V)$ with relative bound zero, the Kato–Rellich theorem, compactness of operators of the form $g(x)f(p)$ (Lemma 7.11) to obtain relative compactness, Weyl's theorem on the invariance of the essential spectrum, $\sigma(H_0) = [0,\infty)$ with no eigenvalues, and the fact that $C_c^\infty$ is a core for $H_0$ . None of these intermediate results is in Mathlib for unbounded operators.

The milestones add their own difficulties: the virial theorem requires the dilation group and a derivative argument on domains; Corollary 10.4 requires a variational argument producing infinitely many negative eigenvalues; Theorem 10.9 requires separation of variables in spherical coordinates and the Laguerre polynomials; and Theorem 10.12 uses the Trotter product formula and strong resolvent convergence to transfer positivity from $e^{-tH_0}$ to $e^{-tH}$ .

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure and $L^2(\mathbb R^n)$ is Mathlib's Lp ℂ 2 volume, a separable complex Hilbert space. Unbounded operators are Mathlib LinearPMaps, sums of unbounded operators are LinearPMap sums on the intersection of domains, self-adjointness is Mathlib's IsSelfAdjoint, and "core" is LinearPMap.HasCore. The resolvent is the bounded two-sided inverse of $A - z$ ; $\rho(A)$ , $\sigma(A)$ , $\sigma_p$ , $\sigma_d$ and $\sigma_{ess}$ are defined from it, and Mathlib's Banach-algebra spectrum is not used. Compactness is IsCompactOperator.

The Fourier transform is Mathlib's unitary $L^2$ transform with kernel $e^{-2\pi i\langle x,\xi\rangle}$ , not Teschl's $(2\pi)^{-n/2}e^{-ipx}$ . $H_0$ is defined as $\mathcal F^{-1}(2\pi|\xi|)^2\mathcal F$ and $H^2$ as $\{f \mid (2\pi|\xi|)^2 \mathcal F f \in L^2\}$ ; both coincide with the book's objects, independently of the normalization. No projection-valued measure or functional calculus is taken as data. $C_\infty(\mathbb R^n)$ is Mathlib's space of continuous functions vanishing at infinity, and positivity of complex values is taken in ComplexOrder.

The virial hypothesis $U(-s)VU(s) = e^{-s}V$ is stated as $V(e^s x) = e^{-s}V(x)$ for almost every $x$ , for every $s$ , which is what the operator identity means for a multiplication operator. Corollary 10.4's index set $\{E_{j-1}\}_{j\in\mathbb N_0}$ is read as the sequence $E_0, E_1, \dots$ . Only the eigenvalue formula of Theorem 10.9 is included, not its explicit eigenbasis.

A trivializing formalization is ruled out: the only hypotheses of the goal are the function-space conditions on $V$ and $n \ge 1$ . Neither $\mathfrak D(H_0) \subseteq \mathfrak D(V)$ , a relative bound below one, nor closedness of $H_0 + V$ is assumed; the equality of the domain with $H^2(\mathbb R^n)$ and the relative compactness of $V$ are conclusions. The essential spectrum requires all three of "eigenvalue", "isolated" and "finite multiplicity" in its complement, so $[0,\infty)$ is a genuine identification.

Selected references

G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, AMS, 2009, Chapter 10. https://doi.org/10.1090/gsm/099
T. Kato, Fundamental properties of Hamiltonian operators of Schrödinger type, Transactions of the AMS 70 (1951), 195–211. https://doi.org/10.1090/S0002-9947-1951-0041010-X
M. Reed and B. Simon, Methods of Modern Mathematical Physics II: Fourier Analysis, Self-Adjointness (Section X.2) and IV: Analysis of Operators (Sections XIII.4, XIII.12), Academic Press, 1975, 1978.
H. L. Cycon, R. G. Froese, W. Kirsch and B. Simon, Schrödinger Operators, Springer, 1987.

20 thms2 active usersReviewed

Completed

Functional Analysis Mathematical Physics·Captain: mikedeng1

Mathematical Methods in Quantum Mechanics IV: The Min-Max Principle and Temple's InequalityTextbook

Motivation

In quantum mechanics the energy levels of a system are the eigenvalues of a self-adjoint Hamiltonian $A$ , and for almost every Hamiltonian of interest (atoms with more than one electron, molecules) they cannot be computed in closed form. What can be computed are expectation values $\langle \psi, A\psi\rangle$ of explicit trial functions $\psi$ . The min-max principle turns such numbers into rigorous statements about the eigenvalues: every trial computation gives an upper bound, and the optimal choices reproduce the eigenvalues exactly. It goes back to Fischer (1905) for quadratic forms in finitely many variables and to Courant (1920) for differential operators; Temple (1928) added the matching lower bound. This mission formalizes the version for unbounded self-adjoint operators with essential spectrum, as stated in Chapter 4 of Teschl's Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), where eigenvalues below the essential spectrum are characterized and estimated.

Setting

Let $\mathfrak H$ be a complex Hilbert space, with inner product $\langle\cdot,\cdot\rangle$ conjugate linear in the first argument. An operator $A$ is a linear map defined on a subspace $\mathfrak D(A) \subseteq \mathfrak H$ , its domain; $A$ is self-adjoint if $\mathfrak D(A)$ is dense and $A$ equals its adjoint. The resolvent set $\rho(A)$ is the set of $z \in \mathbb C$ for which $A - z : \mathfrak D(A) \to \mathfrak H$ is a bijection with bounded inverse, and the spectrum is $\sigma(A) = \mathbb C \setminus \rho(A)$ . For self-adjoint $A$ , $\sigma(A) \subseteq \mathbb R$ .

For $z \in \mathbb C$ the eigenspace is $\operatorname{Ker}(A - z) = \{\psi \in \mathfrak D(A) \mid A\psi = z\psi\}$ ; $z$ is an eigenvalue when it is nonzero, and its dimension is the multiplicity. The discrete spectrum $\sigma_d(A)$ consists of the eigenvalues that are isolated points of $\sigma(A)$ and have finite multiplicity, and the essential spectrum is $\sigma_{ess}(A) = \sigma(A) \setminus \sigma_d(A)$ .

Let $\Sigma = \inf \sigma_{ess}(A) \in [-\infty, +\infty]$ ( $+\infty$ if $\sigma_{ess}(A)$ is empty). The numbers $E_1 \le E_2 \le E_3 \le \cdots$ are the eigenvalues of $A$ below $\Sigma$ , listed in increasing order and repeated according to multiplicity; if there are only $N$ of them, $E_n = \Sigma$ for $n > N$ . For vectors $\psi_1, \dots, \psi_m \in \mathfrak H$ let

U(\psi_1, \dots, \psi_m) = \{\psi \in \mathfrak D(A) \mid \|\psi\| = 1,\ \psi \perp \psi_1, \dots, \psi_m\}.

Some statements involve the spectral projections $P_A(\Omega)$ of $A$ , for Borel sets $\Omega \subseteq \mathbb R$ : the projection-valued measure with $A = \int \lambda\, dP_A(\lambda)$ . With the spectral measures $\mu_\psi(\Omega) = \langle \psi, P_A(\Omega)\psi\rangle$ , the form domain is $\mathfrak Q(A) = \{\psi \mid \int |\lambda|\, d\mu_\psi(\lambda) < \infty\}$ , and on it $\langle \psi, A\psi\rangle$ means $\int \lambda\, d\mu_\psi(\lambda)$ .

Formalization targets

Goal: the min-max principle (Theorem 4.10)

For self-adjoint $A$ and every $n \ge 1$ ,

E_n = \sup_{\psi_1, \dots, \psi_{n-1} \in \mathfrak H} \ \inf_{\psi \in U(\psi_1, \dots, \psi_{n-1})} \langle \psi, A\psi\rangle .

Both sides are extended real numbers; the infimum over an empty set is $+\infty$ .

Milestones

Theorem 2.19 (the case $n = 1$ and its mirror image): $\inf \sigma(A) = \inf_{\psi \in \mathfrak D(A), \|\psi\| = 1} \langle\psi, A\psi\rangle$ and $\sup \sigma(A) = \sup_{\psi \in \mathfrak D(A), \|\psi\| = 1} \langle\psi, A\psi\rangle$ .
Theorem 4.12 (i): if $\psi_1, \dots, \psi_k \in \mathfrak Q(A)$ are linearly independent and $\langle \psi, A\psi\rangle < \lambda\|\psi\|^2$ for every nonzero $\psi \in \operatorname{span}\{\psi_j\}$ , then $\dim \operatorname{Ran} P_A((-\infty,\lambda)) \ge k$ ; with $>$ , $\dim \operatorname{Ran} P_A((\lambda,\infty)) \ge k$ .
Theorem 4.12 (ii): if $\psi_1, \dots, \psi_k \in \mathfrak D(A)$ are linearly independent, $\lambda_1 < \lambda_2$ , and $\|(A - \tfrac{\lambda_2+\lambda_1}{2})\psi\| < \tfrac{\lambda_2-\lambda_1}{2}\|\psi\|$ for every nonzero $\psi$ in their span, then $\dim \operatorname{Ran} P_A((\lambda_1,\lambda_2)) \ge k$ .
Corollary 4.11: if $A, B$ are self-adjoint, $\mathfrak D(A) \subseteq \mathfrak D(B)$ and $\langle \psi, (A - B)\psi\rangle \ge 0$ on $\mathfrak D(A)$ , then $E_n(A) \ge E_n(B)$ for all $n \ge 1$ .
Theorem 4.13 (Temple's inequality): if $\lambda_1 < \lambda_2$ , $\psi \in \mathfrak D(A)$ , $\|\psi\| = 1$ , $\lambda = \langle \psi, A\psi\rangle \in (\lambda_1, \lambda_2)$ and $\sigma(A) \cap (\lambda_1, \lambda_2) = \{E\}$ , then

\lambda - \frac{\|(A-\lambda)\psi\|^2}{\lambda_2 - \lambda} \le E \le \lambda + \frac{\|(A-\lambda)\psi\|^2}{\lambda - \lambda_1}.

Significance

The min-max principle is the standard tool for comparing eigenvalues of different operators: Corollary 4.11 (monotonicity under operator inequalities) follows from it, and with it the stability of eigenvalues under perturbations, Dirichlet–Neumann bracketing and the Rayleigh–Ritz method used in computational quantum chemistry. Theorem 4.12 converts a finite-dimensional computation into a lower bound for the number of eigenvalues in an interval, and Temple's inequality supplies lower bounds on an eigenvalue to complement the variational upper bounds, which is what makes numerical eigenvalue enclosures rigorous.

All of these results are classical and proved in the literature. What is not available is a machine-checked version for unbounded operators: Mathlib has the Courant–Fischer characterization only for finite-dimensional or compact self-adjoint operators, and existing formal developments of Temple's inequality and min-max levels treat bounded operators. This mission formalizes the unbounded case, with the essential spectrum and the counting of eigenvalues by multiplicity made explicit, and with the edge cases (operators unbounded below, empty essential spectrum) covered by extended-real values.

Difficulty

The central difficulty is that $E_n$ is defined by spectral data (which points of the spectrum are isolated eigenvalues of finite multiplicity, and how many there are below a given level), while the right-hand side is defined by expectation values on the domain. Relating the two needs the spectral theorem for unbounded operators: for every level below $\Sigma$ the spectral subspace must be shown to be finite dimensional and spanned by eigenvectors, and for the level $\Sigma$ itself one needs infinite-dimensional spectral subspaces in every neighbourhood, which is where the essential spectrum enters. When $E_n = \Sigma$ the supremum and infimum need not be attained, so the finite-dimensional argument with eigenvectors does not transfer. For Corollary 4.11 and Temple's inequality the hypotheses concern only the operator and one vector, while the conclusions concern the spectrum.

Formalization scope

The formalization uses Lean 4 with Mathlib. Operators are partially defined linear maps (LinearPMap, H →ₗ.[ℂ] H) on a complex Hilbert space; self-adjointness is Mathlib's IsSelfAdjoint, which includes a dense domain. The Hilbert space is not assumed separable. The spectrum is the resolvent spectrum defined above, not Mathlib's Banach-algebra spectrum, and for self-adjoint operators it enters through its real points. Eigenspace dimensions are cardinals (Module.rank). $E_n$ is defined from the spectrum, the essential spectrum and these dimensions, as an element of EReal, indexed from $n = 1$ ; if $A$ is unbounded below its value is $-\infty$ , and if the essential spectrum is empty and the eigenvalues run out it is $+\infty$ . The min-max identity is stated in EReal, with $\langle\psi, A\psi\rangle$ entering through its real part.

A formalization that defines $E_n$ as the min-max expression itself would make the goal true by definition. This is ruled out: $E_n$ is defined only from the spectrum, the essential spectrum and the dimensions of eigenspaces.

The spectral theorem is not part of this mission. Theorem 4.12 takes a projection-valued measure $P$ on the Borel sets of $\mathbb R$ as data, together with the hypothesis that $A = \int \lambda\, dP(\lambda)$ (domain $\{\psi \mid \int \lambda^2 d\mu_\psi < \infty\}$ and $\langle\psi, A\psi\rangle = \int \lambda\, d\mu_\psi$ ), which is the form the spectral theorem guarantees; $P_A$ is then $P$ , and $\mathfrak Q(A)$ and the quadratic form are defined from it. Nothing else the book derives is taken as a hypothesis. The goal, Theorem 2.19, Corollary 4.11 and Temple's inequality use no projection-valued measure. Corollary 4.11 states the domain inclusion $\mathfrak D(A) \subseteq \mathfrak D(B)$ explicitly, as the meaning of $A - B \ge 0$ .

A complete development needs the spectral theorem for unbounded self-adjoint operators (or an equivalent functional calculus), the identification of $\sigma_{ess}$ with the points where spectral projections have infinite rank, and the orthogonality of eigenspaces. These are reusable across the rest of the book. Proofs of any milestone, and of lemmas connecting the resolvent spectrum with spectral projections, are welcome.

Selected references

G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, American Mathematical Society, 2009. doi:10.1090/gsm/099. Theorem 2.19 (p. 77), Section 4.3–4.4 (pp. 117–120), essential spectrum (p. 145).
E. Fischer, Über quadratische Formen mit reellen Koeffizienten, Monatshefte für Mathematik und Physik 16 (1905), 234–249. doi:10.1007/BF01693781.
R. Courant, Über die Eigenwerte bei den Differentialgleichungen der mathematischen Physik, Mathematische Zeitschrift 7 (1920), 1–57. doi:10.1007/BF01199396.
G. Temple, The theory of Rayleigh's principle as applied to continuous systems, Proceedings of the Royal Society of London A 119 (1928), 276–293. doi:10.1098/rspa.1928.0098.

15 thms2 active usersReviewed

Completed

Functional Analysis Mathematical Physics·Captain: mikedeng1

Mathematical Methods in Quantum Mechanics XI: Weyl's Limit Circle / Limit Point AlternativeTextbook

Why the endpoint behaviour of Sturm–Liouville operators matters

A quantum particle on a line or half-line, and the radial part of a particle in a spherically symmetric potential, are described by a Sturm–Liouville expression

\tau f = \frac{1}{r}\big(-(pf')' + qf\big)

on an interval $I = (a, b)$ . The expression alone does not define a Hamiltonian: a self-adjoint operator needs a domain, and on a general interval the choice of domain is a choice of boundary conditions at $a$ and $b$ . Whether a boundary condition is needed at all depends on the behaviour of $\tau$ near the endpoint. H. Weyl settled this in 1910 (Math. Ann. 68, 220–269) with his limit circle / limit point dichotomy: at each endpoint either all solutions of $\tau u = z u$ are square integrable near it and a boundary condition must be imposed, or they are not and no condition is possible. This mission formalizes Sections 9.1–9.2 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), which develop the theory for coefficients that are only locally integrable, and culminate in Theorem 9.9, the Weyl alternative.

Setting

Let $-\infty \le a < b \le \infty$ and $I = (a,b)$ . The coefficients satisfy: $p^{-1} \in L^1_{loc}(I)$ with $p > 0$ ; $q \in L^1_{loc}(I)$ real-valued; $r \in L^1_{loc}(I)$ with $r > 0$ . The Hilbert space is $L^2(I, r\,dx)$ with $\langle f, g\rangle = \int_a^b f^* g\, r\,dx$ .

A function $f$ is locally absolutely continuous, $f \in AC_{loc}(I)$ , if it is an indefinite integral of a locally integrable function on $I$ . The equation $\tau f = g$ means that $f$ and its quasi-derivative $pf'$ both lie in $AC_{loc}(I)$ and $-(pf')' + qf = rg$ almost everywhere. A solution of $(\tau - z)u = 0$ , $z \in \mathbb{C}$ , is a complex-valued $u$ with $\tau u = z u$ in this sense. The maximal domain is

\mathfrak{D}(\tau) = \{ f \in L^2(I, r\,dx) \mid f, pf' \in AC_{loc}(I),\ \tau f \in L^2(I, r\,dx) \}.

The modified Wronskian is $W_x(f_1, f_2) = f_1(x)(pf_2')(x) - (pf_1')(x) f_2(x)$ , with no complex conjugation, and $W_a(f_1, f_2) = \lim_{x \to a} W_x(f_1, f_2)$ , $W_b$ likewise.

$\tau$ is limit circle (l.c.) at $a$ if there is a $v \in \mathfrak{D}(\tau)$ with $W_a(v^*, v) = 0$ and $W_a(v, f) \ne 0$ for some $f \in \mathfrak{D}(\tau)$ ; otherwise it is limit point (l.p.) at $a$ . The same holds at $b$ . A function $u$ is square integrable near $a$ if $\int_a^c |u|^2 r\,dx < \infty$ for some $c \in I$ .

Formalization targets

Goal: the Weyl alternative (Theorem 9.9)

For every Sturm–Liouville expression as above,

\tau \text{ is l.c. at } a \iff \text{for one } z_0 \in \mathbb{C}, \text{ all solutions of } (\tau - z_0)u = 0 \text{ are square integrable near } a,

and if $\tau$ is l.c. at $a$ , then for every $z \in \mathbb{C}$ all solutions of $(\tau - z)u = 0$ are square integrable near $a$ . The same two statements hold at $b$ .

Milestones

Theorem 9.1. For $rg \in L^1_{loc}(I)$ , $c \in I$ , $\alpha, \beta \in \mathbb{C}$ , the problem $(\tau - z) f = g$ , $f(c) = \alpha$ , $(pf')(c) = \beta$ has a unique solution, entire in $z$ .
Lemma 9.2. If $u_1, u_2$ solve $(\tau - z)u = 0$ with $W(u_1, u_2) = 1$ , every solution of $(\tau - z)f = g$ is given by the variation-of-constants formula (9.10).
Eq. (9.7). For $f, g \in \mathfrak{D}(\tau)$ the limits $W_a(g^*, f)$ , $W_b(g^*, f)$ exist and $\langle g, \tau f\rangle = W_a(g^*, f) - W_b(g^*, f) + \langle \tau g, f\rangle$ (the printed $W_b - W_a$ has the wrong sign for the Wronskian (9.5)).
Lemma 9.5. If $v \in \mathfrak{D}(\tau)$ , $W_a(v^*, v) = 0$ and $W_a(v^*, \hat f) \ne 0$ for some $\hat f \in \mathfrak{D}(\tau)$ , then $W_a(v, f) = 0 \Leftrightarrow W_a(v, f^*) = 0$ , and $W_a(v, f) = W_a(v, g) = 0 \Rightarrow W_a(g^*, f) = 0$ .
Theorem 9.6. The operator $Af = \tau f$ on $\mathfrak{D}(A) = \{ f \in \mathfrak{D}(\tau) \mid W_a(v, f) = 0 \text{ if l.c. at } a,\ W_b(w, f) = 0 \text{ if l.c. at } b\}$ is self-adjoint, and the set $\mathfrak{D}_1$ of (9.21) is a core.
Lemma 9.7. For $z \in \rho(A)$ there are solutions $u_a$ , $u_b$ of $(\tau - z)u = 0$ , square integrable near $a$ resp. $b$ and satisfying the boundary condition there, and $(A - z)^{-1}$ is the integral operator with the Green function (9.28).

Significance

The Weyl alternative turns a question about operators into a question about an ordinary differential equation. Whether a Schrödinger operator $-d^2/dx^2 + q$ on a half-line needs a boundary condition at infinity, or whether $-\Delta + V$ with a radial potential is essentially self-adjoint on smooth functions, reduces to checking square integrability of solutions for a single value of $z$ . Combined with Theorem 9.6 it classifies the self-adjoint realizations with separated boundary conditions: none at an l.p. endpoint, a one-parameter family at an l.c. endpoint. The Green function of Lemma 9.7 is the starting point of the spectral theory of one-dimensional Schrödinger operators: Weyl–Titchmarsh $m$ -functions, spectral transformations, and oscillation theory in the rest of Teschl's Chapter 9.

The results are classical and proved in many textbooks. The formal content is new: Mathlib has unbounded operators (LinearPMap) and their adjoints, but no Sturm–Liouville theory, no quasi-derivatives, no ODE existence theorem for measurable, locally integrable coefficients (its Picard–Lindelöf theorem needs Lipschitz right-hand sides), and no self-adjoint realizations of differential operators on general intervals.

Difficulty

The definition of limit circle refers only to $\mathfrak{D}(\tau)$ and boundary limits of Wronskians, while the conclusion is about all solutions of an ODE for all $z \in \mathbb{C}$ . The two sides are linked only through self-adjoint operators: the passage from boundary Wronskians to square integrable solutions goes through the resolvent of a self-adjoint realization, which exists only for $z \in \rho(A)$ , and so only for nonreal $z$ in general. Extending the conclusion to real $z$ , where no resolvent is available, needs an argument of a different kind. On the ODE side, the coefficients are only locally integrable, so solutions are merely locally absolutely continuous, equations hold only almost everywhere, and every boundary quantity is a limit whose existence must itself be established.

Formalization scope

Interval and coefficients. The structure SLData bundles $a, b \in$ EReal with $a < b$ (infinite endpoints allowed), $p, q, r : \mathbb{R} \to \mathbb{R}$ , and the standing hypotheses (i)–(iii) of p. 181; $p, r > 0$ pointwise on $I$ . $L^2(I, r\,dx)$ is Lp ℂ 2 for the measure $r\,dx$ on $I$ .
Regularity. $AC_{loc}(I)$ is encoded by its integral characterization. The quasi-derivative $pf'$ is the continuous function $f^{[1]} \in AC_{loc}(I)$ with $f(y) - f(x) = \int_x^y f^{[1]}/p$ , chosen by Classical.choose (it is unique on $I$ ). $\tau f = g$ is $(pf')(y) - (pf')(x) = \int_x^y (qf - rg)$ with a local integrability clause. No smoothness of the coefficients and no $C^2$ solutions are assumed.
Boundary Wronskians $W_a$ , $W_b$ are Filter.limUnder along $x \to a$ , $x \to b$ inside $I$ . They are used only on $\mathfrak{D}(\tau)$ , where milestone (9.7) states that the limits exist. In Lemma 9.7, where $u_a$ need not lie in $\mathfrak{D}(\tau)$ , the boundary condition is stated as a convergence.
Operators. Operators in $L^2(I, r\,dx)$ are LinearPMaps; self-adjointness is Mathlib's IsSelfAdjoint. Theorem 9.6 asserts that an operator with graph $\{(f, \tau f) \mid f \in \mathfrak{D}(A)\}$ exists (i.e. is well defined) and is self-adjoint. $\rho(A)$ and $(A - z)^{-1}$ follow Teschl (2.66): a bounded two-sided inverse of $A - z$ . No projection-valued measure or functional calculus is used.
Corrections to the printed text. Lemma 9.7 says "a solution $u_a$ of $(\tau - z)u = g$ "; the proof and (9.28) need $(\tau - z)u = 0$ , which is what is stated. The condition at an endpoint in (9.21) is imposed only where $\tau$ is l.c., as in (9.20). The second line of (9.10) is stated for quasi-derivatives. The boundary term of (9.7) is printed as $W_b(g^*, f) - W_a(g^*, f)$ ; integration by parts with (9.5) gives $W_a(g^*, f) - W_b(g^*, f)$ (check: $p = r = 1$ , $q = 0$ on $(0,1)$ , $f = x^2$ , $g = 1$ ), and the corrected identity is stated.
Ruling out trivialization. Limit circle is the Wronskian notion of p. 187, never "all solutions are square integrable", which would make the goal circular. The goal has no hypothesis beyond the standing assumptions on $p, q, r$ .

A complete development needs a Carathéodory-type existence theorem for linear first-order systems with $L^1_{loc}$ coefficients, the Lagrange identity with its boundary limits, Lemma 9.3 (a linear-algebra fact about functionals) and the computation of the closure and adjoint of the minimal operator (Lemma 9.4). The ODE layer and the $L^2(I, r\,dx)$ operator layer can be reused for the Weyl–Titchmarsh theory, oscillation theory (Sec. 9.7) and one-particle Schrödinger operators (Ch. 10). Contributions that build them as general lemmas are welcome.

Selected references

G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, AMS Graduate Studies in Mathematics 99, 2009, Sections 9.1–9.2. https://doi.org/10.1090/gsm/099
H. Weyl, "Über gewöhnliche Differentialgleichungen mit Singularitäten und die zugehörigen Entwicklungen willkürlicher Funktionen", Math. Ann. 68 (1910), 220–269. https://doi.org/10.1007/BF01474161
J. Weidmann, Spectral Theory of Ordinary Differential Operators, Lecture Notes in Mathematics 1258, Springer, 1987. https://doi.org/10.1007/BFb0077960
A. Zettl, Sturm–Liouville Theory, Mathematical Surveys and Monographs 121, AMS, 2005. https://doi.org/10.1090/surv/121

20 thms2 active usersReviewed

Analysis

Missions

Distribution Function Inequalities for Martingales 9: EΦ(f*) Is Controlled by the Conditional Square Function and the Largest Jump, for Every Φ of Moderate GrowthResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 21.1

Milestones

Further statements

Significance

Difficulty

Formalization scope

Selected references

Distribution Function Inequalities for Martingales 3: For Brownian Motion Stopped at Any Stopping Time τ, EΦ(X*(τ)) and EΦ(τ^{1/2}) Are ComparableResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Distribution Function Inequalities for Martingales 6: For a Nonnegative Martingale, EΦ(S(f)) ≤ c·EΦ(f*) for Every Φ of Moderate GrowthResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 18.3 (p. 36)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Distribution Function Inequalities for Martingales 5: A Nonnegative Martingale's Square Function, Stopped Before |f_n| Exceeds λ, Is Exponentially Square IntegrableResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Vertical Integration and Antitrust Policy: Integrating Successive Monopolies Lowers the Final Price and Raises Output, Joint Profit and Consumer SurplusResearch Paper

Motivation

Setting

Formalization targets

Goal: vertical integration benefits producer and consumer

Milestones

Significance

Difficulty

Formalization scope

Selected references

Concentration of Measure and Isoperimetric Inequalities in Product Spaces V: The Convex Hull Distance — ∫ exp f_α(A,x) dP ≤ P(A)^{−α}Textbook

Motivation

Setting

Formalization targets

Goal: Theorem 4.2.4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Concentration of Measure and Isoperimetric Inequalities in Product Spaces I: Control by One Point — ∫ e^{t f(A,x)} dP ≤ P(A)^{−α} exp(Nt²(1+1/α)/8) for the Hamming Distance to ATextbook

Motivation

Setting

Formalization targets

Goal: Corollary 2.2.3

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

Concentration of Measure and Isoperimetric Inequalities in Product Spaces III: Penalties — Exponential Moments of the Penalized Distance f_h(A, x)Textbook

Motivation

Setting

Formalization targets

Goal: Theorem 2.4.1

Milestones

Significance

Difficulty

Formalization scope

Milestone: Lemma 4.7 (the normal case $D(x,u)=\mathrm N_{\mathcal M}(x)$ )