All missions

Motivation

The classical Chernoff bound controls the probability that a sum of independent, nonnegative, uniformly bounded random variables deviates from its mean, with exponentially small tails governed by the Kullback–Leibler divergence between two Bernoulli laws. Many problems in numerical linear algebra, graph sparsification, compressed sensing and randomized algorithms instead require control of a sum of independent random matrices: the smallest singular value of a random matrix with independent columns, the spectrum of a sampled Laplacian, or the conditioning of a random submatrix. For these, what matters is not a scalar sum but the extreme eigenvalues of a random positive-semidefinite matrix.

Ahlswede and Winter (2002) introduced a matrix version of the Laplace transform method and proved a matrix Chernoff bound for identically distributed summands. Tropp's paper (arXiv:1004.4389, Found. Comput. Math. 2012) replaced the Golden–Thompson step of their argument with Lieb's concavity theorem, obtaining a master tail bound for independent sums, and derived from it matrix Chernoff, Bernstein and Azuma inequalities that require no identical distribution and lose only a dimensional factor. This mission formalizes the matrix Chernoff inequalities of §5 of that paper.

Timeline:

• 2002, Ahlswede–Winter: matrix Laplace transform method; matrix Chernoff bound for i.i.d. summands via Golden–Thompson.
• 2010, Oliveira: a variant of the Laplace transform method used in Proposition 3.1 of the paper.
• 2010–2012, Tropp: master tail bound via Lieb's theorem (Theorem 3.6), and Theorem 5.1 / Corollary 5.2 for independent, non-identical psd summands.

Setting

All matrices are $d\times d$ complex matrices with $d\ge1$. For a self-adjoint (Hermitian) matrix $A$, $\lambda_{\max}(A)$ and $\lambda_{\min}(A)$ are its algebraically largest and smallest eigenvalues. The semidefinite order $A\preccurlyeq B$ means that $B-A$ is positive semidefinite (psd). Functions of a self-adjoint matrix are defined spectrally: if $A = Q\Lambda Q^*$ then $f(A) = Qf(\Lambda)Q^*$; this gives the matrix exponential $e^A$ and, on positive-definite matrices, the matrix logarithm $\log A$.

A random matrix is a measurable map $X:\Omega\to\mathbb C^{d\times d}$ on a probability space $(\Omega,\mathcal F,\mathbb P)$, and its expectation $\mathbb E X$ is taken entrywise. The matrix moment generating function of $X$ is $\theta\mapsto\mathbb E\,e^{\theta X}$.

The objects of the mission are independent random Hermitian matrices $X_1,\dots,X_n$ that are almost surely psd contractions: $X_k\succcurlyeq0$ and $\lambda_{\max}(X_k)\le1$. Their average expectation has extreme eigenvalues

$$\bar\mu_{\min} = \lambda_{\min}\Big(\frac1n\sum_{k=1}^n\mathbb E X_k\Big),\qquad \bar\mu_{\max}=\lambda_{\max}\Big(\frac1n\sum_{k=1}^n\mathbb E X_k\Big),$$

and the binary information divergence is

$$\mathrm D(a\,\|\,u) = a(\log a-\log u)+(1-a)(\log(1-a)-\log(1-u)),\qquad a,u\in[0,1].$$

In Lean these are lambdaMax, lambdaMin, mexp, mlog, mean and binDiv in the namespace MatrixTail.Chernoff.

Formalization targets

Goal: Theorem 5.1 (Matrix Chernoff I)

$$\mathbb P\Big\{\lambda_{\min}\Big(\tfrac1n\textstyle\sum_k X_k\Big)\le\alpha\Big\}\le d\,e^{-n\,\mathrm D(\alpha\|\bar\mu_{\min})}\quad(0\le\alpha\le\bar\mu_{\min}),$$ $$\mathbb P\Big\{\lambda_{\max}\Big(\tfrac1n\textstyle\sum_k X_k\Big)\ge\alpha\Big\}\le d\,e^{-n\,\mathrm D(\alpha\|\bar\mu_{\max})}\quad(\bar\mu_{\max}\le\alpha\le1).$$

Milestones

1. Theorem 3.6 (master tail bound): for every $\theta>0$ at which the mgfs exist, $\mathbb P\{\lambda_{\max}(\sum_kX_k)\ge t\}\le e^{-\theta t}\operatorname{tr}\exp(\sum_k\log\mathbb E\,e^{\theta X_k})$.
2. Corollary 3.9: the same with the mgfs under one logarithm, $d\cdot\exp(-\theta t+n\log\lambda_{\max}(\frac1n\sum_k\mathbb E\,e^{\theta X_k}))$.
3. Lemma 5.8 (Chernoff mgf): $\mathbb E\,e^{\theta X}\preccurlyeq\mathbf I+(e^\theta-1)\mathbb E X$ for a random psd contraction $X$.
4. Display (5.1): $\mathbb P\{\lambda_{\max}(\sum_kX_k)\ge t\}\le d\exp(-\theta t+n\log(1+(e^\theta-1)\bar\mu_{\max}))$.
5. Display (5.2): $\mathbb P\{\lambda_{\min}(\sum_kX_k)\le t\}\le d\exp(\theta t+n\log(1-(1-e^{-\theta})\bar\mu_{\min}))$.

Further statement

Corollary 5.2 (Matrix Chernoff II), the form usually quoted: with $\lambda_{\max}(X_k)\le R$, $\mu_{\min},\mu_{\max}$ the extreme eigenvalues of $\sum_k\mathbb E X_k$,

$$\mathbb P\{\lambda_{\min}(\textstyle\sum_kX_k)\le(1-\delta)\mu_{\min}\}\le d\Big[\tfrac{e^{-\delta}}{(1-\delta)^{1-\delta}}\Big]^{\mu_{\min}/R},\quad \mathbb P\{\lambda_{\max}(\textstyle\sum_kX_k)\ge(1+\delta)\mu_{\max}\}\le d\Big[\tfrac{e^{\delta}}{(1+\delta)^{1+\delta}}\Big]^{\mu_{\max}/R}.$$

Significance

Theorem 5.1 matches the strongest scalar Chernoff bound for independent, non-identical Bernoulli trials, up to the factor $d$, which cannot be removed (coupon collector, Remark 5.6). Corollary 5.2 is the version used in applications: lower bounds on the smallest singular value of matrices with independent columns (Remark 5.4), spectral sparsification, column subset selection and random sampling of matrices. Remark 5.5 derives from it the expectation bound $\mathbb E\lambda_{\max}(\sum_kX_k)\le C\max\{\mu_{\max},R\log d\}$.

The results are proved in the paper, from Lieb's concavity theorem. As far as is known, no machine-checked proof of a matrix Chernoff inequality exists in Lean or Mathlib. A formalization yields a reusable statement for the random-matrix and randomized-numerical-linear-algebra literature, and the milestones (the master bound, the single-logarithm corollary and the semidefinite mgf bound) are reusable beyond this mission.

Difficulty

The scalar Chernoff argument uses $\mathbb E\,e^{\theta(X+Y)}=\mathbb E\,e^{\theta X}\,\mathbb E\,e^{\theta Y}$ for independent $X,Y$. For matrices $e^{A+B}\neq e^Ae^B$ unless $A$ and $B$ commute, so the trace of the mgf of a sum does not factor. The Golden–Thompson inequality handles two summands but does not extend to three, which is why the Ahlswede–Winter bound needed identical distributions. The master bound (Theorem 3.6) requires Lieb's concavity theorem, which has no counterpart in Mathlib. Corollary 3.9 in addition needs operator concavity of the matrix logarithm, and Lemma 5.8 needs the transfer of a scalar inequality to the semidefinite order through the spectral calculus.

Formalization scope

Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d]; the semidefinite order is Mathlib's MatrixOrder (A ≤ B ↔ (B − A).PosSemidef). exp and log of a matrix are the continuous functional calculus cfc. $\lambda_{\max}$, $\lambda_{\min}$ are sSup/sInf of the real spectrum. Expectation is entrywise. Random matrices are measurable with respect to the Borel σ-algebra on matrices, independence is iIndepFun, and the probability measure is a probability measure. The summands are Hermitian for every outcome; "psd" and "$\lambda_{\max}\le1$" hold almost surely. The sequence has $n\ge1$ terms wherever an average $1/n$ appears. An infimum over $\theta>0$ is stated as a bound for every admissible $\theta>0$; integrability of $e^{\theta X_k}$ is a hypothesis only in Theorem 3.6 and Corollary 3.9, where the summands are unbounded. In Lean $\log 0=0$, so at the boundary values $\bar\mu\in\{0,1\}$ the divergence is finite where the paper's is $+\infty$; this only weakens the stated bound.

A formalization in which $d=0$ (empty spectrum, $\lambda_{\max}=0$) or $n=0$ (the average $1/0=0$) were allowed, or in which the range of $\alpha$ were dropped, would state a different, partly false theorem; these cases are excluded.

A complete development needs Lieb's theorem or another route to the master bound, operator concavity of the logarithm, the spectral mapping theorem and the transfer rule for the functional calculus on Hermitian matrices, monotonicity of the trace exponential, and the scalar optimization in $\theta$. Contributions of any of these as stand-alone lemmas are welcome.

Selected references

• J. A. Tropp, User-Friendly Tail Bounds for Sums of Random Matrices, arXiv:1004.4389v7 (2011); Found. Comput. Math. 12 (2012) 389–434. https://arxiv.org/abs/1004.4389, https://doi.org/10.1007/s10208-011-9099-z
• R. Ahlswede, A. Winter, Strong converse for identification via quantum channels, IEEE Trans. Inform. Theory 48 (2002) 569–579. https://doi.org/10.1109/18.985947
• E. H. Lieb, Convex trace functions and the Wigner–Yanase–Dyson conjecture, Adv. Math. 11 (1973) 267–288. https://doi.org/10.1016/0001-8708(73)90011-X
• R. I. Oliveira, Sums of random Hermitian matrices and an inequality by Rudelson, Electron. Commun. Probab. 15 (2010) 203–212. https://arxiv.org/abs/1004.3821

Motivation

In a time-inconsistent control problem, a control that is optimal when planned at time $t$ stops being optimal when the problem is re-solved at a later time. Two sources of time inconsistency are common in finance and economics. One is a variance term in the objective, as in continuous-time Markowitz mean–variance portfolio selection (Zhou–Li 2000; Basak–Chabakauri 2010). The other is a state-dependent target, as in Björk–Murgoci–Zhou 2014. Dynamic programming does not apply. A standard response is to look for an equilibrium: a control that no planner at any time $t$ can improve by an infinitesimal deviation on $[t,t+\varepsilon)$.

Hu, Jin and Zhou define open-loop equilibria for a general stochastic linear–quadratic (LQ) problem with both sources of time inconsistency. They give a sufficient condition through a flow of forward–backward SDEs, which is the subject of mission I of this series. This mission covers §4 of the paper: the scalar-state case with deterministic coefficients, where the equilibrium is computed explicitly from a system of coupled Riccati equations. Mission III covers §5, the mean–variance application with random coefficients.

Setting

On a probability space carrying a standard $d$-dimensional Brownian motion $W$ with its filtration $(\mathcal F_t)$, the state $X$ is scalar ($n=1$) and the control $u$ takes values in $\mathbb R^l$:

$$dX_s=[A_sX_s+B_s'u_s+b_s]\,ds+[C_sX_s+D_su_s+\sigma_s]'\,dW_s,\qquad X_0=x_0.$$

The coefficients are deterministic functions on $[0,T]$: $A_s,b_s,Q_s\in\mathbb R$, $B_s\in\mathbb R^l$, $C_s,\sigma_s\in\mathbb R^d$, $D_s\in\mathbb R^{d\times l}$ and $R_s\in\mathbb R^{l\times l}$ symmetric. $A,B,C,D,Q,R$ are bounded, $b,\sigma$ are square integrable, $Q\ge0$, $R\succeq0$, and $G\ge0$. At time $t$, in state $x_t$, the planner evaluates

$$J(t,x_t;u)=\tfrac12\mathbb E_t\!\int_t^T\!\big(Q_sX_s^2+\langle R_su_s,u_s\rangle\big)ds+\tfrac12\mathbb E_t[GX_T^2]-\tfrac h2\big(\mathbb E_t[X_T]\big)^2-(\mu_1x_t+\mu_2)\,\mathbb E_t[X_T],$$

where $\mathbb E_t=\mathbb E[\,\cdot\mid\mathcal F_t]$. The third term (the variance-like term) and the fourth term (which depends on $x_t$) make the problem time-inconsistent. A control $u^*$ with state $X^*$ is an equilibrium (Definition 2.1) if, for every $t\in[0,T)$ and every $\mathcal F_t$-measurable square-integrable $v$, the spike $u^{t,\varepsilon,v}=u^*+v\mathbf 1_{[t,t+\varepsilon)}$ satisfies

$$\liminf_{\varepsilon\downarrow0}\frac{J(t,X^*_t;u^{t,\varepsilon,v})-J(t,X^*_t;u^*)}{\varepsilon}\ge0.$$

With $\Gamma^{(1)}_s=\mu_1e^{\int_s^TA_r\,dr}$, $|C|^2=C'C$ and $K=(R+MD'D)^{-1}$, the coupled Riccati system (4.9) for deterministic $(M,N)$ is

$$\begin{aligned}\dot M&=-\big[2A+|C|^2+\Gamma^{(1)}B'K(B+D'C)\big]M-Q+(B+D'C)'K(B+D'C)M^2-B'K(B+D'C)MN,& M_T&=G,\\ \dot N&=-\big[2A+\Gamma^{(1)}B'KB\big]N+B'K(B+D'C)MN-B'KBN^2,& N_T&=h.\end{aligned}$$

Given $(M,N)$, a linear ODE (4.8) determines $\Phi$ with $\Phi_T=-\mu_2$. The candidate equilibrium is the linear feedback (4.4)

$$u^*_s=\alpha_sX^*_s+\beta_s,\quad\alpha_s=-K_s\big[(M_s-N_s-\Gamma^{(1)}_s)B_s+M_sD_s'C_s\big],\quad\beta_s=-K_s(\Phi_sB_s+M_sD_s'\sigma_s).$$

Formalization targets

Goal: Theorem 4.4

Suppose $G\ge h>0$ and one of three cases holds:

• (i) $R\succeq\delta I$, $\frac{QD'D+|C|^2R}{l}+\Gamma^{(1)}\mathcal S(D'CB')\succeq0$ and $B=\lambda D'C$ with $\lambda\ge0$;
• (ii) the first two conditions of (i) and $D'D\succeq\delta I$;
• (iii) $R\equiv0$, $D'D\succeq\delta I$, $Q+\Gamma^{(1)}B'(D'D)^{-1}(B+D'C)\ge0$ and $Q+\Gamma^{(1)}B'(D'D)^{-1}D'C\ge0$.

Then

$$\text{(4.9) has a unique positive solution pair }(M,N)\text{ on }[0,T],$$

and, for every solution $\Phi$ of (4.8), the closed-loop equation of (4.4) has a solution, and the feedback control along every closed-loop state is an equilibrium.

Milestones

• Proposition 4.1: a positive solution $(M,J)$ of the transformed system (4.10) gives the positive solution $(M,M/J)$ of (4.9).
• Theorem 4.2: existence and uniqueness of positive solutions of (4.10) and (4.9) in the standard case $R\succeq\delta I$.
• Theorem 4.3: existence for (4.13) and (4.9) in the singular case $R\equiv0$.
• Three steps from the proof of Theorem 4.4:
  • $\alpha$ is bounded, so $u^*$ is admissible and $X^*$ has continuous paths with $\mathbb E\sup_s|X^*_s|^2<\infty$;
  • the ansatz $p(s;t)=M_sX^*_s-N_s\mathbb E_t[X^*_s]-\Gamma^{(1)}_sX^*_t+\Phi_s$, $k(s;t)=M_s[C_sX^*_s+D_su^*_s+\sigma_s]$ solves the adjoint flow (3.10);
  • the identity $\Lambda(s;t)=N_s[X^*_s-\mathbb E_tX^*_s]B_s+\Gamma^{(1)}_s(X^*_s-X^*_t)B_s$ holds, and $\Lambda$ satisfies condition (3.4).

Significance

The theorem gives an equilibrium in closed form, as a linear feedback of the current state with deterministic gains. That makes the equilibrium computable and comparable with the classical, time-consistent LQ regulator. Setting $h=\mu_1=0$ recovers a standard LQ problem, but (4.9) differs from the classical Riccati equation even then: it is a nonsymmetric coupled system (footnote 2, p. 10), and the cases (i)–(iii) are the conditions under which it is solvable. The mean–variance results of §5 (mission III) follow the same pattern.

The result is proved in the paper; to our knowledge it has not been formalized. A formal proof needs global existence for a nonlinear, nonautonomous ODE system with Carathéodory coefficients, obtained by truncation and a priori bounds. It also needs linear SDEs with bounded feedback, Itô calculus for products of deterministic and Itô processes, and the sufficient condition of mission I. Uniqueness in case (iii) is claimed by Theorem 4.4 but not proved in Theorem 4.3; it is part of the goal.

Difficulty

The system (4.9) is quadratic in $(M,N)$. Its solutions can blow up in finite time, and $(R+MD'D)^{-1}$ can degenerate when $M$ changes sign. Picard–Lindelöf therefore gives only local solutions, and a global solution needs a priori bounds $0<\eta\le M\le L$ and $J\ge1$, with $\eta$ and $L$ independent of the truncation level. Those bounds are where the case hypotheses enter. In the stochastic half, the equilibrium property is not proved by computing $J$ directly. It requires checking that the explicit candidate meets the flow-of-FBSDE sufficient condition, and the flow carries a parameter $t$ and the conditional expectations $\mathbb E_t[X^*_s]$ for every $s\ge t$.

Formalization scope

The general model (data, standing assumptions, states, conditional cost, spike, equilibrium) is stated for arbitrary $n$ and instantiated at $n=1$ through toData. It is built on the published substrate Peng1990_SMP_Stochastic (Brownian motion, natural filtration, $L^2_{\mathcal F}$, Itô integrals, SDE solutions). The formalization commits to the following choices.

• Definition 2.1 uses $\liminf$ in $\overline{\mathbb R}$, along every sequence $\varepsilon_k\downarrow0$, almost surely for each sequence, and for every version of the state and of the perturbed states. The page writes $\lim$, which need not exist.
• The filtration is the natural, uncompleted filtration of $W$, not the augmented one.
• The state from time $t$ is encoded through the full horizon. The spike is additive on $[t,t+\varepsilon)$.
• "Essentially bounded" and "a.s., a.e." are read $d\mathbb P\otimes ds$-a.e.
• Every ODE ((4.8), (4.9), (4.10), (4.13)) is stated in integral form on $[0,T]$, because the coefficients are only bounded measurable. A solution includes invertibility of $R+MD'D$ (resp. $D'D$) on $[0,T]$. Uniqueness means agreement on $[0,T]$.
• The constants $\delta,\lambda$ are uniform in $s$, and the case conditions hold for every $s\in[0,T]$. In $\frac{QD'D+|C|^2R}{l}$, $l$ is the control dimension.
• "Let $\Phi$ be a solution of (4.8)" means every solution. "$u^*$ is an equilibrium" means that a closed-loop state exists and that the feedback is an equilibrium along every closed-loop state.
• Conditional-expectation families $\mathbb E_t[X^*_s]$ are handled through arbitrary progressive versions. Condition (3.4) is stated exactly: its first part as a localization on $\mathcal F_t$-sets, its second part with a jointly measurable version and "a.e. $s$".
• The paper's "$\beta$ uniformly bounded" is false when $\sigma$ is only square integrable. The milestone states the true claim: $\alpha$ is essentially bounded on $[0,T]$ (the coefficients are only essentially bounded) and $\beta$ is square integrable.

The goal's conclusion is Definition 2.1 itself; it does not mention $\Lambda$, $p$ or (3.4). Existence of the closed-loop state is asserted, not assumed. A formalization that assumes existence, or that replaces equilibrium by condition (3.4), is a different and weaker theorem.

Theorem 3.3 (the $n=1$ sufficient condition) is not posed here. Under the shared model it is mission I's goal at $n=1$. Contributions are welcome on the ODE layer (truncation, comparison and Gronwall bounds for Carathéodory systems), on linear SDEs with bounded feedback, and on the Itô product rule. These parts are reusable well beyond this paper.

Selected references

• Y. Hu, H. Jin, X. Y. Zhou, Time-Inconsistent Stochastic Linear–Quadratic Control, arXiv:1111.0818v1, 2011; SIAM J. Control Optim. 50(3), 2012. https://arxiv.org/abs/1111.0818
• T. Björk, A. Murgoci, X. Y. Zhou, Mean–variance portfolio optimization with state-dependent risk aversion, Mathematical Finance 24(1), 2014. https://doi.org/10.1111/j.1467-9965.2011.00515.x
• S. Basak, G. Chabakauri, Dynamic mean–variance asset allocation, Review of Financial Studies 23(8), 2010. https://doi.org/10.1093/rfs/hhq028
• X. Y. Zhou, D. Li, Continuous-time mean–variance portfolio selection: a stochastic LQ framework, Applied Mathematics and Optimization 42, 2000. https://doi.org/10.1007/s002450010003
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990. https://doi.org/10.1137/0328054
• J. Yong, X. Y. Zhou, Stochastic Controls: Hamiltonian Systems and HJB Equations, Springer, 1999. https://doi.org/10.1007/978-1-4612-1466-3
• Missions I and III of this series: the sufficient condition (Theorem 3.2) and the mean–variance equilibrium (Theorem 5.4).

Motivation

Many optimization problems in shape analysis, computer vision, numerical linear algebra and statistics have a feasible set that is not a vector space but a Riemannian manifold: spaces of curves modulo reparametrization, the Stiefel and Grassmann manifolds, fixed-rank matrices. On such a set the classical recipe "add a multiple of the search direction to the iterate" is not available, and line-search methods replace it by a retraction, a map that follows a tangent direction back onto the manifold (Absil, Mahony, Sepulchre 2008).

Quasi-Newton methods are the most widely used line-search methods in the Euclidean setting, and BFGS is the most popular of them. Transferring BFGS to a manifold raises a specific problem: the Hessian approximation $B_k$ lives on the tangent space at $x_k$, while the next one must live on the tangent space at $x_{k+1}$, so a vector transport $T_k$ between tangent spaces enters the update.

Timeline:

• Gabay (1982) proposed a Riemannian BFGS update with geodesics and parallel transport (doi:10.1007/BF00934767).
• Absil, Mahony and Sepulchre (2008) and Qi, Gallivan and Absil (2010) generalized it to arbitrary retractions and vector transports.
• Ring and Wirth (2012), the source of this mission, proved global convergence and an R-linear rate for transported BFGS on possibly infinite-dimensional Riemannian manifolds, assuming that the transports are isometries (doi:10.1137/11082885X).
• Later work by Huang, Gallivan and Absil (2015) relaxed the conditions on the transport (doi:10.1137/140955483).

Setting

Let $\mathcal M$ be a smooth manifold modelled on a real Hilbert space $E$, with a Riemannian inner product $g_x$ and norm $\|\cdot\|_x$ on each tangent space $T_x\mathcal M$. For $f:\mathcal M\to\mathbb R$, $\mathrm Df(x)$ is its differential, a functional on $T_x\mathcal M$ with dual norm $\|\mathrm Df(x)\|_x$.

A retraction is a family of smooth maps $R_x:T_x\mathcal M\to\mathcal M$ with $R_x(0)=x$ and $\mathrm DR_x(0)=\mathrm{id}$. Write $f_{R_x}=f\circ R_x$, a function on the vector space $T_x\mathcal M$, with derivatives $\mathrm Df_{R_x}$ and $\mathrm D^2f_{R_x}$.

Algorithm 1 produces iterates $x_{k+1}=R_{x_k}(\alpha_kp_k)$. The step $\alpha_k>0$ satisfies the Wolfe conditions with $0<c_1<c_2<1$:

$$f(R_x(\alpha p))\le f(x)+c_1\alpha\,\mathrm Df(x)p,\qquad \mathrm Df(R_x(\alpha p))\,\mathrm DR_x(\alpha p)\,p\ \ge\ c_2\,\mathrm Df(x)p.$$

The BFGS direction solves $B_k(p_k,\cdot)=-\mathrm Df(x_k)$ for a bounded bilinear form $B_k$ on $T_{x_k}\mathcal M$. With $s_k=\alpha_kp_k$ and $y_k=\mathrm Df_{R_{x_k}}(s_k)-\mathrm Df_{R_{x_k}}(0)$, the next form is defined on $T_{x_{k+1}}\mathcal M$ through an invertible linear map $T_k:T_{x_k}\mathcal M\to T_{x_{k+1}}\mathcal M$:

$$B_{k+1}(T_kv,T_kw)=B_k(v,w)-\frac{B_k(s_k,v)B_k(s_k,w)}{B_k(s_k,s_k)}+\frac{(y_kv)(y_kw)}{y_ks_k}.$$

The analysis uses the angle $\cos\theta_k=B_k(s_k,s_k)/(\|s_k\|\,\|B_k(s_k,\cdot)\|)$ and the Rayleigh quotient $q_k=B_k(s_k,s_k)/\|s_k\|^2$.

Formalization targets

Goal: Proposition 10

Assume:

• the $T_k$ are isometries;
• $B_0$ is symmetric and coercive;
• for $0<m<M$ and every $k$, the set $S_k=R_{x_k}^{-1}(\{f\le f(x_0)\})$ is convex and $m\|v\|^2\le\mathrm D^2f_{R_{x_k}}(p)(v,v)\le M\|v\|^2$ for $p\in S_k$;
• $x^*$ is a minimizer of $f$ that every $R_{x_k}$ reaches.

Then there is $0<\mu<1$ with

$$f(x_{k+1})-f(x^*)\le\mu^{k+1}\big(f(x_0)-f(x^*)\big)\qquad\forall k\in\mathbb N.$$

The rate $\mu$ is not specified: the goal asserts only R-linear convergence, the shape of the result.

Milestones, in proof order

1. Lemma 9. If $\|T_k\|$ and $\|T_k^{-1}\|$ are uniformly bounded and $B_0$ is (symmetric and) coercive, then $y_ks_k>0$ and every $B_k$ is coercive.
2. Curvature-pair bounds. $\|y_k\|^2/(y_ks_k)\le M$ and $y_ks_k/\|s_k\|^2\ge m$.
3. Good indices. For every $0<r<1$ there are $\kappa,\rho,\sigma>0$ such that every $k$ has at least $\lfloor r(k+1)\rfloor$ indices $i\le k$ with $\cos\theta_i\ge\kappa$ and $\rho\le q_i/\cos\theta_i\le\sigma$.
4. Step-length bound. $\alpha_i\ge\frac{1-c_2}{M}q_i$.
5. Gradient dominance. $f(x)-f(x^*)\le\|\mathrm Df(x)\|^2/(2m)$ on the sublevel set.
6. Rate display. Given milestone 3's constants,

$$f(x_{k+1})-f(x^*)\le\Big(1-\tfrac{1-c_2}{M}c_1\tfrac{\kappa^2\rho}{\sigma}2m\Big)^{\lfloor r(k+1)\rfloor}\big(f(x_0)-f(x^*)\big).$$

Significance

The result. Proposition 10 is a global convergence guarantee for a quasi-Newton method on manifolds, with no restriction to a neighbourhood of the minimizer and no finite-dimensionality. It applies to Riemannian shape spaces of curves, where the paper's numerical experiments take place. The paper's superlinear-rate theory (Proposition 12, Corollary 13) starts from this linear rate.

Formalizing it. The result is proved on paper but has not been machine-checked. A formal proof also checks the delicate points of the infinite-dimensional argument, in particular the use of traces and Fredholm determinants of trace-class perturbations of the identity. The statement as printed needs a correction: the printed bound $f(x_k)-f(x^*)\le\mu^{k+1}(f(x_0)-f(x^*))$ fails at $k=0$, and the formal goal bounds $f(x_{k+1})$, as the appendix's own final display does.

Difficulty

The Euclidean proof idea of bounding the eigenvalues of $B_k$ uniformly does not work for BFGS: those eigenvalues are not uniformly controlled. The Byrd–Nocedal argument replaces them by trace and determinant estimates, which show that a fixed fraction of the iterations have well-conditioned angles. In infinite dimensions the trace and the determinant of $B_k$ do not exist. One must work with $A_k\hat B_kA_k-\mathrm{id}$, which is trace class, and with the Fredholm determinant, and show that isometric transports leave these quantities invariant. That invariance is exactly where the isometry hypothesis enters. Lemma 9 is also not a finite-dimensional triviality: positive definiteness of $B_{k+1}$ does not give coercivity, and a separate compactness-free argument is needed.

Formalization scope

The manifold is a Mathlib ChartedSpace E M, with $E$ a complete real inner-product space, IsManifold 𝓘(ℝ, E) ∞ M, and a RiemannianBundle on TangentSpace 𝓘(ℝ, E). Every norm on a tangent space is the Riemannian one. $\mathrm Df(x)$ is mfderiv, read as a functional on $T_x\mathcal M$, and its norm is the operator norm.

Committed conventions and explicit readings:

• One retraction family $R$ for all $k$. The paper allows a different retraction per step.
• Smoothness of $R_x$ is stated for the map out of the model space $E$, which carries the topology of $T_x\mathcal M$.
• The run equation $x_{k+1}=R_{x_k}(\alpha_kp_k)$ is an explicit hypothesis: it is what identifies $T_{x_{k+1}}\mathcal M$ with the tangent space at the new point. The $B_k$ and $T_k$ (as continuous linear equivalences) are data constrained by the update formula.
• Regularity and non-termination: $\alpha_k>0$, $f$ differentiable, $f_{R_{x_k}}$ of class $C^2$, and $\mathrm Df(x_k)\neq0$ for all $k$. Only runs that never stop are covered.
• Symmetry of $B_0$ is assumed in Lemma 9 as well. The lemma's proof uses it, and without it the first update can lose coercivity.
• Convexity of $S_k$ is part of "uniformly convex on the sublevel set". Without it, a double-well function whose sublevel set has two strongly convex components is a counterexample.
• Reachability of $x^*$ by every $R_{x_k}$ is assumed, since the appendix uses $R_{x_k}^{-1}(x^*)$.
• Dropped assumptions: geodesic completeness, separability, the distance and the Levi-Civita connection are not used and are dropped.
• Corrected index: the rate display and the goal bound $f(x_{k+1})$, because the decrease obtained at a good index $i$ improves $x_{i+1}$.

A trivializing formalization is ruled out on three fronts. A sorry-free check on $\mathcal M=E=\mathbb R$, with $R_x(v)=x+v$, $f(x)=x^2/2$ and $x_{k+1}=0.4x_k$, shows that the run hypotheses are satisfiable. Every quotient in a statement has a positive denominator along such a run. The rate $\mu$ is quantified after the run and before $k$.

Infrastructure that a complete development needs, and that is reusable beyond this mission:

• calculus of $f\circ R_x$ on a tangent space with its Riemannian norm;
• Taylor's formula with integral remainder;
• trace-class operators and Fredholm determinants on Hilbert spaces, with Lidskii's theorem.

The last item is absent from Mathlib, and contributions toward it are welcome. The paper's other main result, convergence of Fletcher–Reeves conjugate gradients (Proposition 15), is a separate mission. The superlinear-rate results (Lemma 6, Propositions 5, 7, 8, 12, Corollaries 11, 13) and the numerical §4 are out of scope.

Selected references

• W. Ring, B. Wirth, Optimization Methods on Riemannian Manifolds and Their Application to Shape Space, SIAM J. Optim. 22(2), 596–627, 2012. https://doi.org/10.1137/11082885X
• P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244
• D. Gabay, Minimizing a differentiable function over a differential manifold, J. Optim. Theory Appl. 37, 177–219, 1982. https://doi.org/10.1007/BF00934767
• R. H. Byrd, J. Nocedal, A tool for the analysis of quasi-Newton methods with application to unconstrained minimization, SIAM J. Numer. Anal. 26(3), 727–739, 1989. https://doi.org/10.1137/0726042
• W. Huang, K. A. Gallivan, P.-A. Absil, A Broyden class of quasi-Newton methods for Riemannian optimization, SIAM J. Optim. 25(3), 1660–1685, 2015. https://doi.org/10.1137/140955483

Motivation

Mean–variance portfolio selection (Markowitz, 1952) trades off the expected terminal wealth of an investor against its variance. In a dynamic setting the problem is time-inconsistent: the variance is not a conditional expectation of a function of terminal wealth, so the dynamic-programming principle fails, and a strategy that is optimal when computed at time $0$ is no longer optimal when re-evaluated at a later time. A standard response is to treat the investor at each time $t$ as a separate player and to look for a subgame-perfect equilibrium strategy, which no future self wishes to deviate from locally (Björk–Murgoci, Ekeland–Lazrak, and others).

Hu, Jin and Zhou (arXiv:1111.0818v1; SIAM J. Control Optim. 50(3), 2012) define open-loop equilibria for a general class of time-inconsistent stochastic linear–quadratic (LQ) problems and characterize them through a flow of forward–backward SDEs. Their §5 applies this to mean–variance investment in a complete market with a random risk premium, where the weight on expected wealth depends on current wealth (a state-dependent risk aversion, motivated in Björk–Murgoci–Zhou, 2014). Earlier equilibrium results for mean–variance investment (Basak–Chabakauri, 2010; Björk–Murgoci–Zhou) work with deterministic or Markovian coefficients and within feedback classes.

This mission is the third of a series on the paper. Mission I formalizes the general sufficient condition (Theorem 3.2); Mission II treats deterministic coefficients and coupled Riccati equations (Theorem 4.4). This mission targets the explicit mean–variance equilibrium of Theorem 5.4.

Setting

Fix a horizon $T>0$ and a probability space carrying a standard $d$-dimensional Brownian motion $W$ with its filtration $(\mathcal F_t)$; write $E_t=E[\,\cdot\,|\mathcal F_t]$. The market has a deterministic bounded interest rate $r$ and a progressively measurable, essentially bounded risk premium $\theta$ with values in $\mathbb R^d$. A strategy is a progressively measurable $u$ with $E\int_0^T|u_s|^2ds<\infty$ (the class $L^2_{\mathcal F}(0,T;\mathbb R^d)$); the wealth $X$ under $u$ solves

$$dX_s=r_sX_s\,ds+\theta_s'u_s\,ds+u_s'\,dW_s,\qquad X_0=x_0 .\tag{5.2}$$

At time $t$, with current wealth $x_t$, the investor's cost is

$$J(t,x_t;u)=\tfrac12\mathrm{Var}_t(X_T)-(\mu_1x_t+\mu_2)E_t[X_T],\qquad\mu_1\ge0 .\tag{5.3}$$

This is the case $n=1$ of the paper's general LQ problem, with $A=r$, $B=\theta$, $C=0$, $D=I$, $Q=R=0$, $G=h=1$; the mission states it that way. For $t\in[0,T)$, $\varepsilon>0$ and an $\mathcal F_t$-measurable square-integrable $v$, the spike $u^{t,\varepsilon,v}_s=u_s+v\,\mathbf 1_{[t,t+\varepsilon)}(s)$ perturbs $u$ on a short window. A strategy $u^*$ with wealth $X^*$ is an equilibrium (Definition 2.1) if, for all such $t$ and $v$,

$$\liminf_{\varepsilon\downarrow0}\frac{J(t,X^*_t;u^{t,\varepsilon,v})-J(t,X^*_t;u^*)}{\varepsilon}\ge0\quad\text{a.s.}$$

The equilibrium is built from $\Gamma^{(1)}_s=\mu_1e^{\int_s^Tr}$, $\Gamma_s=-\mu_2e^{\int_s^Tr}$, and two backward SDEs: an indefinite stochastic Riccati equation for $(M,U)$,

$$dM_s=-\big(2r_sM_s-U_s'\theta_s+\Gamma^{(1)}_s|\theta_s|^2-M_s^{-1}|U_s|^2+\Gamma^{(1)}_sM_s^{-1}U_s'\theta_s\big)ds+U_s'\,dW_s,\quad M_T=1,\tag{5.8}$$

and a linear BSDE (5.13) for $(\Gamma^{(2)},\gamma^{(2)})$ whose coefficients involve $M$ and $U$. A process $Z$ gives a BMO martingale $Z\cdot W$ if $E[\int_\tau^T|Z_s|^2ds\,|\,\mathcal F_\tau]\le C$ for all stopping times $\tau\le T$.

Formalization targets

Goal: Theorem 5.4

If $(M,U)$ solves (5.8) with $M$ bounded and $M\ge c>0$, and $(\Gamma^{(2)},\gamma^{(2)})$ solves (5.13) with $\Gamma^{(2)}$ bounded, then

$$u^*_s=-M_s^{-1}\Big[\big(U_s-\theta_s\mu_1e^{\int_s^Tr_v\,dv}\big)X^*_s+\Gamma_s\theta_s+\gamma^{(2)}_s\Big]$$

is an equilibrium: the closed-loop wealth exists, and for every closed-loop wealth $X^*$ the strategy $u^*$ satisfies Definition 2.1.

Milestones

1. Proposition 5.1: (5.8) has a unique solution in $L^\infty\times L^2$ with $M\ge c>0$, and $U\cdot W$ is BMO.
2. Proposition 5.2: (5.13) has a unique solution in $L^\infty\times L^2$, and $\gamma^{(2)}\cdot W$ is BMO.
3. Proposition 5.3: the closed-loop wealth under the feedback exists with continuous paths, $E\sup_t|X^*_t|^2<\infty$, and $u^*\in L^2$.
4. Proof of Theorem 5.4: the processes $p(s;t)$, $k(s;t)$ of (5.5) and (5.7) solve the adjoint equation (5.4), $\Lambda(s;t)=p(s;t)\theta_s+k(s;t)$ has the closed form displayed on p. 22, and $\Lambda$ meets condition (3.4).

Significance

Theorem 5.4 gives the equilibrium of a time-inconsistent mean–variance investor in closed form, linear in current wealth, for a random risk premium. With a deterministic premium it reduces to explicit formulas (§5.4), and for $\mu_1=0$ it recovers the equilibrium of Basak–Chabakauri and Björk–Murgoci; for $\mu_2=0$ it differs from the feedback equilibrium of Björk–Murgoci–Zhou, which shows that open-loop and feedback equilibria are different notions. The random premium is what makes $U\neq0$ and the feedback gain unbounded.

The result is proved in the paper; nothing here is formalized elsewhere. The mission produces machine-checked statements of the equilibrium, of solvability of the Riccati-type BSDE (5.8), and of the integrability of a linear SDE with BMO-type coefficients, on the platform's published stochastic-calculus substrate. The definition of BMO martingales and the encoding of open-loop equilibria are reusable beyond this paper.

Difficulty

The verification step that most readers try first, plugging $u^*$ into the wealth equation and applying standard SDE estimates, fails: the gain $\alpha=(\Gamma^{(1)}\theta-U)/M$ is unbounded, because $U$ is only BMO, so the closed-loop SDE is linear with non-Lipschitz-bounded random coefficients and neither existence of the wealth nor $u^*\in L^2$ follows from standard theory (Proposition 5.3). The BSDE (5.8) has a driver with quadratic growth in $U$ and a singular factor $M^{-1}$; it is not covered by the standard theory of stochastic Riccati equations and its solution must be bounded away from zero for the feedback to make sense. Uniqueness in (5.8) and solvability of (5.13) rely on BMO-martingale and change-of-measure facts (Kazamaki) that are not in Mathlib. Finally, the equilibrium property is a statement about every $t$ and every perturbation, and the sufficient condition (Theorem 3.3) needs the limit behaviour of conditional expectations $E_t[\Lambda(s;t)]$ as $s\downarrow t$.

Formalization scope

Everything is built on the published definition Peng1990_SMP_Stochastic (Brownian motion, $L^2_{\mathcal F}$, Itô integrals, SDEs and BSDEs as relations). The general LQ model, the spike, the conditional cost and Definition 2.1 are in Model; the adjoint equation on $[t,T]$, $\Lambda$ and condition (3.4) in Adjoint; the market, $\Gamma^{(1)}$, $\Gamma$, BMO, (5.8), (5.13) and (5.14) in Market. Conventions the statements commit to:

• Lower limit. Definition 2.1 is stated with $\liminf$ in $\overline{\mathbb R}$, along every sequence $\varepsilon_k\downarrow0$, almost surely for each sequence. The page writes $\lim$; the limit need not exist, and the paper's own argument bounds the lower limit.
• Filtration. The natural, uncompleted filtration of $W$ instead of the augmented one; conditional expectations and progressive processes agree up to null sets.
• States from time $t$ are solutions on the whole horizon $[0,T]$ for a control equal to $u^*$ before $t$.
• Versions. Conditions involving conditional expectations at uncountably many times are stated through jointly measurable versions; "a.s., a.e." means $ds\otimes dP$-a.e.; uniqueness of BSDE solutions is up to modification and $ds\otimes dP$-null sets; BMO is in integrated form.
• Market primitive. The risk premium $\theta$ is the primitive, as in (5.2); every bounded progressive $\theta$ comes from some bounded $(\mu,\sigma)$ with $\sigma\sigma'\succeq\varepsilon I$.
• Existence statements. Peng's SDE solutions already carry $u^*\in L^2$ and $\sup_tE|X_t|^2<\infty$, so Proposition 5.3 is stated as existence of a closed-loop solution with continuous paths and $E\sup_t|X^*_t|^2<\infty$. Theorem 5.4 asserts existence of the closed-loop wealth instead of assuming it.

The goal does not assume the BMO properties of $U$ and $\gamma^{(2)}$ (they are conclusions of Propositions 5.1–5.2), does not assume $\theta$ deterministic or $U=0$ (that is the special case of §5.4), and keeps $Q=R=0$, $G=h=1$; a formalization that assumes any of these, or that admits the junk value $M^{-1}=0$ on a non-null set, proves a different theorem. Theorem 3.3, the sufficient condition used in the last line of the proof, is the $n=1$ case of Mission I's goal and is not restated here. Welcome contributions: a BMO and Girsanov library on the Peng substrate, existence for quadratic BSDEs, and a proof of the sufficient condition.

Selected references

• Y. Hu, H. Jin, X. Y. Zhou, Time-Inconsistent Stochastic Linear–Quadratic Control, arXiv:1111.0818v1, 2011; SIAM J. Control Optim. 50(3), 2012. https://arxiv.org/abs/1111.0818
• S. Basak, G. Chabakauri, Dynamic mean-variance asset allocation, Rev. Financ. Stud. 23(8), 2010. https://doi.org/10.1093/rfs/hhq028
• T. Björk, A. Murgoci, X. Y. Zhou, Mean–variance portfolio optimization with state-dependent risk aversion, Math. Finance 24(1), 2014. https://doi.org/10.1111/j.1467-9965.2011.00515.x
• N. Kazamaki, Continuous Exponential Martingales and BMO, Lecture Notes in Math. 1579, Springer, 1994. https://doi.org/10.1007/BFb0073585
• M. Kobylanski, Backward stochastic differential equations and partial differential equations with quadratic growth, Ann. Probab. 28(2), 2000. https://doi.org/10.1214/aop/1019160253
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990. https://doi.org/10.1137/0328054

Motivation

A real number is normal in base $b$ when every block of $k$ base-$b$ digits occurs in its expansion with limiting frequency $b^{-k}$, exactly as it would in a sequence of independent uniformly random digits. It is normal (absolutely normal) when it is normal in every base $b\ge 2$. Whether the classical constants of analysis, above all $\pi$, are normal is one of the oldest open questions linking number theory and probability: it asks whether a number defined by geometry has digits that are statistically indistinguishable from random ones.

Timeline.

• 1909. Borel introduces normality and proves that Lebesgue-almost every real number is normal in every base (Borel 1909). The proof is non-constructive and gives no explicit example.
• 1933. Champernowne gives the first explicit normal numbers. The best known is $0.123456789101112\ldots$, the positive integers written one after another, which is normal in base ten (Champernowne 1933, Theorems I–IV). He conjectures that $0.235711131719\ldots$, built from the primes, is also normal.
• 1946. Copeland and Erdős prove that $0.a_1a_2a_3\ldots$ is normal in base $b$ for every increasing sequence of positive integers $a_n$ that contains more than $N^\theta$ terms up to $N$ for every $\theta<1$ and all large $N$. This settles Champernowne's conjecture for the primes (Copeland–Erdős 1946).
• 1997–2001. The Bailey–Borwein–Plouffe formula computes binary digits of $\pi$ without the earlier ones (BBP 1997). Bailey and Crandall reduce the base-2 normality of $\pi$ to a conjecture on a specific discrete dynamical system (Bailey–Crandall 2001). The conjecture remains open.
• 2002. Becher and Figueira give a computable absolutely normal number (Becher–Figueira 2002).

Large-scale digit computations of $\pi$ are statistically consistent with normality. No base is known in which $\pi$ is normal, and it is not even known that any particular digit occurs infinitely often in its decimal expansion.

Setting

A digit sequence is a function $s:\mathbb N\to\mathbb N$; $s_0$ is the first digit after the point. A word is a finite list $w=(w_0,\dots,w_{k-1})$ of naturals. For $N\in\mathbb N$, the occurrence count $\mathrm{count}(s,w,N)$ is the number of positions $i<N$ with $s_{i+j}=w_j$ for every $j<k$. Overlapping occurrences each count.

The sequence $s$ is normal in base $b$ (IsNormalSeq b s) if, for every word $w$ with all entries $<b$,

$$\lim_{N\to\infty}\frac{\mathrm{count}(s,w,N)}{N}=b^{-|w|}.$$

The $n$-th base-$b$ digit of a real $x$ after the point is

$$\mathrm{digit}_b(x,n)=\lfloor x\,b^{\,n+1}\rfloor \bmod b .$$

The real $x$ is normal in base $b$ (IsNormalReal b x) if $n\mapsto \mathrm{digit}_b(x,n)$ is normal in base $b$. Two remarks:

• The integer part of $x$ plays no role.
• For a rational number with two expansions, the floor selects the one not ending in repeated $(b-1)$'s.

Formalization targets

Goal: $\pi$ is normal

$$\forall\, b\in\mathbb N,\quad b\ge 2\ \Longrightarrow\ \pi \text{ is normal in base } b.$$

This is the conjecture in its standard form, normality in every base. The base-ten case is the special case $b=10$.

Milestones

None are listed. No decomposition of this problem into intermediate statements is known that would be a faithful attack path, and the mission does not invent one. Proposals for intermediate targets are welcome in the discussion; see the contributions listed under Formalization scope.

The known theorems of the subject (Champernowne's constructions, the Copeland–Erdős theorem, Borel's theorem) concern numbers built to be normal or almost every number; they are not steps toward $\pi$ and are kept in the separate mission Explicit normal numbers: Champernowne and Copeland–Erdős.

Significance

A proof that $\pi$ is normal in base $b$ would give every finite digit pattern a definite limiting frequency in its expansion. It would be the first normality result for a classical constant not built to be normal. Every known normal number is constructed digit by digit (Champernowne, Copeland–Erdős, Sierpiński, Becher–Figueira) or shown to exist by a measure argument (Borel). Even the base-2 case would settle the Bailey–Crandall programme for $\pi$.

Formalization status. The goal is open mathematics. The definitions it is stated with are published and are shared with the mission Explicit normal numbers: Champernowne and Copeland–Erdős, where Champernowne's theorems and the Copeland–Erdős theorem have machine-checked proofs.

Difficulty

The constructive results all prove normality from the digit-by-digit description of the number. In particular, the Copeland–Erdős block criterion needs the expansion to be an explicit concatenation of blocks. $\pi$ has no such description. Its known series (Machin-type formulas, BBP) give digits as values of exponential sums, and no known method controls the joint distribution of long digit blocks of such values.

Borel's theorem does not help: it only says that the exceptional set is null, and gives no criterion for deciding whether a given number lies in it. Neither high-precision digit statistics nor irrationality measures for $\pi$ imply normality.

Formalization scope

All declarations live in the namespace Normal and use the definition bundle Normal_Core:

• count, IsNormalSeq, digit, IsNormalReal;
• ofDigits b s $=\sum_n s_n b^{-(n+1)}$;
• the concatenation operators flatten, digitsBE, concatDigits;
• the Champernowne and Copeland–Erdős constants.

Committed conventions:

• Digits are read after the point, with the floor convention above.
• Frequencies are limits of real quotients.
• Words of every length $k\ge0$ are quantified, with entries $<b$.
• The goal ranges over all natural bases $b\ge2$. The degenerate bases $0$ and $1$ are excluded by hypothesis, not by convention.

The definitions agree with Borel's, and the mission does not admit a trivialising reading. A real number is not normal merely because it is irrational, and the empty word imposes only the trivial condition.

The bundle also contains a verbatim copy of the integer-arithmetic definition IsNormal from xiangyazi24/agafonov; its equivalence with IsNormalSeq is proved on the platform (Normal.isNormalSeq_iff_isNormal), so results stated in either form transfer.

Welcome contributions:

• Borel's theorem, via the strong law of large numbers or a Chernoff bound for digit blocks;
• equivalent characterisations of normality, such as Wall's criterion by uniform distribution of $b^n x \bmod 1$ and the reduction from all words to aligned blocks;
• conditional reductions, such as the Bailey–Crandall hypothesis implying base-2 normality of $\pi$.

Selected references

• É. Borel, Les probabilités dénombrables et leurs applications arithmétiques, Rend. Circ. Mat. Palermo 27 (1909), 247–271. https://doi.org/10.1007/BF03019651
• D. G. Champernowne, The construction of decimals normal in the scale of ten, J. London Math. Soc. 8 (1933), 254–260. https://doi.org/10.1112/jlms/s1-8.4.254
• A. H. Copeland and P. Erdős, Note on normal numbers, Bull. Amer. Math. Soc. 52 (1946), 857–860. https://doi.org/10.1090/S0002-9904-1946-08657-7
• D. Bailey, P. Borwein and S. Plouffe, On the rapid computation of various polylogarithmic constants, Math. Comp. 66 (1997), 903–913. https://doi.org/10.1090/S0025-5718-97-00856-9
• D. H. Bailey and R. E. Crandall, On the random character of fundamental constant expansions, Experiment. Math. 10 (2001), 175–190. https://doi.org/10.1080/10586458.2001.10504441
• V. Becher and S. Figueira, An example of a computable absolutely normal number, Theoret. Comput. Sci. 270 (2002), 947–958. https://doi.org/10.1016/S0304-3975(01)00170-0

Motivation

Random time changes occur when a process is observed on an operational clock rather than calendar time. In queueing models, for example, an arrival-count path may be evaluated at an evolving service clock. A functional limit theorem for the outer path and another for the clock are useful together only when evaluating one path at the times supplied by the other preserves convergence. Ward Whitt's 1980 paper studies several path operations with this question in mind; composition is its first main operation. The issue is specific to paths with jumps, because a small shift of the clock can move an evaluation across a jump.

Setting

Let $T_1,T_2,T_3$ be nonempty intervals of real time, with $T_2\subseteq T_3$, and let $(S,m)$ be a complete separable metric space. The càdlàg path space $D(T,S)$ consists of paths that are right continuous and have left limits on $T$. Its subspace $C(T,S)$ contains the continuous paths. The nondecreasing clock space $D_0(T_1,T_2)$ consists of càdlàg real-valued paths on $T_1$ that are nondecreasing and take their values in $T_2$. Its subspace $C_0(T_1,T_2)$ contains the continuous, strictly increasing clocks. For $x\in D(T_3,S)$ and $y\in D_0(T_1,T_2)$, composition is the path $(x\circ y)(t)=x(y(t))$ on $T_1$.

Convergence uses the Skorohod $J_1$ topology. On a compact interval $[a,b]$, let $\Lambda_{[a,b]}$ be the increasing homeomorphisms of $[a,b]$ and let $e(t)=t$. With $\rho_{[a,b]}$ denoting uniform distance, Whitt's metric is

$$d_{[a,b]}(u,v)=\inf_{\lambda\in\Lambda_{[a,b]}} \max\{\rho_{[a,b]}(\lambda,e),\rho_{[a,b]}(u,v\circ\lambda)\}.$$

Thus close paths may have nearby jumps at different times, provided an increasing time change aligns them. On a general interval, convergence is checked on compact subintervals whose endpoints are continuity points of the limit or endpoints of the full interval. Whitt gives this definition in §2, then gives $C$, $C_0$, and $D_0$ in §3. All subsets carry relative topologies and products carry product topologies.

Formalization targets

Composition at a continuous outer path

For $x_n\to x$ in $D(T_3,S)$ and $y_n\to y$ in $D_0(T_1,T_2)$, the first milestone states

$$x\in C(T_3,S)\quad\Longrightarrow\quad x_n\circ y_n\to x\circ y\text{ in }D(T_1,S).$$

The path-space definition and the two preparatory milestones are a small-oscillation partition for a càdlàg path, cited by Whitt from Billingsley, and Whitt's Lemma 2.2, which relates convergence on a compact interval to convergence on the two pieces made by splitting it at a continuity point.

Composition at a strictly increasing clock

The second case, and the combined goal, also allow the outer limit path to jump. Let $\partial_T T_1$ mean the endpoints of $T_1$ that belong to $T_1$. The corrected target is

$$\left[x\in C(T_3,S)\quad\text{or}\quad \bigl(y\in C_0(T_1,T_2)\ \text{and} x\text{ is continuous at }y(t)\text{ for every }t\in\partial_T T_1\bigr)\right] \Longrightarrow x_n\circ y_n\to x\circ y\text{ in }D(T_1,S).$$

The goal includes both cases for simultaneously varying $x_n$ and $y_n$. The endpoint condition is vacuous for an endpoint excluded from $T_1$. It is part of the strictly increasing clock case only; it imposes no extra restriction when the outer limit path is continuous.

Significance

This theorem supplies a precise condition for carrying two path limits through a random time transformation. In particular, the assertion includes convergence of the composed paths as elements of a càdlàg space, not merely convergence of their values at individual times. The distinction matters at jumps: pointwise convergence does not control the placement or ordering of nearby jumps. The result is a deterministic continuity statement that can be paired with probabilistic mapping theorems when the corresponding random paths are available.

Whitt proved the composition theorem in 1980, subject to the endpoint issue described below. The formalization work here is to construct its path-space interface in Lean, state the corrected continuity theorem with every domain condition visible, and eventually replace the open sorry proofs with checked proofs. The interface can also support the paper's later results on reflection, first passage, and time reversal; those results are separate missions. No proof of this mission's goal is claimed yet.

Difficulty

The tempting argument is to use separate continuity of $x_n\to x$ and $y_n\to y$ and then substitute $y_n(t)$ into the first convergence. That argument loses control of evaluations near a jump of $x$. A $J_1$ time change may align a jump of $x_n$ with the corresponding jump of $x$, while the clock $y_n$ may cross those times differently. Continuity of the outer limit path removes that difficulty in one case; in the other, the clock must be continuous and strictly increasing. The source explicitly shows that composition is not continuous on all of $D\times D_0$ (§3, p. 75).

The endpoints impose a further obstruction because increasing homeomorphisms of a closed time interval fix its endpoints. Bauer's Remark on p. 75 observes a failure at the right endpoint. There is a symmetric failure at the left endpoint, so the statement here includes both. This is a correction to the printed theorem, not a new claim that the uncorrected theorem is true.

Formalization scope

Paths are represented as total functions $\mathbb R\to S$, with only values on the named interval used. The domain assumptions OrdConnected and Nonempty express nonempty real intervals. The outer interval $T_3$ is also required to have nonempty interior: the formal convergence predicate checks only compact intervals $[a,b]$ with $a<b$, so on a one-point $T_3$ it imposes nothing, and the $C\times D_0$ case would fail for constant outer paths with different values. A clock's range condition is explicit, as is nondecreasingness for every prelimit clock. Membership of all paths in the relevant càdlàg spaces is part of the convergence predicates. The output predicate likewise requires every composition and its limit to be càdlàg. This rules out the trivialization in which one merely proves convergence of selected point evaluations or assumes the compositions already have the conclusion's path-space properties.

The compact uniform distance and the infimum over time changes take values in $[0,\infty]$. They use the actual metric on $S$, not a real supremum with a default value on an unbounded set. A time change is a total function whose restriction to the compact interval is continuous, strictly increasing, and onto. Continuity at a time means continuity relative to the path's interval. The general-interval convergence predicate checks the compact intervals specified by Whitt and requires each sequence member to belong to $D$. The theorem is written as sequential continuity; Whitt's $J_1$ spaces are metrizable, making that equivalent to topological continuity. The real-valued clock space uses the relative topology inherited from real-valued càdlàg paths.

The endpoint correction is exact in the Lean statement. At the right endpoint, take $T_1=T_2=T_3=[0,1]$, $y(t)=t$, $y_n(t)=(1-1/n)t$ for $n\ge2$, and $x=1_{\{1\}}$. Then $x\circ y_n$ is zero while $(x\circ y)(1)=1$. At the left endpoint, take $T_1=T_2=[0,1]$, $T_3=[-1,2]$, $y_n=y=e$, $x=1_{[0,2]}$, and $x_n=1_{[1/n,2]}$. The outer paths converge in $J_1$ on $T_3$, but the compositions disagree at $0$. Both examples show why continuity of $x$ at the image of every included endpoint is required in the $D\times C_0$ case.

The development needs the càdlàg definition, $J_1$ metric and convergence predicates, compact restriction lemma, and the finite oscillation partition. Their definitions and lemmas are reusable for other functionals on path spaces. Contributions that prove the milestones and goal under the stated hypotheses are welcome. This mission does not formalize the Borel measurability or probability-measure machinery discussed elsewhere in Whitt's paper; Theorem 3.1 itself is a deterministic continuity claim.

Selected references

• Ward Whitt, Some Useful Functions for Functional Limit Theorems, Mathematics of Operations Research 5(1), 67–85, 1980. DOI: 10.1287/moor.5.1.67.