Harmonic Analysis

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

1. Doob's weak-type inequality (1.5): $\lambda^pP(f^*>\lambda)\le\|f\|_p^p$ for $1\le p<\infty$.
2. 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).$$

3. 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.

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

1. 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).$$

3. 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).$$

4. 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.$$

5. 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

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.

Motivation

Shor's factoring and discrete logarithm algorithms (Shor 1997) reduce both problems to sampling from the output of a quantum Fourier transform: a register holding a superposition with a hidden period is transformed, then measured, and the measured value carries information about the period. The whole speed-up rests on one engineering fact: for $q = 2^l$ the $q \times q$ Fourier matrix, which has $q^2 = 4^l$ entries, can be applied by a quantum circuit of only $O(l^2)$ elementary gates, each acting on one or two bits.

That circuit was found independently by Coppersmith (IBM RC 19642, 1994) and Deutsch, and Shor's §4 presents it following Ekert and Jozsa (Rev. Mod. Phys. 68, 1996). It is the quantum analogue of the radix-2 fast Fourier transform, and it reappears in phase estimation, in the hidden subgroup algorithms for abelian groups, and in every textbook account of quantum computation. This mission formalizes Shor's statement that the circuit computes the Fourier matrix, up to a reversal of the output bits, together with the two displayed steps of its verification.

Setting

A register of $l$ bits has one basis state $|a\rangle = |a_{l-1} a_{l-2} \dots a_0\rangle$ for every bit string, with $a_0$ the least significant bit; the string encodes the integer

$$a = \sum_{j=0}^{l-1} 2^j a_j, \qquad 0 \le a < q = 2^l .$$

A state is a vector of complex amplitudes, one per basis state. A gate is a matrix whose rows are indexed by input basis vectors and whose columns are indexed by output basis vectors (§2, p. 1489). A gate on some of the bits acts on those bits through its matrix and leaves the others alone (§2, p. 1490): the output amplitude at a string $b$ is the sum, over the possible input values $u$ of the acted-on bits, of the input amplitude at $b$ with those bits replaced by $u$, times the matrix entry from $u$ to the corresponding bits of $b$.

The Fourier matrix $A_q$ (eq. (4.1)) is the $q \times q$ matrix with $(a, c)$ entry $q^{-1/2}\exp(2\pi i\,ac/q)$; it takes $|a\rangle$ to $q^{-1/2}\sum_{c=0}^{q-1}\exp(2\pi i\,ac/q)\,|c\rangle$.

The circuit uses two gates (eqs. (4.2), (4.3)):

• $R_j$ acts on bit $j$ with matrix $\frac{1}{\sqrt 2}\begin{pmatrix} 1 & 1 \\ 1 & -1\end{pmatrix}$;
• $S_{j,k}$, for $j < k$, acts on bits $j$ and $k$ with matrix $\mathrm{diag}(1, 1, 1, e^{i\theta_{k-j}})$, where $\theta_{k-j} = \pi / 2^{k-j}$; it multiplies the amplitude of a basis state by $e^{i\theta_{k-j}}$ when bits $j$ and $k$ are both $1$.

The circuit is the gate sequence (4.4), applied from left to right:

$$R_{l-1}\, S_{l-2,l-1}\, R_{l-2}\, S_{l-3,l-1}\, S_{l-3,l-2}\, R_{l-3} \cdots R_1\, S_{0,l-1}\, S_{0,l-2} \cdots S_{0,2}\, S_{0,1}\, R_0 ,$$

that is, for $j = l-1, \dots, 0$ it applies $S_{j,l-1}, \dots, S_{j,j+1}$ and then $R_j$. On three bits it is $R_2 S_{1,2} R_1 S_{0,2} S_{0,1} R_0$.

The bit reversal of a string $b$ is the string $c$ with $c_k = b_{l-1-k}$.

Formalization targets

Goal: the circuit computes $A_q$ up to bit reversal (§4, p. 1496)

For every $l \ge 0$ and every basis state $|a\rangle$, with $q = 2^l$,

$$\text{circuit}\,|a\rangle = \frac{1}{q^{1/2}}\sum_{b}\exp(2\pi i\,ac/q)\,|b\rangle, \qquad c = \text{bit reversal of } b .$$

The sum runs over all $l$-bit strings $b$. Reading the output register in reverse order therefore yields $A_q|a\rangle$.

Milestone 1: the amplitude along the circuit (§4, eq. (4.5), p. 1496)

The amplitude of $|b\rangle$ in $\text{circuit}\,|a\rangle$ is

$$2^{-l/2}\exp\Big(i\Big(\sum_{0\le j<l}\pi a_jb_j + \sum_{0\le j<k<l}\frac{\pi}{2^{k-j}}a_jb_k\Big)\Big).$$

Milestone 2: the phase identity (§4, eqs. (4.6)–(4.10), pp. 1496–1497)

For bit strings $a, b$, with $c$ the bit reversal of $b$ and $a, c$ their values,

$$\exp\Big(i\Big(\sum_{0\le j<l}\pi a_jb_j + \sum_{0\le j<k<l}\frac{\pi}{2^{k-j}}a_jb_k\Big)\Big) = \exp(2\pi i\,ac/q).$$

Significance

The result. The goal says that $A_q$, a dense unitary on $2^l$ amplitudes, is realized by $l$ one-bit gates and $l(l-1)/2$ two-bit gates, followed by a relabelling of the output. This is what makes the Fourier sampling step of the factoring algorithm (§5) and of the discrete logarithm algorithm (§6) polynomial in the number of bits. Without it, the analyses of those sections describe measurements of states that no efficient circuit is known to prepare. The bit reversal is a real part of the statement: the circuit does not compute $A_q$ itself for $l \ge 2$, and an implementation must either permute the output bits or read them in reverse order.

Formalizing it. The identity is classical and its proof is short on paper; its content lies in bookkeeping that is easy to get wrong: which bit a gate touches, which of the input or output value a bit holds when a phase gate acts, and the order in which the gates are applied. A machine-checked version fixes all of these conventions explicitly and yields a reusable model of gate-level circuits on bit strings. To the drafter's knowledge there is no Lean formalization of this circuit on Prove2Me; the platform's FastFourierTransform rows state the classical Cooley–Tukey recursion for the unnormalized transform with the opposite sign, which is a different object.

Difficulty

Multiplying out the gate matrices is not an argument beyond tiny $l$: the difficulty is to control the whole product of $l(l+1)/2$ gates symbolically. The paper's argument (§4, p. 1496) is informal at exactly the points a formal proof must make precise: that only one sequence of intermediate basis states from $|a\rangle$ to $|b\rangle$ carries nonzero amplitude, and that at the moment $S_{j,k}$ acts, bit $k$ already holds its output value $b_k$ while bit $j$ still holds its input value $a_j$. Both facts depend on the order (4.4); applying the same gates in the reverse order gives a different unitary, whose phase pairs $b_j$ with $a_k$. The phase identity then holds only modulo $2\pi$, not as an equality of real numbers, so it cannot be closed by rearranging sums alone.

Formalization scope

• States. A bit string on $l$ bits is Fin l → Fin 2, with bit j equal to $a_j$ and value $\sum_j 2^j a_j$ (least significant bit first). A state is a function from bit strings to ℂ. The case $l = 0$ ($q = 1$, empty circuit) is included.
• Gate application follows the row = input convention: a one-bit gate $M$ on bit $j$ sends $\psi$ to $b \mapsto \sum_u \psi(b[j\mapsto u])\,M_{u, b_j}$, and a two-bit gate acts analogously on the pair (bit $j$, bit $k$).
• The circuit is the gate list (4.4) — an explicit list of constructors R j and S j k — run by a left fold, so the leftmost gate acts first. It is not defined as the matrix $A_q$ or by its entries; a definition of that kind would make the goal true by unfolding and is ruled out.
• Angles. $\theta_{k-j} = \pi/2^{k-j}$ uses natural-number subtraction, which is exact because the list only contains $S_{j,k}$ with $j < k$.
• Normalization. The prefactor $q^{-1/2}$ is written $(\sqrt{2^l})^{-1}$.
• Basis form. The goal is stated on basis states, as on the page; by linearity it determines the circuit on every state.
• Not stated. The gate count: the paper's sentence "we thus need to use $l(l-1)/2$ quantum gates" (p. 1496) counts only the gates $S_{j,k}$; the sequence (4.4) also contains the $l$ gates $R_j$, $l(l+1)/2$ gates in all. The approximate transform of Coppersmith and the one-bit construction of Griffiths and Niu (p. 1497) are out of scope, as is the polynomial-time claim.

Welcome contributions: proofs of the two milestones and the goal; general lemmas about one- and two-bit gate actions on Fin l → Fin 2 states (commutation of gates on disjoint bits, linearity, action on basis states), which are reusable for any gate-level circuit; and a proof that the circuit is unitary.

Selected references

• P. W. Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer, SIAM J. Comput. 26(5):1484–1509, 1997. https://doi.org/10.1137/S0097539795293172
• D. Coppersmith, An approximate Fourier transform useful in quantum factoring, IBM Research Report RC 19642, 1994. https://arxiv.org/abs/quant-ph/0201067
• A. Ekert and R. Jozsa, Quantum computation and Shor's factoring algorithm, Rev. Mod. Phys. 68:733–753, 1996. https://doi.org/10.1103/RevModPhys.68.733
• R. B. Griffiths and C.-S. Niu, Semiclassical Fourier transform for quantum computation, Phys. Rev. Lett. 76:3228–3231, 1996. https://doi.org/10.1103/PhysRevLett.76.3228