Functional Analysis

Completed

Analysis·Captain: wurtle

Backward intertwiners and a transitive commutantResearch Paper

Motivation

A closed subspace $\mathcal M$ of a Hilbert space $H$ is hyperinvariant for a bounded operator $S$ if $A\mathcal M\subseteq\mathcal M$ for every operator $A$ commuting with $S$ . The hyperinvariant subspace problem asks whether every bounded nonscalar operator on an infinite-dimensional separable complex Hilbert space has a nonzero proper closed hyperinvariant subspace. It is a strengthening of the invariant subspace problem, closely tied to the theory of transitive operator algebras: $S$ has no such subspace exactly when its commutant $\{S\}'$ is transitive. A related classical question asks whether every unital transitive operator algebra is strongly dense in $B(H)$ ; Arveson's density theorem gives a positive answer when the algebra contains a maximal abelian self-adjoint subalgebra.

Timeline

1967. Arveson proves that a transitive algebra containing a maximal abelian self-adjoint subalgebra is strongly dense in $B(H)$ (doi:10.1215/S0012-7094-67-03467-9).
1972. Douglas and Pearcy relate hyperinvariant subspaces to transitive algebras (doi:10.1307/mmj/1029000793).
1981–1982. Domar describes translation-invariant subspaces of weighted $\ell^p$ and $L^p$ spaces (doi:10.7146/math.scand.a-11926); Grabiner studies unicellular shifts.
1999. Atzmon and Sodin construct completely indecomposable bilateral weighted shifts with spectrum the unit circle, leaving open whether they have proper hyperinvariant subspaces (doi:10.1006/jfan.1999.3454).
2005. Dykema observes that hyperinvariant subspaces of an operator in a von Neumann algebra have projections in that algebra (doi:10.1007/s00208-005-0669-8).
2025–2026. A preprint of Kérchy and Pearcy claiming an equivalence between the invariant and hyperinvariant problems is withdrawn after a counterexample to its Theorem 3 (arXiv:2503.13005); Kérchy studies hyperinvariant subspaces of operators containing unilateral shifts (doi:10.1007/s11785-026-02038-9).

The source of this mission is an OpenAI preprint dated September 27, 2026. A companion OpenAI preprint of the same date reaches the same existence conclusion through invariant projections in an irrational-rotation factor, by a different construction.

Setting

Let $H$ be a complex Hilbert space and $B(H)$ its bounded operators. For $S\in B(H)$ :

the commutant is $\{S\}'=\{A\in B(H):AS=SA\}$ , a unital subalgebra of $B(H)$ ;
$\{S\}'$ is transitive if the only closed subspaces $\mathcal M$ with $A\mathcal M\subseteq\mathcal M$ for all $A\in\{S\}'$ are $\{0\}$ and $H$ ;
$S$ is norm-quasinilpotent if $\|S^n\|^{1/n}\to0$ ;
the strong operator topology on $B(H)$ is the topology of pointwise norm convergence: $A_\lambda\to A$ iff $A_\lambda x\to Ax$ for every $x\in H$ .

Formalization targets

Goal: Corollary 1.2

For every infinite-dimensional separable complex Hilbert space $H$ there is $S\in B(H)$ with

S\neq0,\qquad \lim_{n\to\infty}\|S^n\|^{1/n}=0,\qquad \{S\}'\ \text{transitive},\qquad \{S\}'\neq B(H),\qquad \{S\}'\ \text{strongly closed}.

The Lean statement OAI.BackwardIntertwiners.direct_algebra_corollary is open on the platform. The family statement OAI.Hyperinvariant.main_theorem asserts the same proposition and is included as a reference item.

Significance

Corollary 1.2 gives a negative answer to the hyperinvariant subspace problem on every separable infinite-dimensional Hilbert space, and its commutant is a proper, strongly closed, unital transitive algebra, so it also answers negatively whether every unital transitive operator algebra is strongly dense in $B(H)$ . The construction behind it (Theorem 1.1) is explicit: a weighted shift over the 2-adic odometer whose fibres have only coordinate-tail invariant subspaces, an explicit bound $\|S^n\|\le\exp(-10\lfloor(n+1)^2/4\rfloor)$ , and a bounded commuting operator moving those tails backward. The operator does have many ordinary invariant subspaces, so the invariant subspace problem itself is untouched.

The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.

Difficulty

Weighted shifts have rich lattices of invariant subspaces, so one must first pin down the invariant subspaces of each fibre (a quadratic weighted-translation criterion in the style of Domar) and then find enough operators in the commutant to destroy every candidate. Multiplication operators and the shift alone leave every fixed tail $L^2(X;K_{\ge h})$ invariant. The essential step is a bounded operator commuting with $S$ that moves tails backward across fibres; this requires opposite logarithmic drifts of the weights at the two ends of the bilateral sequence and one measurable normalization valid on the whole base. Arveson's theorem cannot be used, since the multiplier algebra has infinite multiplicity and is not maximal abelian.

Formalization scope

H is any type with [InnerProductSpace ℂ H] [CompleteSpace H] [SeparableSpace H] and ¬FiniteDimensional ℂ H; the claim is existential in T : H →L[ℂ] H.
commutant T is Subalgebra.centralizer ℂ {T}; TransitiveCommutant T quantifies over closed Submodules invariant under every A with A * T = T * A.
Quasinilpotence is Tendsto (fun n => ‖T ^ n‖ ^ (1 / n)) atTop (𝓝 0) (the $n=0$ term is irrelevant to the limit).
The strong operator topology is TopologicalSpace.induced from the pointwise (product) topology on functions H → H.

A complete development needs vector-valued $L^2$ spaces over the 2-adic integers with Haar measure, weighted shifts and their invariant subspaces, measurable fields of projections, and transport to an arbitrary separable Hilbert space by a unitary. Contributions formalizing Theorem 1.1 (the construction), Lemma 2.1 (weighted translation criterion), Proposition 4.3 (a bounded backward intertwiner) and Lemma 5.1 (strict descent) are welcome.

Selected references

OpenAI, Backward intertwiners and a transitive commutant, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Backward-intertwiners-and-a-transitive-commutant-September-27-2026/paper.pdf
OpenAI, Invariant-projection counterexamples for every irrational rotation, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Invariant-projection-counterexamples-for-every-irrational-rotation-September-27-2026/paper.pdf
W. B. Arveson, A density theorem for operator algebras, Duke Math. J., 1967. https://doi.org/10.1215/S0012-7094-67-03467-9
R. G. Douglas, C. Pearcy, Hyperinvariant subspaces and transitive algebras, Michigan Math. J., 1972. https://doi.org/10.1307/mmj/1029000793
Y. Domar, Translation invariant subspaces of weighted $l^p$ and $L^p$ spaces, Math. Scand., 1981. https://doi.org/10.7146/math.scand.a-11926
A. Atzmon, M. Sodin, Completely indecomposable operators and a uniqueness theorem of Cartwright–Levinson type, J. Funct. Anal., 1999. https://doi.org/10.1006/jfan.1999.3454
K. Dykema, Hyperinvariant subspaces for some B-circular operators, Math. Ann., 2005. https://doi.org/10.1007/s00208-005-0669-8
L. Kérchy, C. Pearcy, Hyperinvariant subspaces of block-triangular operators on Hilbert space, withdrawn preprint, 2025. https://arxiv.org/abs/2503.13005

23 thms2 active usersReviewed

Completed

Group Theory Harmonic Analysis·Captain: wurtle

Unitarizability implies amenability for discrete groupsResearch Paper

Motivation

A representation $\pi$ of a group $G$ by bounded invertible operators on a Hilbert space is uniformly bounded if $\sup_g\|\pi(g)\|<\infty$ , and unitarizable if after a change of inner product it becomes unitary, i.e. some bounded invertible $S$ makes every $S\pi(g)S^{-1}$ unitary. Unitary representations are the ones harmonic analysis knows how to decompose, so it matters which groups have only unitarizable uniformly bounded representations. Day and Dixmier showed in 1950 that every amenable group (one with an invariant mean) has this property, and Dixmier asked whether the converse holds. Dixmier's unitarizability problem has driven work in operator algebras, $\ell^2$ -invariants and measured group theory for seven decades.

Timeline

1947. Sz.-Nagy proves that an invertible operator with uniformly bounded powers is similar to a unitary.
1950. Day and Dixmier prove that amenable groups are unitarizable; Dixmier asks whether the converse holds (doi:10.2307/1990358).
1955. Ehrenpreis and Mautner give nonunitarizable uniformly bounded representations of $\mathrm{SL}_2(\mathbb R)$ (doi:10.1073/pnas.41.4.231); Følner gives his finite-set criterion for amenability (doi:10.7146/math.scand.a-10442).
1986. Pytlik and Szwarc construct explicit nonunitarizable families for free groups, settling all groups containing $F_2$ (doi:10.1007/BF02392596).
1998. Pisier characterizes amenability by a quantitative similarity bound with exponent $<3$ (The similarity degree of an operator algebra, Algebra i Analiz, 1998).
2009. Epstein and Monod use invariant random forests to prove nonunitarizability for residually finite groups with positive first $\ell^2$ -Betti number (doi:10.1093/imrn/rnp090); Osin obtains nonunitarizable groups without free subgroups.
2010. Monod and Ozawa prove that the wreath products $A\wr G$ with $A$ infinite abelian are unitarizable exactly when $G$ is amenable (doi:10.1016/j.jfa.2009.06.029), using the Gaboriau–Lyons theorem (doi:10.1007/s00222-009-0187-5).
2018–2025. Gerasimova, Gruber, Monod and Thom relate unitarizability to Cheeger constants (doi:10.1016/j.jfa.2019.108457); Alpeev and Vergara obtain further cases.

The source of this mission, an OpenAI preprint dated September 23, 2026, answers Dixmier's question affirmatively for all discrete groups.

Setting

Let $G$ be a discrete group. $G$ is amenable if there is a linear functional $m$ on the bounded functions $G\to\mathbb C$ with $m(1)=1$ , $m(f)\ge0$ for $f\ge0$ , and $m(L_gf)=m(f)$ , where $(L_gf)(x)=f(g^{-1}x)$ .

A representation is a homomorphism $\pi:G\to\mathcal B(\mathcal K)$ into bounded operators on a complex Hilbert space $\mathcal K$ (each $\pi(g)$ is then invertible). It is similar to a unitary representation if there is a bounded invertible $S$ with $S\pi(g)S^{-1}$ unitary for every $g$ . $G$ is unitarizable if every uniformly bounded representation on every complex Hilbert space is similar to a unitary representation; the similarity may depend on the representation.

Formalization targets

Milestone: countable case

Every countable nonamenable $G$ has a representation on a separable Hilbert space with $\sup_g\|\pi(g)\|\le101$ that is not similar to a unitary representation.

Goal: Theorem 1.1

G\ \text{amenable}\iff G\ \text{unitarizable},

and for nonamenable $G$ and every $\varepsilon>0$ there is $\pi$ with $\sup_g\|\pi(g)\|\le1+\varepsilon$ not similar to a unitary representation, on a separable space when $G$ is countable. The Lean statement OAI.Dixmier.current_main_theorem is open on the platform.

Significance

Theorem 1.1 characterizes amenability of discrete groups by a purely Hilbert-space property, without any quantitative bound on similarities, and shows that nonunitarizable representations can be chosen with uniform bound arbitrarily close to $1$ . Earlier results produced witnesses for groups with free subgroups, for residually finite groups with positive $\ell^2$ -Betti number, or for wreath-product extensions of $G$ ; the theorem gives a witness for every nonamenable $G$ itself. The paper also derives a consequence for group C $^*$ -algebras using a companion similarity result.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. The amenable direction (Day–Dixmier averaging) is classical and a natural first formalization step; the converse needs the paper's new operator construction.

Difficulty

A witness must be one representation for which no similarity exists, with no a priori control of the condition number of a putative unitarizer; quantitative criteria such as Pisier's do not apply. Nonamenable groups need not contain free subgroups and need not be residually finite, so the earlier free-group, random-forest and $\ell^2$ -Betti routes do not cover them. The paper builds bounded operator cocycles with no bounded implementer, which requires operators whose conjugation differences under translation are uniformly bounded while their distance from the translation commutant tends to infinity.

Formalization scope

Amenability is stated for G with the discrete topology, using G →ᵇ ℂ for $\ell^\infty(G)$ ; positivity is required on functions with nonnegative real values.
Representations are monoid homomorphisms G →* (H →L[ℂ] H) with [InnerProductSpace ℂ H] [CompleteSpace H]; SimilarToUnitary π asks for S : H ≃L[ℂ] H with $\|S\pi(g)S^{-1}x\|=\|x\|$ for all $g,x$ .
Unitarizability quantifies over Hilbert spaces in universe max u v, and the witness is built there; since the theorem holds for every v, this covers all Hilbert spaces.
Separability of the witness is required only for countable G, as in the paper.

A complete development needs bounded operator cocycles and triangular representations, Hilbert direct sums, Hilbert–Schmidt estimates, Følner's criterion, induction of representations from subgroups, and invariant means. Contributions formalizing the Day–Dixmier direction, Proposition 2.2 (direct-sum obstruction) and Lemma 5.1 (induction from a subgroup) are welcome.

Selected references

OpenAI, Unitarizability implies amenability for discrete groups, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Unitarizability-Implies-Amenability-for-Countable-Groups-September-23-2026/paper.pdf
M. M. Day, Means for the bounded functions and ergodicity of the bounded representations of semi-groups, Trans. Amer. Math. Soc., 1950. https://doi.org/10.2307/1990358
J. Dixmier, Les moyennes invariantes dans les semi-groupes et leurs applications, Acta Sci. Math. (Szeged), 1950.
G. Pisier, Are unitarizable groups amenable?, preprint, 2004. https://arxiv.org/abs/math/0405282
I. Epstein, N. Monod, Nonunitarizable representations and random forests, IMRN, 2009. https://doi.org/10.1093/imrn/rnp090
N. Monod, N. Ozawa, The Dixmier problem, lamplighters and Burnside groups, J. Funct. Anal., 2010. https://doi.org/10.1016/j.jfa.2009.06.029
D. Gaboriau, R. Lyons, A measurable-group-theoretic solution to von Neumann's problem, Invent. Math., 2009. https://doi.org/10.1007/s00222-009-0187-5
T. Pytlik, R. Szwarc, An analytic family of uniformly bounded representations of free groups, Acta Math., 1986. https://doi.org/10.1007/BF02392596
M. Gerasimova, D. Gruber, N. Monod, A. Thom, Asymptotics of Cheeger constants and unitarisability of groups, J. Funct. Anal., 2020. https://doi.org/10.1016/j.jfa.2019.108457

30 thms2 active usersReviewed

Completed

Group Theory·Captain: wurtle

Thompson's group F is nonamenableResearch Paper

Motivation

Thompson's group $F$ consists of the increasing piecewise linear homeomorphisms of $[0,1]$ with finitely many pieces, dyadic rational breakpoints, and slopes that are integer powers of $2$ . It is finitely presented, has strong topological finiteness properties, and appears across group theory, dynamics and logic. Whether $F$ is amenable, i.e. whether its bounded functions admit a translation-invariant mean, is one of the best-known open questions about a single explicit group. It is a natural test case because the two classical routes to deciding amenability both fail: $F$ contains no nonabelian free subgroup (Brin–Squier 1985), so the free-subgroup obstruction is unavailable, yet $F$ is not elementary amenable (Cannon–Floyd–Parry 1996, Theorem 4.10). Geoghegan conjectured in 1979 that $F$ is nonamenable. The problem has attracted claimed resolutions in both directions, several later withdrawn or found to contain errors.

This mission asks for a formal proof of nonamenability as stated in an OpenAI preprint dated September 23, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

1929–1957 — Von Neumann and Day develop invariant means and amenability (Fund. Math. 1929; Illinois J. Math. 1957); Følner's criterion (Math. Scand. 1955).
1965–1973 — Thompson introduces $F$ ; an early published construction is McKenzie–Thompson (1973).
1979 — Geoghegan conjectures that $F$ is nonamenable (recorded in Cannon–Floyd–Parry 1996, p. 227).
1984–1985 — Brown and Geoghegan: $F$ is $\mathrm{FP}_\infty$ (Invent. Math. 1984); Brin and Squier: no nonabelian free subgroups (Invent. Math. 1985).
2009–2013 — Shavgulidze's amenability claim (arXiv:0906.0107) and Moore's identification of its errors (arXiv:1102.0747); Moore's tower lower bounds for Følner functions (GGD 2013) and Ramsey characterization of amenability (Fund. Math. 2013); Moore's later amenability manuscript is withdrawn (arXiv:1209.2063).
2017 — Haagerup and Olesen: $C^*$ -simplicity of $T$ would imply nonamenability of $F$ (JFA 2017).
2021–2026 — Akhmedov's nonamenability claim via height functions (arXiv:1310.4395v3); Guba's density estimates (J. Comb. Algebra 2025; J. Algebra 2026).

Setting

A homeomorphism $f$ of $[0,1]$ is a dyadic PL map if there are dyadic rationals $0=x_0<x_1<\dots<x_k=1$ and integers $e_i$ such that on each $[x_{i-1},x_i]$ , $f(x)=f(x_{i-1})+2^{e_i}(x-x_{i-1})$ . The group $F$ is the set of increasing dyadic PL homeomorphisms of $[0,1]$ , with multiplication $hg=h\circ g$ , regarded as a discrete group. Let $\ell^\infty(F;\mathbb R)$ be the bounded real functions on $F$ . A left-invariant mean is a linear functional $M:\ell^\infty(F;\mathbb R)\to\mathbb R$ with $M(\mathbf 1)=1$ , $M(\varphi)\ge0$ whenever $\varphi\ge0$ , and $M(g\mapsto\varphi(hg))=M(\varphi)$ for every $h\in F$ . $F$ is amenable if such a mean exists.

Formalization targets

Goal: Theorem 1.1 (p. 1)

Thompson's group $F$ is not amenable: there is no positive, normalized, left-invariant mean on $\ell^\infty(F;\mathbb R)$ .

Significance

The result itself. It settles Geoghegan's conjecture and the amenability problem for $F$ . Because $F$ has no free subgroups, $F$ becomes a finitely presented, torsion-free example of a nonamenable group without free subgroups. Through companion results the preprint derives that $F$ has uniformly bounded representations that are not unitarizable (Corollary 3.1, p. 7) and that Bernoulli percolation on every Cayley graph of $F$ has a nonuniqueness phase (Corollary 3.2, p. 8). The proof is short (Section 2) and uses an infinite-dimensional fixed-point phenomenon: the Benyamini–Sternfeld theorem that the unit ball of an infinite-dimensional Hilbert space admits a Lipschitz self-map moving every point by at least a fixed $\delta>0$ (Lemma 1.2, p. 2; Proc. AMS 1983).

Formalizing it. Given the length of the published argument, this is a realistic target for a complete formal proof of a result that had been open for over forty years. It needs the dyadic-partition model of $F$ , the Følner criterion (forward direction), and a Lipschitz map on a Hilbert ball with no approximate fixed points (Appendix A of the preprint constructs one on $L^2([0,1];\mathbb R^2)$ with $\delta=1/2$ ). The Følner direction from invariant means to Følner sets is reusable infrastructure for amenability in Mathlib.

Difficulty

Neither standard obstruction applies: there is no free subgroup to produce a paradoxical decomposition, and no structural closure property shows amenability. Følner sets, if they existed, would have to grow extremely fast (Moore's tower bounds), so explicit counting is ineffective. The preprint's argument converts approximate invariance of a finite set $A\subset F$ into an approximate fixed point of a Lipschitz map on a Hilbert ball, via recursively defined Hilbert-valued colours of dyadic partitions. The delicate points are exact covariance of normalized restrictions under the group action (equation (2.2), p. 4) and controlling the diagonal and nested pairs in the correlation expansion, which yields a uniform lower bound on the relative boundary of every finite set (Proposition 2.3, p. 5).

Formalization scope

UnitInterval is Set.Icc (0:ℝ) 1; an element of F is a homeomorphism of it that is StrictMono and has a DyadicPLWitness: finitely many strictly increasing dyadic knots from $0$ to $1$ and integer exponents with the affine formula on each piece.
The goal asserts that some group structure on F exists whose multiplication is composition ((h * g) x = h (g x)); since multiplication is fixed, this structure is unique.
InvariantMean F is a real-linear functional on lp (fun _ : F => ℝ) ∞ that is positive, sends the constant $1$ to $1$ , and is invariant under leftPull h, $\varphi\mapsto(g\mapsto\varphi(hg))$ ; the goal is ¬ Nonempty (InvariantMean F).
No generating set, Følner constant or boundary bound is fixed in the statement, so the goal is stable under improved constants.

Selected references

OpenAI, Thompson's group F is nonamenable, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Thompsons-group-F-is-nonamenable-September-23-2026/paper.pdf
J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, Enseign. Math. (2) 42 (1996), 215–256. https://www.imo.universite-paris-saclay.fr/~emmanuel.breuillard/Cannon.pdf
M. G. Brin, C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Invent. Math. 79 (1985), 485–498. https://doi.org/10.1007/BF01388519
K. S. Brown, R. Geoghegan, An infinite-dimensional torsion-free $\mathrm{FP}_\infty$ group, Invent. Math. 77 (1984), 367–381. https://doi.org/10.1007/BF01388451
Y. Benyamini, Y. Sternfeld, Spheres in infinite-dimensional normed spaces are Lipschitz contractible, Proc. Amer. Math. Soc. 88 (1983), 439–445. https://doi.org/10.1090/S0002-9939-1983-0699410-7
E. Følner, On groups with full Banach mean value, Math. Scand. 3 (1955), 243–254. https://doi.org/10.7146/math.scand.a-10442
J. T. Moore, Amenability and Ramsey theory, Fund. Math. 220 (2013), 263–280. https://doi.org/10.4064/fm220-3-6
J. T. Moore, Fast growth in the Følner function for Thompson's group F, Groups Geom. Dyn. 7 (2013), 633–651. https://doi.org/10.4171/GGD/201
U. Haagerup, K. K. Olesen, Non-inner amenability of the Thompson groups T and V, J. Funct. Anal. 272 (2017), 4838–4852. https://doi.org/10.1016/j.jfa.2017.02.003
M. M. Day, Amenable semigroups, Illinois J. Math. 1 (1957), 509–544. https://doi.org/10.1215/ijm/1255380675

7 thms2 active usersReviewed

Completed

Combinatorics Theoretical Computer Science·Captain: wurtle

Finite-Circle Obstructions, Binary Codes, and Histogram Embeddings for Edit DistanceResearch Paper

Motivation

Edit distance $\mathrm{ED}(x,y)$ , the least number of single-symbol insertions, deletions and substitutions turning $x$ into $y$ , is the standard distance on strings. Embedding strings into $\ell_1$ with small distortion would make edit distance amenable to the fast nearest-neighbour and sketching tools available for $\ell_1$ , so the least achievable distortion is a central quantity in metric embedding theory. A single insertion shifts every later symbol, yet cyclically shifting a word costs only two edits; this tension between position and alignment is what makes edit distance hard to embed.

This preprint gives two independent constructions of binary word sets whose least $\ell_1$ distortion is $\exp(\Omega(\sqrt{\log d\log\log d}))$ , two binary coding arguments that transfer large-alphabet constructions to binary, and a complete histogram embedding attaining the matching upper scale. Together they determine the exponential scale of the distortion.

Background

1966, 1974. Levenshtein introduces insertion/deletion codes; Wagner and Fischer describe alignments by increasing traces.
1995. Linial, London and Rabinovich develop finite metric embeddings into $\ell_1$ .
1999. Schulman and Zuckerman construct asymptotically good codes for insertions and deletions.
2003. Andoni, Deza, Gupta, Indyk and Raskhodnikova give binary sets with $\ell_1$ distortion approaching $3/2$ .
2006. Khot and Naor prove a $(\log d)^{1/2 - o(1)}$ lower bound by Fourier analysis of cuts.
2007. Ostrovsky and Rabani prove the upper bound $\exp(O(\sqrt{\log d\log\log d}))$ for fixed-length binary strings.
2009. Krauthgamer and Rabani prove an $\Omega(\log d)$ lower bound.
2026. The OpenAI preprint Finite-Circle Obstructions, Binary Codes, and Histogram Embeddings for Edit Distance (dated September 27, 2026), a companion to Edit Distance in $\ell_1$ : Matching Bounds up to Constants in the Exponent, proves the results below. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

For a finite alphabet $\Sigma$ with $|\Sigma| \ge 2$ and an integer $d \ge 1$ , let $\Sigma^{\le d}$ be the words of length at most $d$ , including the empty word. For an injective $f : \Sigma^{\le d} \to \ell_1$ ,

\mathrm{dist}(f) = \Big(\max_{x\ne y}\frac{\|f(x)-f(y)\|_1}{\mathrm{ED}(x,y)}\Big)\Big(\max_{x\ne y}\frac{\mathrm{ED}(x,y)}{\|f(x)-f(y)\|_1}\Big), \qquad E_\Sigma(d) = \inf_f \mathrm{dist}(f).

The longest common subsequence $\mathrm{LCS}(x,y)$ and the deficit $r_L(x,y) = L - \mathrm{LCS}(x,y)$ for words of length $L$ are used in the coding results. A binary substitution $c : \Sigma \to \{0,1\}^w$ replaces each letter by a codeword.

In Lean (OAI.FiniteCircle), editDistance is the least script length, lcs and deficit are as above, optimalDistortion is the infimum of distortion over injective maps into lp (fun _ : ℕ => ℝ) 1, E α d is the least distortion of words of length at most $d$ , and maskWord, excludedWord are the two finite-circle constructions with prime-period parameters.

Formalization targets

Goal: `finiteCircle_fullMain`

The conjunction of the paper's main statements, with common absolute constants:

Theorem 1.1. For $d \ge d_0$ and every finite $\Sigma$ with $|\Sigma| \ge 2$ ,

\exp\big(c\sqrt{\log d\log\log d}\big) \le E_\Sigma(d) \le \exp\big(C\sqrt{\log d\log\log d}\big),

and the same bounds for $\sup_{|\Sigma| \ge 2} E_\Sigma(d)$ .

Lower constructions (Sections 5–7): for each $d \ge d_0$ , both the mask construction and the excluded-prime construction, encoded in binary, give a set of words of one common length $n \le d$ with least distortion at least $\exp(c\sqrt{\log d\log\log d})$ .
Theorem 4.1 (two binary substitutions): for every alphabet of $A \ge 2$ letters there are codes $c : \Sigma \to \{0,1\}^w$ with $w = O(\log 2A)$ and $a\,w\,r_L(x,y) \le r_{wL}(c(x),c(y)) \le w\,r_L(x,y)$ for equal-length words, $\mathrm{ED}(c(x),c(y)) \le w\,\mathrm{ED}(x,y)$ , plus the local separation property each construction needs.
Theorem 8.1 (uniform upper bound): a deterministic finite-dimensional map $F$ with $\mathrm{ED}(x,y) \le \|F(x)-F(y)\|_1 \le \exp(C\sqrt{\log d\log\log d})\,\mathrm{ED}(x,y)$ .

Significance

The result. The lower bounds reach the Ostrovsky–Rabani scale, so the order of $\log E_\Sigma(d)$ is $\sqrt{\log d\log\log d}$ ; this improves the previous $\Omega(\log d)$ lower bound to $\exp(\Omega(\sqrt{\log d\log\log d}))$ . The histogram embedding gives an explicit, alphabet-uniform upper bound including all shorter words.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. Unlike the companion paper, the upper bound here is proved in full (Section 8) rather than imported, so the goal is self-contained relative to the preprint. The edit-distance and distortion definitions are reusable across the edit-distance missions.

Difficulty

Lower bounds for edit distance must control every increasing matching of the two words, including matchings crossing the row boundaries used to construct them. A cheap translation of phases moves row lists at low edit cost, while a simultaneous half-turn at every leaf must be expensive; proving the latter for arbitrary alignments, and then showing that every $\ell_1$ image must distort one of these comparisons, requires combining a combinatorial separation estimate with a Fourier argument on the finite phase space that forces large total frequency.

Formalization scope

Words are List α with Fintype α; the domain $\Sigma^{\le d}$ is a subtype by length; the empty word is included.
distortion uses sSup over finite sets of ratios; optimalDistortion is sInf over injective maps into $\ell_1(\mathbb N)$ ; exponentScale d = sqrt(log d · log log d) with natural logarithms.
The lower witnesses fix the paper's constructions (prime assignments MaskPrimes, ExcludedPrimes, depth parameters) and require a common positive length $n \le d$ .
UniformUpper asks for a map into Fin M → ℝ with the $\ell_1$ norm written as a finite sum.

The goal is not vacuous: a set with one element would have least distortion $0$ , so witnesses must be nontrivial, and both bounds are required uniformly.

Needed infrastructure: LCS and alignment combinatorics, cut decompositions of finite $\ell_1$ metrics, Fourier analysis on finite cyclic groups, prime counting estimates, and random partition arguments for the upper bound. Contributions toward any component are welcome.

Selected references

OpenAI, Finite-Circle Obstructions, Binary Codes, and Histogram Embeddings for Edit Distance, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Finite-Circle-Obstructions-Binary-Codes-and-Histogram-Embeddings-for-Edit-Distance-September-27-2026/paper.pdf
OpenAI, Edit Distance in $\ell_1$ : Matching Bounds up to Constants in the Exponent, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/main/preprints/Edit-Distance-in-l1-Matching-Bounds-up-to-Constants-in-the-Exponent-September-27-2026/paper.pdf
R. Ostrovsky, Y. Rabani, Low distortion embeddings for edit distance, J. ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284322
R. Krauthgamer, Y. Rabani, Improved lower bounds for embeddings into $L_1$ , SIAM J. Comput. 38(6), 2009.
S. Khot, A. Naor, Nonembeddability theorems via Fourier analysis, Math. Ann. 334(4), 2006. https://doi.org/10.1007/s00208-005-0745-0
A. Andoni, M. Deza, A. Gupta, P. Indyk, S. Raskhodnikova, Lower bounds for embedding edit distance into normed spaces, SODA 2003.
N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2), 1995. https://doi.org/10.1007/BF01200757
L. J. Schulman, D. Zuckerman, Asymptotically good codes correcting insertions, deletions, and transpositions, IEEE Trans. Inform. Theory 45(7), 1999. https://doi.org/10.1109/18.796406
V. I. Levenshtein, Binary codes capable of correcting deletions, insertions, and reversals, Soviet Physics Doklady 10(8), 1966.
R. A. Wagner, M. J. Fischer, The string-to-string correction problem, J. ACM 21(1), 1974. https://doi.org/10.1145/321796.321811

54 thms2 active usersReviewed

Completed

Analysis Discrete Geometry·Captain: wurtle

A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embeddingResearch Paper

Motivation

A metric space is doubling if every ball can be covered by a bounded number of balls of half the radius. Every subset of a finite-dimensional Euclidean space is doubling, so doubling is a necessary condition for a metric space to embed bi-Lipschitzly into some $\mathbb R^k$ . Whether it is also sufficient, for subsets of Hilbert space, is the Lang–Plaut problem. It sits at the meeting point of metric geometry and algorithm design: doubling is a standard notion of "intrinsic dimension" for data, and a positive answer would mean that intrinsically low-dimensional Euclidean data can always be represented in a bounded number of coordinates with bounded distortion.

Timeline

1983. Assouad proves that every doubling metric space embeds bi-Lipschitzly into some $\mathbb R^k$ after snowflaking, i.e. after replacing the distance $d$ by $d^\alpha$ with $0<\alpha<1$ (doi:10.24033/bsmf.1997).
2001. Lang and Plaut ask whether every doubling subset of Hilbert space admits a bi-Lipschitz embedding into a finite-dimensional Euclidean space (Question 2.4) (doi:10.1023/A:1012093209450).
2003. Gupta, Krauthgamer and Lee independently pose the question for algorithmic dimension reduction (doi:10.1109/SFCS.2003.1238226).
2012. Naor and Neiman bound the target dimension in Assouad's theorem independently of the snowflake exponent near $1$ (doi:10.4171/RMI/706).
2014. Lafforgue and Naor construct, for $p>2$ , a doubling subset of $L_p$ with no bi-Lipschitz embedding into any $\mathbb R^k$ (doi:10.1007/s10711-013-9924-4).
2015. Bartal, Gottlieb and Neiman obtain obstructions for doubling subsets of $\ell_p$ via Laakso-type configurations (doi:10.1137/140977655); Gottlieb and Krauthgamer embed snowflakes of finite Hilbert subsets with distortion close to one (doi:10.1007/s00454-015-9707-9).
2017. Schioppa announces a negative answer for $\ell_2$ and later withdraws the preprint (arXiv:1703.10265).
2021. Baudier, Świȩcicki and Swift give an elementary proof of the fixed-set theorem for $\ell_q$ , $q>2$ (doi:10.1016/j.jmaa.2021.125407).

The Hilbert case ( $p=2$ ) remained open. The source of this mission, an OpenAI preprint dated September 25, 2026, claims a negative answer.

Setting

A metric space $(X,d)$ is doubling with constant at most $\lambda$ if for every $x\in X$ and $r>0$ , the ball of radius $r$ about $x$ is covered by at most $\lambda$ balls of radius $r/2$ with centers in $X$ . A map $f:X\to\mathbb R^k$ is a bi-Lipschitz embedding with distortion at most $D$ if some scale $a>0$ satisfies

a\,d(x,y)\ \le\ \|f(x)-f(y)\|\ \le\ D\,a\,d(x,y)\qquad(x,y\in X).

Real $\ell_2$ is the Hilbert space of square-summable real sequences indexed by $\mathbb N$ ; subsets carry the induced distance.

Formalization targets

Corollary 6 (milestone)

There is a universal $\Lambda$ such that every infinite-dimensional real Banach space $B$ contains a compact set $K_B$ with doubling constant at most $\Lambda$ that admits no bi-Lipschitz embedding into any finite-dimensional real normed space at any finite distortion.

Goal: Theorem 1

\exists\, S\subset\ell_2:\quad S\ \text{is doubling with constant}\ \le 76800,\ \text{and}\ \forall k\ge1,\ S\ \text{admits no bi-Lipschitz embedding into}\ \mathbb R^k.

The set is fixed once, independently of $k$ and of the distortion. The Lean statement OAI.DoublingHilbert.main is open on the platform. The constant $76800=300\cdot16^2$ comes from the paper's covering count; any finite universal constant would answer the Lang–Plaut problem, but the Lean goal records the paper's value.

Significance

The theorem answers the Lang–Plaut problem negatively: there is no function of the doubling constant alone that bounds both the dimension and the distortion for doubling subsets of Hilbert space. It extends the Lafforgue–Naor and Bartal–Gottlieb–Neiman obstructions from $p>2$ to the Hilbert case, which is the case of most interest for applications. By Gaussian isometric embedding the same metric space sits in every $L_p[0,1]$ , $1\le p<\infty$ (Corollary 5), and by Dvoretzky's theorem a compact version sits in every infinite-dimensional Banach space (Corollary 6). Assouad's theorem shows that any snowflake of the set does embed, so the obstruction is specific to the original distance.

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A previous announced proof of this statement (Schioppa, 2017) was withdrawn, which makes an independent formal verification particularly informative.

Difficulty

Doubling gives covering control at every scale, and Assouad's theorem shows that any loss in the exponent of the metric removes the obstruction, so a counterexample must be sharp at the level of exact Lipschitz bounds. The $p>2$ constructions rely on uniform convexity estimates of $L_p$ that degenerate at $p=2$ , and Hilbert space has the most symmetric geometry available, so the standard Laakso and diamond-type obstructions do not transfer. The set must also be chosen before the target dimension and distortion, so a single set has to defeat every $k$ and every $D$ simultaneously.

Formalization scope

The ambient space is RealL2 := lp (fun _ : ℕ => ℝ) 2; $S$ is a Set RealL2 with the subspace metric.
DoublingAtMost S bound: for each $x\in S$ and $r>0$ there is a Finset of at most bound centers in $S$ such that every $y\in S$ with $d(y,x)<r$ satisfies $d(y,c)<r/2$ for some center (open balls; centers in $S$ ).
AdmitsBiLipschitzEmbedding S k: there are $f:S\to$ EuclideanSpace ℝ (Fin k), $a>0$ and $D\ge1$ with the two-sided bound above.
For Corollary 6, CompactBanach.main quantifies over all complete real normed spaces that are not finite-dimensional and all finite-dimensional real normed targets, with the doubling constant $\Lambda$ chosen before $B$ .

A complete development needs Hilbert direct sums, the explicit strip-colored set, covering estimates, a.e. differentiability of Lipschitz maps on open subsets of $\mathbb R^2$ (Rademacher), and a Euclidean packing bound. Rademacher's theorem and packing estimates are reusable well beyond this mission. Contributions formalizing Proposition 2 (the doubling bound) are a natural first step.

Selected references

OpenAI, A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embedding, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-doubling-Hilbert-subset-with-no-finite-dimensional-bi-Lipschitz-embedding-September-25-2026/main.pdf
U. Lang, C. Plaut, Bilipschitz embeddings of metric spaces into space forms, Geom. Dedicata, 2001. https://doi.org/10.1023/A:1012093209450
P. Assouad, Plongements lipschitziens dans $\mathbb R^n$ , Bull. Soc. Math. France, 1983. https://doi.org/10.24033/bsmf.1997
A. Gupta, R. Krauthgamer, J. R. Lee, Bounded geometries, fractals, and low-distortion embeddings, FOCS 2003. https://doi.org/10.1109/SFCS.2003.1238226
A. Naor, O. Neiman, Assouad's theorem with dimension independent of the snowflaking, Rev. Mat. Iberoam., 2012. https://doi.org/10.4171/RMI/706
V. Lafforgue, A. Naor, A doubling subset of $L_p$ for $p>2$ that is inherently infinite dimensional, Geom. Dedicata, 2014. https://doi.org/10.1007/s10711-013-9924-4
Y. Bartal, L.-A. Gottlieb, O. Neiman, On the impossibility of dimension reduction for doubling subsets of $\ell_p$ , SIAM J. Discrete Math., 2015. https://doi.org/10.1137/140977655
F. P. Baudier, K. Świȩcicki, A. Swift, No dimension reduction for doubling subsets of $\ell_q$ when $q>2$ revisited, J. Math. Anal. Appl., 2021. https://doi.org/10.1016/j.jmaa.2021.125407

25 thms2 active usersReviewed

Completed

Discrete Geometry Probability·Captain: wurtle

Subpolynomial dimension reduction in LpResearch Paper

Motivation

The Johnson–Lindenstrauss lemma (1984) says that any $n$ points of a Hilbert space can be placed in $O_D(\log n)$ -dimensional Euclidean space with distortion at most any prescribed $D>1$ . This dimension reduction is used throughout analysis, geometry and algorithm design. Johnson and Lindenstrauss also asked what analogues hold in other Banach spaces. For the spaces $L_p$ with $p\ne2$ the question splits into several versions: whether one needs the map to be linear, whether one discretizes a whole subspace or only a finite set, and whether the target is a coordinate space $\ell_p^d$ with the same exponent. This mission concerns the finite-set, coordinate-target, nonlinear version: how many coordinates $d$ are needed so that every $n$ -point subset of $L_p$ embeds into $\ell_p^d$ with distortion at most $D$ ?

Timeline

1958. Lamperti characterizes equality in the $p$ -parallelogram inequality, the tool behind exact-embedding lower bounds (doi:10.2140/pjm.1958.8.459).
1984. Johnson and Lindenstrauss prove the Hilbert-space lemma and ask for analogues in other spaces (doi:10.1090/conm/026/737400).
1987 and 2011. Schechtman's finite-set estimates for $p<2$ improve from $O_D(n\log n)$ coordinates to $O_{p,D}(n)$ (numdam, arXiv:1110.2148).
1989 and 1995. Bourgain–Lindenstrauss–Milman and Talagrand discretize whole $r$ -dimensional subspaces of $L_p$ by linear maps (doi:10.1007/BF02392835, doi:10.1007/978-3-0348-9090-8_26); applied to $n$ points this gives dimension polynomial in $n$ .
1990. Ball proves that exact embeddings need at most $\binom n2$ coordinates and that quadratic order is necessary for $1\le p<2$ (doi:10.1016/S0195-6698(13)80131-X).
2004–2005. Brinkman–Charikar and Lee–Naor show that dimension reduction fails in $\ell_1$ even for nonlinear maps (doi:10.1145/1089023.1089026, doi:10.1007/s00039-004-0473-8); Lee–Mendel–Naor show that linear maps can require dimension linear in $n$ when $p\ne2$ (doi:10.1016/j.ejc.2004.07.002).
2018. Naor surveys metric dimension reduction and the coordinate-target question (arXiv:1809.02376).
2026. Naor and Ren show that for $p>2$ the dimension cannot be $O_{p,D}(\log n)$ (arXiv:2609.01079).

The source of this mission, an OpenAI preprint dated September 23, 2026, claims that for every fixed $1<p<\infty$ , $p\ne2$ , and $D>1$ the dimension is $n^{o(1)}$ .

Setting

All spaces are real. Fix $1<p<\infty$ , an integer $n\ge2$ and $D\ge1$ . Let $d_p(n,D)$ be the least integer $d$ such that for every measure space and every $n$ distinct points $x_1,\dots,x_n\in L_p$ there are $y_1,\dots,y_n\in\mathbb R^d$ and a scale $s>0$ with

s\,\|x_i-x_j\|_p\ \le\ \|y_i-y_j\|_{\ell_p^d}\ \le\ D\,s\,\|x_i-x_j\|_p\qquad(1\le i,j\le n).

The map $x_i\mapsto y_i$ is arbitrary, not required to be linear. Put

\gamma(p)=\begin{cases}2-p,&1<p<2,\\ 1-2/p,&2<p<\infty.\end{cases}

Formalization targets

Goal: Theorem 1.1

For fixed $1<p<\infty$ , $p\ne2$ :

\forall D>1\ \exists C_{p,D}\ \forall n\ge2:\quad \frac{\log n}{\log(1+2D)}\ \le\ d_p(n,D)\ \le\ \exp\bigl(C_{p,D}(\log n)^{\gamma(p)}\bigr);

\Bigl\lfloor\tfrac{n-1}{4}\Bigr\rfloor^2\ \le\ d_p(n,1)\ \le\ \binom n2\qquad(n\ge9);

\lim_{n\to\infty}\frac{\log d_p(n,D)}{\log n}=\begin{cases}0,&D>1,\\ 2,&D=1.\end{cases}

Since $\gamma(p)<1$ , the upper bound is $n^{o(1)}$ . The Lean statement OAI.SubpolynomialLp.source_main is open on the platform.

Significance

For $p\ne2$ the best previous finite-set bounds were polynomial in $n$ (linear for $p<2$ ), and for $p>2$ logarithmic dimension is impossible. The theorem places $d_p(n,D)$ at $n^{o(1)}$ for every fixed $D>1$ , in contrast with exact embeddings, where the dimension is of order $n^2$ . Thus the exponent $\lim \log d_p/\log n$ jumps from $2$ at $D=1$ to $0$ for every $D>1$ . The upper exponent and the logarithmic lower bound are not claimed to be optimal. The theorem is existential; no embedding algorithm is asserted.

The result is claimed in an OpenAI preprint and has not been peer reviewed; no machine-checked proof exists. A formal proof would include a probabilistic construction (stable laws, Poisson sampling, Rosenthal-type moment inequalities), an electrical-flow localization estimate, and a convex-separation argument.

Difficulty

Linear maps cannot work: fixed-distortion linear maps on some $L_p$ configurations need dimension proportional to $n$ when $p\ne2$ . Subspace discretization theorems apply to the span of the points, which has dimension up to $n-1$ , so they also give only polynomial bounds. The Johnson–Lindenstrauss approach relies on Gaussian rotation invariance, which has no analogue in $L_p$ . One needs a single random scalar map whose increments have nearly equal normalized $p$ -th moments simultaneously for all $\binom n2$ pairs, with relative (not additive) error control.

Formalization scope

coordinateDistance p y z is $(\sum_a |y_a-z_a|^p)^{1/p}$ on Fin d → ℝ.
GoodDimension p n D d quantifies over every measure space (Ω, mΩ, μ) in a fixed universe and every injective x : Fin n → Lp ℝ (ENNReal.ofReal p) μ; the target is Fin d → ℝ with the $\ell_p$ distance and a scale $s>0$ .
dimension p n D is the sInf of the good dimensions in ℕ. The goal also asserts that this infimum is good, so the default value of sInf ∅ cannot make the bounds trivial.
gamma p is as above; the exact-embedding lower bound uses natural-number division, i.e. the floor.
The limit is a Tendsto statement along n : ℕ for each $D\ge1$ .

A complete development needs $L_p$ spaces, $p$ -stable random variables, Poisson sampling and moment inequalities, effective resistance and electrical flows on complete graphs, and Carathéodory's theorem for the exact-embedding upper bound. Contributions formalizing the exact-embedding bounds (Ball's upper bound and the antipodal lower bound) and the weighted moment criterion are welcome.

Selected references

OpenAI, Subpolynomial dimension reduction in $L_p$ , preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Subpolynomial-dimension-reduction-in-Lp-September-23-2026/paper.pdf
W. B. Johnson, J. Lindenstrauss, Extensions of Lipschitz mappings into a Hilbert space, Contemp. Math. 26, 1984. https://doi.org/10.1090/conm/026/737400
K. Ball, Isometric embedding in $l_p$ -spaces, European J. Combin., 1990. https://doi.org/10.1016/S0195-6698(13)80131-X
G. Schechtman, Dimension reduction in $L_p$ , $0<p<2$ , preprint, 2011. https://arxiv.org/abs/1110.2148
B. Brinkman, M. Charikar, On the impossibility of dimension reduction in $\ell_1$ , J. ACM, 2005. https://doi.org/10.1145/1089023.1089026
J. R. Lee, M. Mendel, A. Naor, Metric structures in $L_1$ : dimension, snowflakes, and average distortion, European J. Combin., 2005. https://doi.org/10.1016/j.ejc.2004.07.002
A. Naor, Metric dimension reduction: a snapshot of the Ribe program, Proc. ICM 2018. https://arxiv.org/abs/1809.02376
A. Naor, K. Ren, A threshold phenomenon for embeddings of Euclidean snowflakes and impossibility of dimension reduction, preprint, 2026. https://arxiv.org/abs/2609.01079
O. Gurel-Gurevich, A. Nachmias, S. Sachdeva, A tight bound on localization of electrical flows, preprint, 2026. https://arxiv.org/abs/2605.24130

2 thms2 active usersReviewed

Convex Optimization Optimization·Captain: mikedeng1

A Monotone+Skew Splitting Model for Composite Monotone Inclusions in Duality: The Inexact Primal–Dual Forward–Backward–Forward Iterates Converge Weakly to a Primal and a Dual SolutionResearch Paper

Motivation

Many problems in convex optimization, variational inequalities, mechanics, traffic equilibrium and signal processing reduce to finding a zero of a monotone operator on a Hilbert space. Frequently that operator is a sum $A + L^*\circ B\circ L$ of a monotone operator and a monotone operator composed with a linear map and its adjoint, and one also wants the solution of an associated dual inclusion. The prototype is Fenchel–Rockafellar duality: with $A=\partial f$ and $B=\partial g$ , the pair of problems is $\min_x f(x)+g(Lx-r)-\langle x\mid z\rangle$ and $\min_v f^*(z-L^*v)+g^*(v)+\langle v\mid r\rangle$ .

Before this paper, splitting methods for the primal problem needed $B$ to be single-valued and smooth (forward–backward, or Tseng's forward–backward–forward method), or needed the resolvent of $L^*\circ B\circ L$ , which has no closed form in terms of $B$ and $L$ in general. Briceño-Arias and Combettes (arXiv:1011.5517, SIAM J. Optim. 2011) observed that the primal–dual pair is equivalent to a single inclusion on the product space involving a maximally monotone operator plus a bounded skew linear operator. Applying an inexact forward–backward–forward method to that inclusion gives the first algorithm that solves the primal and dual inclusions simultaneously and uses $A$ , $B$ and $L$ separately. Later primal–dual methods, including those of Combettes–Pesquet (2012), Vũ (2013) and Condat (2013), build on this construction.

Setting

Let $\mathcal H$ and $\mathcal G$ be real Hilbert spaces. A set-valued operator $M:\mathcal H\to2^{\mathcal H}$ assigns to each point a subset; its graph is $\{(x,u)\mid u\in Mx\}$ , its inverse $M^{-1}$ has graph $\{(u,x)\mid u\in Mx\}$ , and $\operatorname{zer}M=\{x\mid 0\in Mx\}$ . $M$ is monotone if $\langle x-y\mid u-v\rangle\ge0$ whenever $u\in Mx$ , $v\in My$ , and maximally monotone if no monotone operator has a strictly larger graph. For $\gamma>0$ the resolvent $J_{\gamma M}=(\mathrm{Id}+\gamma M)^{-1}$ is then an everywhere-defined single-valued map.

Problem 1.1. Let $A:\mathcal H\to2^{\mathcal H}$ and $B:\mathcal G\to2^{\mathcal G}$ be maximally monotone, $L:\mathcal H\to\mathcal G$ bounded linear, $z\in\mathcal H$ , $r\in\mathcal G$ . Solve the primal inclusion

z\in Ax+L^*B(Lx-r)\qquad(1.2)

and the dual inclusion

-r\in -LA^{-1}(z-L^*v)+B^{-1}v.\qquad(1.3)

Their solution sets are $\mathcal P$ and $\mathcal D$ .

Problem 1.2. On the Hilbert direct sum $\mathcal K=\mathcal H\oplus\mathcal G$ set

M:(x,v)\mapsto(-z+Ax)\times(r+B^{-1}v),\qquad S:(x,v)\mapsto(L^*v,-Lx),

and find a zero of $M+S$ .

The algorithm (3.1) of the paper, for step sizes $\gamma_n$ and error sequences $a_{i,n},b_{i,n},c_{i,n}$ , reads

\begin{aligned}y_{1,n}&=x_n-\gamma_n(L^*v_n+a_{1,n}), & y_{2,n}&=v_n+\gamma_n(Lx_n+a_{2,n}),\\ p_{1,n}&=J_{\gamma_nA}(y_{1,n}+\gamma_nz)+b_{1,n}, & p_{2,n}&=J_{\gamma_nB^{-1}}(y_{2,n}-\gamma_nr)+b_{2,n},\\ q_{1,n}&=p_{1,n}-\gamma_n(L^*p_{2,n}+c_{1,n}), & q_{2,n}&=p_{2,n}+\gamma_n(Lp_{1,n}+c_{2,n}),\\ x_{n+1}&=x_n-y_{1,n}+q_{1,n}, & v_{n+1}&=v_n-y_{2,n}+q_{2,n}.\end{aligned}

Formalization targets

Goal: Theorem 3.1

Assume $L\neq0$ , $z\in\operatorname{ran}(A+L^*\circ B\circ(L\cdot-r))$ , all six error sequences absolutely summable, $\varepsilon\in\,]0,1/(\|L\|+1)[$ and $\gamma_n\in[\varepsilon,(1-\varepsilon)/\|L\|]$ . Then for some $\bar x\in\mathcal P$ and $\bar v\in\mathcal D$ with $z-L^*\bar v\in A\bar x$ and $\bar v\in B(L\bar x-r)$ :

x_n-p_{1,n}\to0,\quad v_n-p_{2,n}\to0,\qquad x_n,\,p_{1,n}\rightharpoonup\bar x,\quad v_n,\,p_{2,n}\rightharpoonup\bar v,

and the convergence of $x_n,p_{1,n}$ (resp. $v_n,p_{2,n}$ ) is strong if $A$ is uniformly monotone at $\bar x$ (resp. $B^{-1}$ at $\bar v$ ).

Milestones

Lemma 2.1: $\alpha_{n+1}\le\alpha_n-\beta_n+\varepsilon_n$ with nonnegative terms and summable $\varepsilon_n$ implies $(\alpha_n)$ converges and $\sum\beta_n<\infty$ . Covered by the proved platform theorem GradErrors.Deterministic.lemma_1 (Bertsekas–Tsitsiklis), of which it is the special case $Y=\alpha\ge0$ , so that the alternative $Y_t\to-\infty$ cannot occur.
Lemma 2.2: a quasi-Fejér sequence whose sequential weak cluster points lie in $C$ converges weakly to a point of $C$ .
Theorem 2.5(i)–(ii): for $A$ maximally monotone and $B$ monotone and $\beta$ -Lipschitz with $\operatorname{zer}(A+B)\ne\varnothing$ , the inexact forward–backward–forward iteration has $\sum\|x_n-p_n\|^2<\infty$ , $\sum\|y_n-q_n\|^2<\infty$ , and $x_n,p_n\rightharpoonup\bar x\in\operatorname{zer}(A+B)$ .
Proposition 2.7(i)–(iv): $M$ and $M+S$ are maximally monotone; $S$ is bounded linear with $S^*=-S$ and $\|S\|=\|L\|$ ; $J_{\gamma M}(x,v)=(J_{\gamma A}(x+\gamma z),J_{\gamma B^{-1}}(v-\gamma r))$ .
Proposition 2.8: $\operatorname{zer}(M+S)$ is a closed convex subset of $\mathcal P\times\mathcal D$ , and $z\in\operatorname{ran}(A+L^*\circ B\circ(L\cdot-r))$ , $\mathcal P\ne\varnothing$ , $\operatorname{zer}(M+S)\ne\varnothing$ , $\mathcal D\ne\varnothing$ and $-r\in\operatorname{ran}(-L\circ A^{-1}\circ(z-L^*\cdot)+B^{-1})$ are equivalent.

Significance

Theorem 3.1 gives a method that handles two arbitrary maximally monotone operators coupled by an arbitrary bounded linear map, with only resolvent evaluations of $A$ and $B^{-1}$ (computed in parallel) and forward applications of $L$ and $L^*$ . It tolerates summable errors in every step and variable step sizes, and it produces a primal and a dual solution simultaneously, assuming only that the primal problem is solvable. The paper derives from it, as instances, methods for sums of composite operators (Theorem 3.8) and for Fenchel–Rockafellar-type composite minimization (Section 4).

The theorem is proved in the literature. This mission formalizes it, which in turn requires a machine-checked inexact forward–backward–forward theorem (Theorem 2.5) and the structural facts about the monotone+skew reformulation (Propositions 2.7, 2.8). These intermediate results are reusable for the descendants of this algorithm. No machine-checked proof of Theorem 3.1, of Theorem 2.5, or of the quasi-Fejér Lemma 2.2 is known to the mission's authors. On Prove2Me, CondatPD.FB.lemma_4_4 (inexact forward–backward with a cocoercive operator) and CondatPD.FB.theorem_3_1 (Condat's primal–dual method) concern related algorithms; CondatPD.PPA.A_maximal_monotone is an open subdifferential special case of Proposition 2.7(iii).

Difficulty

The obvious route, applying a known splitting method directly to $A_1+A_2$ with $A_2=L^*\circ B\circ(L\cdot-r)$ , fails: $A_2$ need not be maximally monotone, and its resolvent cannot be computed from that of $B$ . The reformulation on $\mathcal K$ avoids this, but at a cost. $M+S$ is not a subdifferential, $S$ is not cocoercive (it is skew, so $\langle Sx\mid x\rangle=0$ ), and forward–backward theory does not apply; one needs the forward–backward–forward method with Lipschitz, merely monotone $S$ . Proving that method's convergence with errors requires quasi-Fejér analysis in a possibly infinite-dimensional space, where bounded sequences only have weakly convergent subsequences and the limit must be identified through the maximal monotonicity of $M+S$ , whose graph is sequentially closed in the weak–strong topology. The strong convergence clauses (iii)–(iv) need a further estimate, since uniform monotonicity of $A$ at $\bar x$ does not by itself control the coupled iterate.

Formalization scope

Hilbert spaces are [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]; set-valued operators are maps E → Set E. Monotonicity, maximal monotonicity (no proper monotone extension of the graph), zer, the resolvent predicate IsResolvent, weak convergence WeakTendsto ( $\langle u_n,y\rangle\to\langle u,y\rangle$ for all $y$ ), opInv and opAdd are imported from published platform definitions.
$\mathcal K=\mathcal H\oplus\mathcal G$ is WithLp 2 (H × G), whose inner product is $\langle x\mid x'\rangle+\langle v\mid v'\rangle$ ; the plain product would carry the sup norm.
Resolvents are given maps with the resolvent property, one per iteration since $\gamma_n$ varies: JA n satisfies $\gamma_n^{-1}(w-J^A_nw)\in A(J^A_nw)$ for all $w$ , and likewise for $B^{-1}$ . For maximally monotone operators and $\gamma_n>0$ such maps exist (Minty's theorem) and are unique, so quantifying over them is the paper's statement. Proposition 2.7(iv) is stated as "the product map is a resolvent of $\gamma M$ ", which is the equality by uniqueness.
"Absolutely summable" is Summable (fun n => ‖a n‖); indices start at $0$ ; $\|L\|$ is the operator norm and $L\ne0$ is kept, so the step-size window is nonempty.
" $S\in\mathcal B(\mathcal K)$ " is the existence of a continuous linear operator equal to $S$ pointwise, whose adjoint is its negative and whose norm is $\|L\|$ .
"Uniformly monotone at $x$ " (Lemma 2.4(i)) uses a nondecreasing $\phi:[0,\infty[\to[0,+\infty]$ vanishing only at $0$ , compared in EReal, against every point of the graph. It is neither strong monotonicity nor uniform monotonicity on a set.
Lemma 2.1 is not restated: the mission references the proved platform theorem GradErrors.Deterministic.lemma_1, of which it is a special case.
A trivializing formalization is ruled out. The resolvents are constrained by their defining property (an unconstrained map would make the goal false), the existence hypothesis is the paper's only one ( $z\in\operatorname{ran}(A+L^*\circ B\circ(L\cdot-r))$ , not a dual solution or a zero of $M+S$ ), and the hypotheses are satisfiable ( $\mathcal H=\mathcal G=\mathbb R$ , $A=B=0$ , $L=\mathrm{Id}$ is a checked instance).

The mission needs Minty-type facts (existence of resolvents), demiclosedness of maximally monotone graphs, sums of a maximally monotone and a Lipschitz monotone operator, and quasi-Fejér/Opial arguments in Hilbert space. None of these is in Mathlib in this form, and all are reusable beyond this mission. Contributions toward any of the milestones, or toward this general infrastructure, are welcome.

Selected references

L. M. Briceño-Arias, P. L. Combettes, A monotone+skew splitting model for composite monotone inclusions in duality, arXiv:1011.5517v1 (2010); SIAM J. Optim. 21 (2011) 1230–1250. https://arxiv.org/abs/1011.5517v1 , https://doi.org/10.1137/10081602X
P. Tseng, A modified forward-backward splitting method for maximal monotone mappings, SIAM J. Control Optim. 38 (2000) 431–446. https://doi.org/10.1137/S0363012998338806
H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011. https://doi.org/10.1007/978-1-4419-9467-7
D. P. Bertsekas, J. N. Tsitsiklis, Gradient convergence in gradient methods with errors, SIAM J. Optim. 10 (2000) 627–642. https://doi.org/10.1137/S1052623497331063
P. L. Combettes, J.-C. Pesquet, Primal-dual splitting algorithm for solving inclusions with mixtures of composite, Lipschitzian, and parallel-sum type monotone operators, Set-Valued Var. Anal. 20 (2012) 307–330. https://doi.org/10.1007/s11228-011-0191-y
B. C. Vũ, A splitting algorithm for dual monotone inclusions involving cocoercive operators, Adv. Comput. Math. 38 (2013) 667–681. https://doi.org/10.1007/s10444-011-9254-8
L. Condat, A primal–dual splitting method for convex optimization involving Lipschitzian, proximable and linear composite terms, J. Optim. Theory Appl. 158 (2013) 460–479. https://doi.org/10.1007/s10957-012-0245-9

13 thms2 active usersReviewed

Markov Chain Probability·Captain: mikedeng1

Logarithmic Sobolev Inequalities for Finite Markov Chains 3: Lower Bound α ≥ (1 − 2/q)λ / 2(λt_q + log M_q + (q − 2)/q) from a Bound on ‖H_{t_q}‖_{2→q}Research Paper

Motivation

A finite Markov chain describes a system that changes state according to fixed transition probabilities. For a chain that settles toward an equilibrium distribution, a central question is how quickly the effect of its starting state disappears. The logarithmic Sobolev constant supplies quantitative control of this convergence and, through hypercontractive estimates, also governs how the continuous-time transition operator changes the size of functions measured in different norms. Diaconis and Saloff-Coste's 1996 paper develops these relations for finite chains and uses them to study mixing on graphs and product spaces.

The constant can be hard to calculate directly. Its definition is an infimum over all nonconstant functions, while a particular Markov semigroup may admit an accessible bound from $\ell^2$ to $\ell^q$ at one time. Theorem 3.9 turns such an operator estimate into a numerical lower bound for the log-Sobolev constant. This mission formalizes that result, including both finite $q$ and the supremum-norm endpoint.

Setting

Let $\mathcal X$ be a finite state space. A Markov kernel $K(x,y)$ is nonnegative, with $\sum_yK(x,y)=1$ for every $x$ . A strictly positive stationary distribution $\pi$ satisfies $\sum_x\pi(x)K(x,y)=\pi(y)$ and $\sum_x\pi(x)=1$ . The chain is reversible when $\pi(x)K(x,y)=\pi(y)K(y,x)$ for every pair of states. Its continuous-time heat semigroup is $H_t=e^{-t(I-K)}$ , acting on a function $f$ by $H_tf$ . These conventions follow §§2.1–2.3 of the source paper.

For a real function on $\mathcal X$ , write $\|f\|_p=(\sum_x|f(x)|^p\pi(x))^{1/p}$ when $p$ is finite, and $\|f\|_\infty=\max_x|f(x)|$ . The Dirichlet form is $\mathcal E(f,g)=\sum_x(f(x)-Kf(x))g(x)\pi(x)$ . The quadratic entropy functional is $\mathcal L(f)=\sum_x|f(x)|^2\log(|f(x)|^2/\|f\|_2^2)\pi(x)$ , with a zero contribution where $f(x)=0$ . Write $Ef=\sum_xf(x)\pi(x)$ and $\operatorname{Var}_\pi(f)=\|f-Ef\|_2^2$ .

The spectral gap in this mission is the variational constant $\lambda=\inf_{\operatorname{Var}_\pi(f)\ne0}\mathcal E(f,f)/\operatorname{Var}_\pi(f)$ , as in (2.4). The log-Sobolev constant is $\alpha=\inf_{\mathcal L(f)\ne0}\mathcal E(f,f)/\mathcal L(f)$ , as in (3.1). These definitions specify the quantities that Theorem 3.9 relates; in particular, $\lambda$ is the paper's variational quantity, rather than an eigenvalue expression imported from a different convention.

Formalization targets

Theorem 3.9: a single heat-operator estimate bounds $\alpha$

Suppose $2<q<\infty$ , $t_q>0$ , and $M_q$ satisfy $\|H_{t_q}f\|_q\le M_q\|f\|_2$ for every function $f$ . The paper's theorem asserts

\alpha\ge\frac{(1-2/q)\lambda}{2\left(\lambda t_q+\log M_q+(q-2)/q\right)}.

It also covers $q=\infty$ : the hypothesis then uses $\|H_{t_q}f\|_\infty$ , and the two fractions involving $q$ in the displayed bound become $1$ .

Companion results

Theorem 3.10 replaces $H_{t_q}$ in the norm hypothesis with $H_{t_q}-E$ , where $E$ sends a function to its constant mean. Corollary 3.11 relates $\alpha$ to $\tau$ , the first time at which every heat-kernel density $h_t^x(y)=H_t(x,y)/\pi(y)$ is within $1/e$ of $1$ in $\ell^2(\pi)$ :

\frac1{2\alpha}\le\tau\le\frac{4+\log\log(1/\pi_*)}{4\alpha}, \qquad \pi_*=\min_x\pi(x).

The three milestones reproduce the interpolation estimate (3.6), the resulting entropy inequality, and the centering inequality (3.7). Theorem 3.10's printed finite- $q$ denominator contains $(q-2)/2$ ; its displayed proof and the $q=\infty$ use in Corollary 3.11 require $(q-2)/q$ . That proof also needs $\log M_q+(q-2)/q\ge0$ , which the page does not state and without which the printed statement fails on a four-state product chain. The formal companion records both corrections, while the main goal follows the printed Theorem 3.9 exactly.

Significance

Theorem 3.9 makes a norm bound at a chosen time useful beyond that time: it yields a bound on a functional inequality that holds for every function on the state space. Thus estimates obtained from an explicit heat kernel or another analytic method can be compared across chains using the same constant $\alpha$ . The centered version and the bound for $\tau$ connect this functional viewpoint back to convergence from a point mass, as the paper explains in §3.4.

The mathematical results are proved in the 1996 paper. Here the remaining work is to give their finite-state objects, norm hypotheses, and constants machine-checked meanings, then formalize the proofs. The definition layer and the centering inequality have use beyond this mission: they can support other statements about entropy decay and heat-kernel convergence in the same paper.

Difficulty

A bound for $H_t$ in the same norm is too weak to recover the displayed lower bound: the information here is the change from an $\ell^2$ input to an $\ell^q$ output. The dependence of the exponent on time must retain the factors $(1-2/q)$ and $(q-2)/q$ exactly. The endpoint $q=\infty$ also requires a separate norm statement, since a real exponent cannot represent infinity. The centering inequality (3.7) is another substantial step; the paper points to earlier proofs rather than treating it as immediate.

Formalization scope

The state space is a finite Lean type, the kernel a real matrix, and the invariant law a positive real-valued probability vector. Reversibility is detailed balance, and irreducibility is retained from the standing setting of §3.1. The heat semigroup uses the already published Poissonized heat kernel. Operator norms are represented by inequalities quantified over every real function. The finite- $q$ and $q=\infty$ conclusions are separate clauses of the goal. Time is real; $t_q>0$ makes explicit the positive-time convention used in §3.4. Theorem 3.10 carries the condition $M_q\ge e^{-(q-2)/q}$ (and $M_\infty\ge e^{-1}$ ) described above; Corollary 3.11 is stated without any extra condition.

The variational constants are real infima, the logarithms and real powers use Lean's total operations, and the supremum norm is a supremum over the finite state space. The stationary probability hypothesis rules out an empty state space; the operator hypothesis on the constant function forces $M_q\ge1$ in Theorem 3.9. These facts prevent the bound from arising from a zero norm, an empty operator test, an invalid logarithm, or an eigenvalue convention different from (2.4). Useful contributions include finite-state entropy inequalities, interpolation machinery, estimates for the heat operator, and proofs of the three stated milestones.

Selected references

P. Diaconis and L. Saloff-Coste, Logarithmic Sobolev inequalities for finite Markov chains, Annals of Applied Probability 6 (1996), 695–750. DOI.

10 thms2 active usersReviewed

Convex Optimization Numerical Analysis·Captain: mikedeng1

A Dual Algorithm for the Solution of Nonlinear Variational Problems via Finite Element Approximation 2: Internal Approximations Under (4.1)–(4.3) Have Solutions v_h Converging Strongly to vResearch Paper

Motivation

An infinite dimensional variational problem can be described by continuous linear operators and convex functionals, yet numerical work needs finite dimensional spaces. The question is whether a solution computed in a finite dimensional approximation still approaches the solution of the original problem when the approximation is refined. Gabay and Mercier's IRIA report studies this question alongside a dual algorithm. Its Section 4 gives a convergence statement for internal approximations of the primal problem. The result is relevant to finite element methods because it identifies conditions on the discrete spaces, discrete operators, and nonsmooth part of the objective that ensure convergence of the minimizers.

The report is the June 1975 preprint of a 1976 journal paper. This mission follows the pinned report version, hal-04716124v1, whose theorem and equation numbers are used throughout. Its Section 4 first states the abstract approximation theorem and then turns to a concrete finite element construction. The abstract theorem is the target here. Gabay and Mercier, pp. 20–23.

Setting

Let $V$ and $Y$ be real Hilbert spaces, and let $A:V\to Y$ be a continuous linear operator. A continuous linear functional $b\in V'$ supplies a linear term. Let $f_2:Y\to(-\infty,+\infty]$ be a proper, convex, lower semicontinuous function. Its value may be $+\infty$ , which excludes an inadmissible point. The continuous problem $({\cal P})$ is to minimize

J(v)=\frac12\|Av\|^2+f_2(Av)-\langle b,v\rangle,\qquad v\in V.

A solution has finite objective value and minimizes $J$ over all of $V$ . The report's coercivity condition (2.5) supplies $\alpha>0$ such that $\|Av\|^2\ge\alpha^2\|v\|^2$ for every $v\in V$ . It also assumes the interior of the effective domain of $f_2$ is nonempty. The proof of Proposition 2.1 explicitly requires a point $v_0\in V$ with $f_2(Av_0)<+\infty$ ; this feasibility condition is made explicit here. Gabay and Mercier, pp. 8–9.

For each approximation index $k$ , let $V_k\subseteq V$ be a finite dimensional subspace and $A_k:V_k\to Y$ a continuous linear operator. The discrete problem $({\cal P}_k)$ minimizes $\frac12\|A_kw\|^2+f_2(A_kw)-\langle b,w\rangle$ over $w\in V_k$ . The same $A_k$ appears in both terms involving the image of $w$ . The report also describes a subspace $Y_h\subseteq Y$ containing the range of $A_h$ ; the abstract convergence claim uses those images only as elements of $Y$ . Gabay and Mercier, pp. 20, 23.

The operator assumptions (4.1) include uniform constants $\alpha'>0$ and $M$ with $\alpha'\|w\|\le\|A_kw\|\le M\|w\|$ , preservation of weak and strong limits, and $\|A_kw-Aw\|\to0$ for uniformly bounded families. The compatibility condition (4.3) requires, for each $v\in V$ , points $w_k\in V_k$ with $w_k\to v$ and $f_2(A_kw_k)\to f_2(Av)$ . The latter limit is extended valued when necessary. These conditions define what counts as an internal approximation for this theorem. Gabay and Mercier, p. 20.

Formalization targets

The main target is Theorem 4.1. The continuous problem has a unique solution $v^*$ ; the discrete problems have unique solutions for all sufficiently fine approximations; and

v_k^*\longrightarrow v^*\quad\text{strongly in }V.

The theorem's phrase “in $V_h$ strongly” is read in the common ambient space $V$ , because the spaces $V_h$ vary. The claim covers every selection of discrete minimizers once they exist. The paper's conditions allow a few early discrete problems to be infeasible, so existence is asserted eventually. Gabay and Mercier, p. 21, Theorem 4.1.

The milestone list follows the report's own path from the application of Proposition 2.1 on p. 20 through the variational inequality (4.4), the bound after (4.5), weak convergence after (4.7), the estimate (4.8), and the limits (4.10)–(4.11). The equations (4.5) and (4.8) contain printing slips; their milestone excerpts preserve the printed text, while their formal statements use the mathematically consistent readings explained with each item. Gabay and Mercier, pp. 21–22.

Significance

The theorem gives a precise guarantee for a family of finite dimensional problems: a computed minimizer is meaningful as an approximation to the unique solution of the infinite dimensional problem when the discretization satisfies the stated conditions. The operator $A_k$ may differ from the restriction of $A$ to $V_k$ , and the nonsmooth term $f_2$ may assign $+\infty$ outside its domain. The conclusion therefore covers settings in which simply restricting the continuous objective to a subspace would describe the wrong numerical problem. Gabay and Mercier, pp. 20–23.

The result is proved in the report; the remaining task is a machine checked proof of the abstract approximation theorem and its cited intermediate claims. A formal development would also leave reusable statements about extended valued convex minimization, weak convergence of Hilbert space sequences, and uniformly consistent discrete operators. This proposal supplies statements for those claims; it does not claim that they already have machine checked proofs.

Difficulty

Strong convergence cannot be read off from a bound on the discrete solution norms. Uniform boundedness yields only access to weak limits in the Hilbert space; the solution's images and the nonsmooth objective must still behave correctly under the varying operators. Weak convergence of $v_k^*$ alone also does not imply convergence in norm. A proof must keep the weak limit, the lower semicontinuity of $f_2$ , and the discrepancy between $A_k$ and $A$ aligned under the same approximation assumptions. The fact that $f_2$ may be infinite makes unguarded subtraction of its values invalid. Gabay and Mercier, pp. 21–22.

Formalization scope

Lean uses real complete inner product spaces for $V$ and $Y$ , continuous linear maps for $A$ and $A_k$ , and StrongDual ℝ V for $b$ . The index $k\to\infty$ represents a sequence of mesh parameters $h_k\to0$ ; the report's convergence claims are sequential. Each $V_k$ is finite dimensional. The codomain spaces $Y_h$ are suppressed through their inclusions in $Y$ . Weak convergence uses all Hilbert inner products as tests, while “strongly” means convergence in the norm topology.

The function $f_2$ takes values in EReal, with properness excluding $-\infty$ . Its limit in (4.3) uses the extended real topology. The quadratic term is real valued. A solution must have a finite objective value, and the continuous problem must have a feasible point. The section's interior-domain assumption (2.4) is retained even though the abstract proof does not use it. Condition (4.1)(iv) quantifies over every uniformly bounded family. These choices rule out the vacuous interpretation in which all continuous or discrete objective values are $+\infty$ .

The report's $f_1(y)=\frac12\|y\|^2$ automatically satisfies the earlier gradient monotonicity requirement (2.3). The published InertialFB.IFB.ConvexAnalysis definition provides properness, convexity, and weak convergence with matching conventions. The new local definition supplies the two objectives, solution predicates, and approximation hypotheses. Contributions proving the goal and its milestones are welcome; separate treatments of the concrete triangulation and quadrature construction of Proposition 4.1 are outside this mission. Gabay and Mercier, pp. 20–26.

Selected references

D. Gabay and B. Mercier, A dual algorithm for the solution of non linear variational problems via finite element approximation, IRIA Rapport de Recherche no. 126, June 1975, hal-04716124v1. This report is the version whose numbering the mission uses.
D. Gabay and B. Mercier, A dual algorithm for the solution of nonlinear variational problems via finite element approximation, Computers & Mathematics with Applications 2 (1976) 17–40, doi:10.1016/0898-1221(76)90003-1. The journal version; its numbering is not used here.

13 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Nonlinear Proximal Point Algorithms Using Bregman Functions, with Applications to Convex Programming 2: Bregman Proximal Point Sequences Exist When im ∇h Is ℝⁿ, or Is Open and 0 ∈ im TResearch Paper

Motivation

The proximal point method seeks a zero of an operator by repeatedly solving an implicit equation. For a maximal monotone operator, the ordinary quadratic proximal step is available throughout a Hilbert space. Eckstein's 1993 paper replaces the quadratic penalty with a Bregman function, allowing a step to reflect the geometry of a constrained problem. Before convergence can be discussed, each implicit step must have a solution in the region where the Bregman gradient is defined. Eckstein, 1993, §§1–2 isolates that existence question in Theorem 4.

The theorem draws on the L-property and a range theorem attributed to Brézis and Haraux. Their results describe when the image of a sum of monotone operators is large enough to contain the inputs of a proximal step. The paper uses those results to obtain two practical sufficient conditions: a gradient whose image is the whole space, or an open gradient image together with a zero in the image of the operator. Eckstein, 1993, Theorems 2–4

Setting

Let $H$ be a finite-dimensional real inner product space, representing the paper's $\mathbb R^n$ . An operator $T:H\to2^H$ assigns a set of vectors to each point. It is monotone when $\langle x-y,u-v\rangle\ge0$ whenever $u\in Tx$ and $v\in Ty$ , and maximal monotone when its graph cannot be enlarged while preserving monotonicity. Its domain and image are $\operatorname{dom}T=\{x:Tx\ne\varnothing\}$ and $\operatorname{im}T=\{u:\exists x,\ u\in Tx\}$ .

Let $S\subseteq H$ be open. A Bregman function with zone $S$ is a real function $h$ on $\bar S$ satisfying the six conditions of Definition 1: continuous differentiability on $S$ , strict convexity and continuity on $\bar S$ , boundedness of two families of partial level sets, and two sequential conditions that relate convergence to its D-function

D_h(x,y)=h(x)-h(y)-\langle\nabla h(y),x-y\rangle,\qquad (x,y)\in\bar S\times S.

The gradient is an operator with domain $S$ and image $\nabla h(S)$ . For positive step sizes $c_k$ , a Bregman proximal point sequence is a sequence $x^k\in S$ satisfying

\frac{1}{c_k}\bigl(\nabla h(x^k)-\nabla h(x^{k+1})\bigr)\in T(x^{k+1})\quad(k\ge0).

This is the inclusion form (4) of recursion (3). The expression $\nabla h+c_kT$ is a sum of set-valued operators, and each step asks for a preimage of $\nabla h(x^k)$ under that sum. Eckstein, 1993, pp. 205–207

Formalization targets

The goal is Theorem 4. If $T$ is maximal monotone, $h$ is Bregman with zone $S\supseteq\operatorname{dom}T$ , and either

\operatorname{im}\nabla h=H, \qquad\text{or}\qquad \operatorname{im}\nabla h\text{ is open and }0\in\operatorname{im}T,

then every $x^0\in S$ and every positive sequence $(c_k)$ admit an infinite Bregman proximal point sequence starting at $x^0$ . The theorem asserts existence for every starting point in the zone, at every step. Eckstein, 1993, p. 209, Theorem 4

The milestones follow the cited results and the paper's proof: trimonotone operators and subdifferentials have the L-property (Theorem 2); the interior and closure of the image of a sum agree with those of the sum of images under the hypotheses of Theorem 3; the subdifferential and gradient sums agree on the domain of $T$ and yield a maximal monotone sum; and the relevant gradient image lies in the image of $\nabla h+cT$ for every $c>0$ . These targets provide the range statement needed for the infinite recursion. Eckstein, 1993, pp. 208–209

Significance

Theorem 4 certifies that the nonlinear proximal point recursion is well defined from any admissible starting point under either range condition. Without this existence statement, a convergence theorem for sequences satisfying the recursion leaves open whether a sequence can be generated. Its range conditions also distinguish Bregman geometries whose gradient covers the whole space from geometries with a smaller but open gradient image. Eckstein, 1993, p. 209

The mathematical result is proved in the paper; the work here is to formalize its definitions, the Brézis–Haraux statements cited there, and the existence theorem in Lean. The milestone statements are open proof obligations in the draft, not claims of completed machine-checked proofs. The operator vocabulary and range theorem can be reused for other implicit algorithms involving sums of monotone operators.

Difficulty

Knowing that $T$ and $\nabla h$ are monotone does not by itself show that a prescribed $\nabla h(x^k)$ belongs to $\operatorname{im}(\nabla h+c_kT)$ . Even maximality of $T$ alone gives no direct description of that image. The hard point is the range of the sum on the zone of $h$ , especially when $\nabla h(S)$ is a proper subset of $H$ . Theorem 3 supplies an interior and closure comparison, but its domain, maximality, and L-property hypotheses must all be established for the particular operators in Theorem 4. Eckstein, 1993, pp. 208–209

Formalization scope

The Lean model uses a finite-dimensional real inner product space $H$ , set-valued operators $H\to\operatorname{Set}H$ , and Mathlib's gradient on the open zone $S$ . The image of $\nabla h$ is precisely $\nabla h(S)$ ; values of the total Lean gradient outside $S$ do not enter it. The function $h:H\to\mathbb R$ is total for Lean's type system, but only values on $\bar S$ matter. Its extension by $+\infty$ outside $\bar S$ is EReal-valued, and the subdifferential uses the published convex-analysis predicate. The L-property uses boundedness below in $\mathbb R$ , matching the paper's strict lower bound above $-\infty$ .

Recursion (3) is represented by its equivalent inclusion (4), with every iterate explicitly in $S$ . The paper leaves the positive step sizes implicit in Theorem 4; the goal quantifies over all such sequences and imposes no convergence-specific lower bound on them. Condition (vi) of Definition 1 is applied to first arguments in $\bar S$ , the stated natural domain of $D_h$ . Trimonotonicity is the three-point cyclic condition used by Brézis and Haraux. A one-step solution, a sequence with an arbitrary starting point chosen by the prover, or an image taken over all of $H$ would not establish this target.

The development needs convex subdifferentials, maximal monotonicity, maximality of appropriate sums, and the Brézis–Haraux range result. Contributions that prove these milestones or add reusable range lemmas are within scope; an optional formalization of the existence part of Theorem 5 is outside the core path.

Selected references

J. Eckstein, Nonlinear proximal point algorithms using Bregman functions, with applications to convex programming, Mathematics of Operations Research 18(1), 202–226, 1993. DOI.
H. Brézis and A. Haraux, Image d'une somme d'opérateurs monotones et applications, Israel Journal of Mathematics 23, 165–186, 1976. DOI.

11 thms2 active usersReviewed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Duality and Stability in Extremum Problems Involving Convex Functions 3: If f Is Finite at x and g Is Finite and Continuous at Ax, Then (P) Is Stably Set and inf (P(z)) Is Continuous Near z = 0Research Paper

Motivation

A convex program is useful in practice only if its optimal value responds reasonably to small changes in the data. Lagrangian and Fenchel duality theory makes this precise: the dual problem attains its optimum and has no duality gap exactly when the primal value function does not fall off infinitely steeply under small perturbations. A constraint qualification is a checkable condition on the data that guarantees this good behaviour; Slater's condition (a strictly feasible point) is the best-known example in finite dimensions.

R. T. Rockafellar's 1967 paper Duality and Stability in Extremum Problems Involving Convex Functions (Pacific J. Math. 21 (1967) 167–187) develops Fenchel-type duality for the problem of minimizing $f(x) - g(Ax)$ in general locally convex spaces. It introduces the notion of a stably set problem, shows that stability is equivalent to strong duality with an attained dual optimum (its Theorem 3), and gives in Theorem 1 a general sufficient condition for stability. Theorem 1 is the infinite-dimensional analogue of Slater's condition and is the form in which the result is usually applied: one exhibits a single point where $f$ is finite and $g$ is finite and continuous.

Timeline. Fenchel (1951) proved the duality theorem for $A = I$ in $\mathbb{R}^n$ under relative-interior conditions. Brøndsted (1964) and Moreau (1966–67) extended conjugate duality to paired locally convex spaces. Rockafellar's 1967 paper (this mission) added the linear map $A$ , the perturbation function $h$ , the notion of stability, and Theorem 1. The perturbational approach was later systematized in Rockafellar's Conjugate Duality and Optimization (SIAM, 1974).

Setting

Let $E$ and $F$ be real locally convex Hausdorff topological vector spaces and $A : E \to F$ a continuous linear map. Let $f : E \to [-\infty, +\infty]$ and $g : F \to [-\infty, +\infty]$ .

$f$ is convex if its epigraph $\{(x, \mu) \mid x \in E, \mu \in \mathbb{R}, \mu \ge f(x)\}$ is a convex subset of $E \times \mathbb{R}$ ; it is proper if $f(x) > -\infty$ for all $x$ and $f(x) < +\infty$ for some $x$ . $g$ is concave if $-g$ is convex, and proper concave if $g < +\infty$ everywhere and $g > -\infty$ somewhere.
Throughout, $f$ is lower semicontinuous proper convex and $g$ is upper semicontinuous proper concave. Their effective domains are $C = \{x \mid f(x) < +\infty\}$ and $D = \{y \mid g(y) > -\infty\}$ .
The primal problem is

(P) \qquad \text{minimize } f(x) - g(Ax) \text{ over } x \in E,

and its perturbations are $(P(z))$ : minimize $f(x) - g(Ax - z)$ , for $z \in F$ . The perturbation function is $h(z) = \inf (P(z)) = \inf_x \{ f(x) - g(Ax - z) \} \in [-\infty, +\infty]$ , so $h(0) = \inf (P)$ . $(P)$ is consistent if $h(0) < +\infty$ .

When $h(0)$ is finite, the directional derivative is $h'(0; z) = \lim_{\varepsilon \downarrow 0} [h(\varepsilon z) - h(0)]/\varepsilon$ .
$(P)$ is unstably set if $h(0)$ is finite and every neighbourhood of $0$ contains vectors $z$ with $h'(0; z)$ a negative number of arbitrarily large magnitude ( $-\infty$ included). $(P)$ is stably set if it is consistent but not unstably set.

Formalization targets

Goal: Theorem 1 (p. 175)

Suppose there exists $x \in E$ such that $f$ is finite at $x$ and $g$ is finite and continuous at $Ax$ . Then

(P) \text{ is stably set} \quad\text{and}\quad \text{there is a neighbourhood } U \text{ of } 0 \text{ on which } z \mapsto \inf (P(z)) \text{ is continuous}.

The neighbourhood $U$ is left unspecified, as in the paper.

Milestones (in the order the proof uses them)

(4.4) $\{z \mid h(z) < +\infty\} = \{Ax - y \mid f(x) < +\infty,\ g(y) > -\infty\} = A(C) - D$ .
(4.5) $A(C)$ meets $\operatorname{int} D$ , and $0 \in A(C) - \operatorname{int} D \subseteq \operatorname{int}(A(C) - D)$ .
Epigraph of $h$ has interior (p. 176): the hypograph $G = \{(y, \mu) \mid g(y) \ge \mu > -\infty\}$ has nonempty interior, $(Ax, \lambda) - G$ lies in the epigraph of $h$ for every $(x, \lambda)$ in the epigraph of $f$ , and so the epigraph of $h$ has nonempty interior.
Continuity on the interior of the domain (p. 176): $0 \in \operatorname{int}\{h < +\infty\}$ and $h$ is continuous there.
(4.6) For a convex $h$ with $h(0)$ finite: $h(z) \ge h(0) + h'(0; z)$ and $h'(0; z) \ge -h'(0; -z)$ for all $z$ .

Significance

The result. Combined with the paper's Theorem 3, Theorem 1 yields: if $f$ is finite at some $x$ where $g$ is finite and continuous at $Ax$ , then $\inf (P) = \max (P^*)$ , with the dual maximum attained. This is the standard sufficient condition for Fenchel–Rockafellar duality in infinite dimensions, used in calculus of variations, optimal control, and the convex analysis of integral functionals. The continuity half of Theorem 1 says that the optimal value depends continuously on translations of the constraint data near the unperturbed problem, a basic sensitivity statement.

Formalizing it. The theorem is proved (1967) and appears in many textbooks, but there is no machine-checked version on this platform. Mathlib contains continuity criteria for real-valued convex functions on open sets of normed or finite-dimensional spaces (ConvexOn.continuousOn_tfae, ConvexOn.continuousOn_interior), but nothing for extended-real-valued convex functions on general topological vector spaces, no perturbation function, and no notion of a stably set problem. A complete development would provide reusable infrastructure: the epigraph-interior continuity criterion for $[-\infty, +\infty]$ -valued convex functions and the elementary calculus of one-sided directional derivatives.

Difficulty

The obvious argument says: $g$ is continuous at $Ax$ , so $h(z) \le f(x) - g(Ax - z)$ is bounded above near $0$ , hence $h$ is continuous at $0$ and its directional derivatives are bounded. Two steps of this fail without care. First, the passage from "bounded above near a point" to "continuous" requires convexity of $h$ (Lemma 2 of the paper, proved in the companion mission) and a continuity criterion valid in an arbitrary topological vector space, with values in $[-\infty, +\infty]$ ; the normed-space proofs in Mathlib do not apply. Second, $h$ may take the value $-\infty$ , and the derivative may be $-\infty$ in some directions; the bookkeeping of extended-real arithmetic (where $(+\infty) + (-\infty)$ is not defined mathematically and is given a junk value in Lean) has to be done honestly. Finally, upper bounds on $h'(0;\cdot)$ must be converted into lower bounds, which is where the second inequality of (4.6) enters; an upper bound alone does not give stability.

Formalization scope

All values are in Lean's EReal. Convexity is convexity of the epigraph with real second coordinate (the paper's definition, p. 170); concavity is convexity of $-g$ . Properness is stated as in the paper. The perturbation function is the EReal infimum ⨅ x, f x - g (A x - z); under properness the undefined form $(+\infty) - (+\infty)$ never arises. The directional derivative (4.3) is the lower limit of the difference quotient along $\varepsilon \to 0^+$ , which equals the paper's limit whenever it exists (always, for convex $h$ with $h(0)$ finite). "Unstably set" quantifies over all neighbourhoods of $0$ and all real $M$ , with $h'(0;z) < -M$ allowing $-\infty$ . "Stably set" is $h(0) < +\infty$ together with "not unstably set", so $\inf (P) = -\infty$ is stably set, as the paper says on p. 176. Continuity is with respect to the order topology of EReal, and "continuous at $Ax$ " is continuity of $g$ itself at that point, not of its restriction to $D$ .

The paper's standing setting (§3) includes dual spaces $E^*, F^*$ , the adjoint $A^*$ and the conjugates $f^*, g^*$ . Neither Theorem 1 nor its proof uses them, so they are omitted and the theorem is stated for every pair of real locally convex Hausdorff spaces, which includes every paired setting. The lower and upper semicontinuity of $f$ and $g$ are standing hypotheses of the paper and are kept, although the proof does not use them. Inequality (4.6) is stated for an arbitrary convex function finite at $0$ , the generality in which the paper invokes it. No statement was repaired.

A definition of "stably set" that already presumed finiteness or continuity of $h$ near $0$ , or that tested the derivative only in a fixed set of directions, would make the first conclusion of Theorem 1 trivial; the definition used here is the paper's p. 175 definition verbatim, applied to an arbitrary function $h$ . The definitions are local to this mission; the companion missions on Theorem 3 and Theorem 6 of the same paper define the same objects in their own namespaces. Contributions are welcome on the milestones in any order, and in particular on a general continuity criterion for extended-real-valued convex functions on topological vector spaces, which is reusable well beyond this mission.

Selected references

R. T. Rockafellar, Duality and stability in extremum problems involving convex functions, Pacific J. Math. 21 (1967) 167–187. https://doi.org/10.2140/pjm.1967.21.167
A. Brøndsted, Conjugate convex functions in topological vector spaces, Mat.-Fys. Medd. Dansk. Vid. Selsk. 34 (1964), no. 2.
W. Fenchel, Convex Cones, Sets and Functions, lecture notes, Princeton University, 1951.
J. J. Moreau, Fonctionnelles convexes, Séminaire Leray, Collège de France, 1966–67.
R. T. Rockafellar, Conjugate Duality and Optimization, CBMS-NSF Regional Conference Series in Applied Mathematics 16, SIAM, 1974. https://doi.org/10.1137/1.9781611970524

9 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Régularisation d'inéquations variationnelles par approximations successives I: Every Weak Cluster Point of the Regularized Iterates Solves the Monotone Variational InequalityResearch Paper

Motivation

The proximal point algorithm is a basic iterative scheme of convex optimization and monotone operator theory. To solve a problem governed by a monotone operator, it replaces the problem by a sequence of better-conditioned problems, each regularized by a quadratic term centred at the previous iterate. Augmented Lagrangian methods, the Douglas–Rachford and ADMM splitting schemes, and many bundle methods can all be read as instances of it.

The scheme first appeared in a five-page note by Bernard Martinet in the Revue française d'informatique et de recherche opérationnelle (1970), under the name régularisation par approximations successives. Martinet stated it for a monotone variational inequality on a bounded closed convex subset of a Hilbert space and proved that the weak cluster points of the iterates are solutions. This mission formalizes that first convergence theorem as it was originally stated.

Timeline.

1966–1967: Hartman–Stampacchia and Lions–Stampacchia prove existence of solutions for monotone, hemicontinuous variational inequalities on bounded closed convex sets (Lions–Stampacchia 1967). Minty's lemma characterizes the solution set by the inequality with the operator evaluated at the variable point.
1970: Martinet introduces the regularization iteration (2) and proves Théorème 1 below (Martinet 1970). In §IV of the same note he states the convex-minimization version.
1976: Rockafellar extends the method to maximal monotone operators, allowing inexact steps and variable step sizes, and proves weak convergence of the whole sequence when a zero exists (Rockafellar 1976).
1991: Güler constructs an example in which the iterates converge weakly but not strongly (Güler 1991).

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . Let $H'$ be its dual, and write $(\varphi, y)$ for the value of a functional $\varphi\in H'$ at $y\in H$ . Let $C\subseteq H$ be convex, closed and bounded, and let $T:H\to H'$ be

monotone on $C$ : $(Tx-Ty,\,x-y)\ge0$ for all $x,y\in C$ ;
hemicontinuous on $C$ : for all $x,y\in C$ , the map $t\mapsto T((1-t)x+ty)$ , $t\in[0,1]$ , is continuous into $H'$ with its weak topology.

The variational inequality (1) asks for $\bar x\in C$ such that

(T\bar x,\, x-\bar x)\ge 0\qquad\forall x\in C .

Its solution set is denoted $M$ (solSet T C in Lean).

Martinet's regularization algorithm starts from $x^0\in C$ . Given $x^n\in C$ , it determines $x^{n+1}\in C$ such that

(Tx^{n+1},\, x-x^{n+1})+\langle x^{n+1}-x^n,\, x-x^{n+1}\rangle\ge 0\qquad\forall x\in C. \tag{2}

In words, $x^{n+1}$ solves the variational inequality for the operator $T+(\,\cdot\,-x^n)$ , which is strongly monotone. A point $\tilde x$ is a weak cluster point of $(x^n)$ if every neighbourhood of $\tilde x$ in the weak topology contains $x^n$ for infinitely many $n$ .

Formalization targets

Goal: Théorème 1

\tilde x \text{ a weak cluster point of } (x^n)\ \Longrightarrow\ \tilde x\in M .

Every weak cluster point of the regularized iterates solves (1). The paper's Lemme 2 states the same thing. The goal assumes neither that (1) has a solution nor that $T$ is bounded on $C$ .

Milestones, in the order the paper uses them

§2.1: (1) has at least one solution when $C\neq\emptyset$ , so $M\neq\emptyset$ .
§2.2: the step (2) has exactly one solution $x^{n+1}\in C$ for every $x^n\in C$ .
§2.3, (5): Minty's characterization $M=\{\bar x\in C\mid (Tx,\,x-\bar x)\ge0\ \forall x\in C\}$ .
§2.3, (7): for every $\bar x\in M$ , $\|x^{n+1}-\bar x\|^2\le\|x^n-\bar x\|^2-\|x^{n+1}-x^n\|^2$ .
Lemme 1: $\|x^{n+1}-x^n\|\to0$ .
§2.3, (8): $\liminf_n (Tx^{n+1},\,x-x^{n+1})\ge0$ for every $x\in C$ .
§2.3, (9): $\liminf_n (Tx,\,x-x^{n})\ge0$ for every $x\in C$ .
Corollaire (stronger than the goal): if $M=\{\bar x\}$ , then $x^n\rightharpoonup\bar x$ .

Significance

The result. Théorème 1 is the first convergence theorem for the proximal point method. The method only needs to solve strongly monotone subproblems, and those are well posed even when the original problem is not. Together with the existence result, the theorem says the iterates accumulate weakly only at solutions. When the solution is unique, the whole sequence converges weakly (the Corollaire). The later theory of Rockafellar, Brézis–Lions and the splitting literature refines this statement.

Formalizing it. The result has been proved since 1970. What this mission adds is a machine-checked version that follows the original hypotheses: an operator into the dual, hemicontinuity rather than continuity, and no maximality assumption. The cited ingredients, the Lions–Stampacchia existence theorem in an infinite-dimensional Hilbert space and Minty's lemma, are not in Mathlib as far as this mission is aware. Formalizing them is part of the work and is reusable well beyond this paper. The milestone items on the platform are statements awaiting proof. None of them has a machine-checked proof yet.

Difficulty

Lemme 1 and inequality (7) follow from the defining inequality (2) and the algebra of the inner product. The difficulty is at two other points.

First, the iterates satisfy the variational inequality only approximately, and only with $T$ evaluated at the iterate. A weak cluster point gives no control over $Tx^{n}$ , because $T$ is merely hemicontinuous and is not assumed weakly continuous or bounded. The obvious idea, to pass to the limit in $(Tx^{n+1},\,x-x^{n+1})\ge -\varepsilon_n$ , fails for this reason. Passing to the limit requires the reformulation in which $T$ is evaluated at a fixed point of $C$ . That reformulation is Minty's characterization (5), and proving it uses hemicontinuity along segments.

Second, the proof of Lemme 1 needs a solution of (1) to exist. In infinite dimensions that is the Lions–Stampacchia theorem. Its standard proof goes through Brouwer's fixed point theorem on finite-dimensional sections together with weak compactness of $C$ , and this is the heaviest item of the mission.

Formalization scope

$H$ is a real Hilbert space: NormedAddCommGroup H, InnerProductSpace ℝ H, CompleteSpace H. The paper says only "espace de Hilbert". Its ordered inequalities force real scalars.
$H'$ is StrongDual ℝ H, and $(\varphi,y)$ is φ y. $T$ is not replaced by a map $H\to H$ through the Riesz isomorphism.
Hemicontinuity is weak-* continuity: for $x,y\in C$ and every $z\in H$ , the map $t\mapsto (T((1-t)x+ty),z)$ is continuous on $[0,1]$ . Since $H$ is reflexive, this is the paper's weak topology on $H'$ . It is not strengthened to continuity of $T$ .
The algorithm is a relation (IsRegSeq): any sequence with $x^0\in C$ that satisfies (2) at every step. Existence and uniqueness of the step are milestone 2, not built into a definition.
A weak cluster point is MapClusterPt in WeakSpace ℝ H, a cluster point in the weak topology. It is not a cluster point in the norm topology, which would make the goal weaker.
$\liminf_n a_n\ge0$ in (8) and (9) is stated as $\forall\varepsilon>0$ , eventually $a_n\ge-\varepsilon$ . Filter.liminf on $\mathbb R$ returns a junk value on sequences that are unbounded below.
"C nonempty" is added to the existence milestone. The paper leaves it implicit, and the claim is false for $C=\emptyset$ .
In Lean the sequence is called $x$ and an arbitrary point of $C$ is called $y$ . The paper uses the letter $x$ for both.

A trivializing formalization is ruled out. The goal does not assume $M\neq\emptyset$ , boundedness of $T$ , or strong cluster points. Its hypotheses are satisfiable: $H=\mathbb R$ , $C=[-1,1]$ , $(Tx,y)=xy$ , $x^n=2^{-n}$ is an instance, checked locally.

Not formalized: Remarques 1 and 2 of §II (a variable-weight variant of (2), whose printed form is apparently misprinted, and the removal of boundedness of $C$ under a coercivity condition), because the paper gives neither a proof. Théorème 2 (§III) and the convex-minimization §IV are not formalized either. §IV is the subject of the companion mission.

Contributions are welcome on each milestone, and especially on the general infrastructure: Minty's lemma, Hartman–Stampacchia/Lions–Stampacchia existence for monotone hemicontinuous operators, and the fact that bounded sequences in a Hilbert space have weak cluster points. A proved Brouwer fixed point theorem (AGT.brouwer_fixed_point) and a Banach–Alaoglu theorem (FamousTheorems.banach_alaoglu) are available on the platform as tools.

Selected references

B. Martinet, Brève communication. Régularisation d'inéquations variationnelles par approximations successives, Revue française d'informatique et de recherche opérationnelle, série rouge, 4(R-3) (1970), 154–158. https://doi.org/10.1051/m2an/197004R301541
J.-L. Lions, G. Stampacchia, Variational inequalities, Communications on Pure and Applied Mathematics 20 (1967), 493–519. https://doi.org/10.1002/cpa.3160200302
R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM Journal on Control and Optimization 14 (1976), 877–898. https://doi.org/10.1137/0314056
O. Güler, On the convergence of the proximal point algorithm for convex minimization, SIAM Journal on Control and Optimization 29 (1991), 403–419. https://doi.org/10.1137/0329022

10 thms2 active usersReviewed

Completed

Combinatorics Discrete Geometry Graph Theory·Captain: mikedeng1

The Geometry of Graphs and Some of Its Algorithmic Applications 3: The Complete Graph Kₙ Has Isometric Dimension ⌈log₂ n⌉Research Paper

Motivation

An isometric model of a graph assigns vectors to vertices so that vector distances reproduce shortest-path distances exactly. The choice of norm matters: a graph that needs many Euclidean coordinates may admit a smaller realization under a different norm. Linial, London, and Rabinovich used this freedom to study the dimension of graph metrics and related geometric questions in their 1995 paper on graph embeddings (Linial–London–Rabinovich, 1995). The complete graph is the first calibration point for the invariant. Every two distinct vertices are equally far apart, so the question becomes how many pairwise equidistant points an arbitrary real normed space of dimension $d$ can contain.

The answer is a sharp base-two logarithm. It separates the role of dimension from the particular shape of a norm's unit ball. In particular, a cube equipped with the supremum norm supplies many equidistant vertices, while no norm in the same dimension can accommodate more. Establishing both directions gives a reference case for more complicated graph metrics in the paper's Section 5.

Setting

A finite pseudometric space has a finite point set $X$ and a distance $\delta(x,y)\ge0$ that is symmetric, vanishes on the diagonal, and satisfies the triangle inequality. Distinct points may have distance zero, as the paper explicitly allows. A norm $N$ on $\mathbb R^d$ is nonnegative, vanishes only at the zero vector, is absolutely homogeneous, and satisfies the triangle inequality. It induces the distance $N(u-v)$ between vectors.

An isometric embedding of $(X,\delta)$ into a $d$ -dimensional normed space is a map $\varphi:X\to\mathbb R^d$ with $N(\varphi(x)-\varphi(y))=\delta(x,y)$ for every pair. The isometric dimension $\dim(X,\delta)$ is the least $d$ for which such a norm and map exist. The norm may depend on $X$ and $d$ ; it is part of the realization rather than a fixed background choice. Lemma 5.1 of the paper states that every $m$ -point metric space has an isometric realization in $\ell_\infty^m$ , so this least dimension is taken over a nonempty set (Linial–London–Rabinovich, p. 229).

The complete graph $K_n$ has an edge between every pair of distinct vertices. Its shortest-path distance is zero from a vertex to itself and one between distinct vertices. An isometric realization of $K_n$ is therefore a collection of $n$ points whose pairwise distances are exactly one. The paper's Section 5 treats connected graphs, so this mission takes $n\ge1$ . Its convention is that every logarithm has base two.

Formalization targets

Finite metric spaces have a realization

The foundational target is the paper's finite embedding statement:

|X|=m\quad\Longrightarrow\quad (X,\delta)\hookrightarrow\ell_\infty^m.

It establishes the domain on which the least-dimension definition has its intended meaning. The remaining milestones isolate the geometric assertions used for complete graphs: a difference-body inclusion, separation of the interiors of certain convex-hull translates, and a cardinality bound $n\le2^d$ for equilateral points in $\mathbb R^d$ .

Complete graph dimension

The goal is Proposition 5.4 (Linial–London–Rabinovich, p. 231):

\dim(K_n)=\lceil\log_2 n\rceil\qquad(n\ge1).

The lower bound applies to every real norm on $\mathbb R^d$ . The upper bound has the more specific target $K_n\hookrightarrow\ell_\infty^{\lceil\log_2 n\rceil}$ . Both inequalities, including $n=1$ and dimension zero, are part of the mission.

Significance

The equation determines the optimal dimension for an equilateral finite metric space when the norm is unrestricted. It also bounds the size of an equilateral set in every $d$ -dimensional real normed space by $2^d$ , with equality attainable by vertices of a binary cube under the supremum norm. For graph metrics, it gives a precise baseline against which dimension bounds for trees, cubes, and other connected graphs can be compared. The surrounding section of the paper uses the same geometric vocabulary for those other families (Linial–London–Rabinovich, Section 5).

The mathematical result is proved in the 1995 paper. This mission asks for machine-checked Lean proofs of the specified statements. The local declarations presently encode open proof obligations; compilation checks their types and imports, but does not establish the theorems. A completed development would provide a reusable interface for finite isometric dimension and for equilateral configurations under arbitrary finite-dimensional norms.

Difficulty

The easy direction uses points of a binary cube. The difficult direction must hold uniformly over every possible norm, whose unit ball need not be round or smooth. A direct coordinate count cannot assume that vectors have bounded entries in a prescribed basis. The paper formulates its argument through the convex hull of an equilateral configuration and a comparison of translated sets (Linial–London–Rabinovich, p. 231). Its printed volume line also leaves a degenerate case: if that convex hull has zero volume in the ambient space, cancellation of $\operatorname{vol}(D)$ gives no numerical bound. A complete formal proof must account for such configurations without weakening the theorem to full-dimensional sets.

Formalization scope

The Lean representation of $\mathbb R^d$ is the function space Fin d → ℝ. A norm is an explicit function with all norm axioms, including definiteness and absolute homogeneity. Isometric dimension takes the infimum over dimensions admitting such a norm and an exact distance-preserving map. The complete graph is Mathlib's ⊤ : SimpleGraph (Fin n); its graph distance is converted to a real number. This distance is the discrete zero-or-one metric. The lower bound quantifies over every explicit norm. The cube milestone uses the supremum norm on finite real coordinate vectors. Convex hulls and interiors use the standard topology of this finite-dimensional vector space, which every norm induces.

The formal goal assumes $n\ge1$ , matching the paper's connected-graph convention; $n=1$ remains included, with dimension zero. The logarithmic expression is Nat.clog 2 n, the ceiling of the base-two logarithm, rather than a floor or a real logarithm. The source uses no unspecified asymptotic constant in Proposition 5.4 or its listed milestones. The empty point space is allowed in the general finite embedding lemma; its pairwise claim is vacuous, while the nonempty cases carry the intended content. The dimension definition is only used for realizable finite distances, so a totalized infimum's value on an unrealizable function has no role in the target.

The exact norm axioms and exact distance equality prevent shortcuts through seminorms, truncated distances, or a weaker distortion bound. The cardinality theorem retains lower-dimensional affine configurations; assuming positive ambient volume would discard part of the result. A complete development needs finite pseudometric geometry, the supremum norm, convex hulls and interiors, and a dimension-sensitive measure argument. Those components are useful beyond this graph. The paper's independent results on degrees, trees, cubes, and other graph families, as well as algorithmic running-time claims elsewhere in the article, are outside this mission.

Selected references

N. Linial, E. London, and Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2), 215–245 (1995). DOI: 10.1007/BF01200757.

9 thms2 active usersReviewed

Completed

Captain: savarin

Sharp diagonal Hlawka constants: lower the cutoff to 80Open Problem

The Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.

This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real $p\ge85$ , also holds for every real $p\ge80$ . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three $3\times3$ diagonal matrices. Because the cutoff-85 mission already covers every $p\ge85$ , the new work is the range from 80 to 85.

The cutoff came down from 90 to 85 in two days, through moona3k's proofs at 89, 88, 87 and 85. The step to 89 sharpened the estimates of the cutoff-90 argument. The step to 85 added a new idea, a weighted pair-curvature and confinement estimate. How far that idea reaches is not known; 80 asks for five more units. The goal theorem below gives the exact statement.

This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 80 or lower also settles this mission.

The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.

References

K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv preprint, 2012, §8.2, Problem 7. arXiv:1201.5232
Ezzeri Esa, Hlawka–Schatten inequalities: sharp diagonal construction, Lean source repository, 2026, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library
Ezzeri Esa and project contributors, The cyclic bound for every real p ≥ 90, research note with appendices and exact certificates, 2026. Research note

Established results on Prove2Me

64 thms2 active usersReviewed

Completed

Captain: moona3k

Sharp diagonal Hlawka constants: lower the cutoff to 84Open Problem

This entry lowers the sufficient exponent cutoff for the sharp diagonal Hlawka formula from85 to84. For every real p≥84, the foundation's unchanged cyclic constant is the least constant comparing the triple deficit with the pair-deficit sum for every complex coordinate triple in every finite dimension.

The statement includes unequal and zero input vectors and dimension zero. It concerns complex diagonal matrices through their coordinate norms; it does not settle the conjectured cutoff2 or the full noncommutative matrix problem.

Goal and companion

Exact complex cutoff84 goal.
Real coordinate bound for p≥84, the supporting milestone.

Both exact proof submissions have been ACCEPTED by Prove2Me, and both theorem records are Proved. Their accepted sources match the submitted files and exact target statements in the pinned environment. This proposal references those existing verified results; the remaining steps are human submission and campaign moderation.

Construction and proof route

The construction is by Ezzeri Esa (GitHub savarin), with the accepted cutoff90 formalization by BrunoDCDO. Claude Opus5.5 produced moona3k's accepted89,88,87 work. Codex's accepted85 continuation and new84 extension reuse their verified generic calculus and transfer arguments.

On[84,85], an exact rational matrix sum-of-squares certificate proves a coupled radial energy estimate throughout a larger localization box. Residual estimates give nonnegative actual deficit Hessians and box convexity. Tight logarithm/Taylor bounds and exact positive Bernstein certificates localize every normalized failure. Orbit averaging and circle transfer prove the real and complex bounds, and the cyclic obstruction establishes leastness. The accepted85 development supplies the remaining tail.

Campaign context

The campaign began with cutoff256, followed by90,89,87,85. This entry instantiates its exact template with84 over the same foundation definitions.

Sharp diagonal Hlawka campaign

5 thms2 active usersReviewed

Completed

Algorithmic Game Theory Probability·Captain: mikedeng1

Existence of Correlated Equilibria II: A Game with Finite Strategy Sets and Continuous Payoffs Has a Countably Additive Correlated Equilibrium, However Many PlayersResearch Paper

Motivation

A correlated equilibrium describes a recommendation scheme for a game: a common random device selects a profile of actions, tells each player only their own recommended action, and no player gains in expectation by replacing that recommendation with another action. This makes sense even when there are infinitely many players. The finite-player existence theorem, however, does not settle what happens to a probability distribution on the product of infinitely many strategy sets, or whether that distribution is countably additive. Hart and Schmeidler proved that continuous payoffs and finite individual strategy sets suffice, with no countability assumption on the player set. Their Theorem 2(ii) is the target here.

The distinction between correlation and independent play is material. Peleg's 1969 paper studied equilibrium points with infinitely many players. Hart and Schmeidler reproduce a discontinuous binary-action example with no Nash equilibrium yet a countably additive correlated equilibrium, then change its payoffs to obtain a game with no countably additive correlated equilibrium. Those examples explain why the measure class and payoff regularity in the theorem need to be stated precisely. The modified example is an additional target of this mission. The main existence theorem is already proved in the 1989 paper; the mission asks for a machine-checked formalization of that known result and its selected proof steps.

Setting

Let $N$ be a nonempty set of players, possibly uncountable. Player $i\in N$ has a nonempty finite set $S^i$ of pure strategies. A strategy profile is a tuple $s\in S=\prod_{i\in N}S^i$ . A game specifies a real payoff $h^i(s)$ for every player and profile. Each $S^i$ has the discrete topology; $S$ has the product topology. Write $\Sigma_0$ for the product σ-algebra, generated by cylinder events that inspect finitely many coordinates. It can be strictly smaller than the Borel σ-algebra of $S$ when $N$ is uncountable.

For $r^i,t^i\in S^i$ , write $(s^{-i},t^i)$ for the profile obtained by replacing only the $i$ th coordinate of $s$ by $t^i$ . A countably additive probability measure $p$ on $(S,\Sigma_0)$ is a correlated equilibrium when every recommendation $r^i$ gives a nonnegative expected advantage over switching to $t^i$ :

\int_{\{s:s^i=r^i\}}\left[h^i(s)-h^i(s^{-i},t^i)\right]\,dp(s)\ge 0.

The inequality is weighted by the probability of receiving $r^i$ ; it remains meaningful when that probability is zero. The integrand must be integrable on this cylinder. In the theorem, continuity and compactness provide the boundedness and measurability needed for the integral. For the separate discontinuous example, integrability is checked as part of the equilibrium condition.

Formalization targets

Theorem 2(ii): countably additive existence

For arbitrary nonempty $N$ , finite nonempty $S^i$ , and continuous payoffs $h^i:S\to\mathbb R$ , the goal is

\exists p\in\mathcal P_{\sigma}(S,\Sigma_0)\quad \forall i\in N\ \forall r^i,t^i\in S^i, \quad \int_{\{s:s^i=r^i\}}[h^i(s)-h^i(s^{-i},t^i)]\,dp(s)\ge0.

Here $\mathcal P_{\sigma}$ denotes countably additive probability measures. The supporting targets follow the source's proof: every finite-restriction game has an equilibrium, a family of such equilibrium measures has a cluster point when tested against continuous real functions, and that cluster point satisfies the incentive inequalities. The cluster statement tests finite collections of functions, which is what a neighborhood in the weak topology requires.

Example 2: the continuity boundary

Players $i=1,2,\ldots$ choose $s^i\in\{0,1\}$ . Let Case 1 mean that only finitely many players choose $1$ . The payoff is $s^i/i^2$ in Case 1 and $-s^i$ otherwise. The additional target states

\nexists\text{ a countably additive correlated equilibrium on }(S,\Sigma_0).

Theorem 2(i), which asserts existence for bounded measurable payoffs using a finitely additive probability on a larger algebra, is outside this proposal. It is a different conclusion requiring finitely additive integration.

Significance

Theorem 2(ii) gives an equilibrium distribution that is an ordinary countably additive probability measure, while allowing arbitrarily many players. It lets the same incentive test be applied to each player's observable recommendation event, without replacing the product σ-algebra by a larger space of events. Example 2 shows the statement changes when continuity is dropped: bounded measurable binary payoffs alone do not guarantee a countably additive equilibrium. Both claims are established in the source paper.

Formalizing the result produces reusable interfaces for probability measures on products of finite strategy spaces, finite-support equilibrium distributions, and weak tests by continuous functions. The local Lean files compile as statements; the goal and milestone theorems remain open for machine-checked proofs. Platform work on finite Nash and correlated equilibria, including AGT.nash_existence, AGT.IsCorrelatedEquilibrium, Aumann1987.*, and CalibratedCE.*, supplies related vocabulary but uses finite-player or different distribution conventions. None of those declarations is used as a substitute for this theorem about an arbitrary player set.

Difficulty

Finite strategy sets do not make the full profile space finite when the player set is infinite. A direct finite-game argument therefore supplies only finite restrictions, and an arbitrary limit of their distributions may lose either countable additivity or the incentive inequalities if the topology and σ-algebra are handled carelessly. Continuity is what makes the payoff-difference tests compatible with the weak topology on measures. The paper's discontinuous Example 2 rules out the tempting extension from continuous to merely bounded measurable payoffs.

Formalization scope

Profiles have Lean type ∀ i, S i; payoffs have type ι → (∀ i, S i) → ℝ. The theorem assumes [Nonempty ι], a finite nonempty strategy type for each player, discrete topologies and discrete measurable structures on the factors, and continuity of every payoff on the product. It does not assume Countable ι. The default Pi measurable structure is $\Sigma_0$ . Measures are Mathlib's countably additive Measure, with IsProbabilityMeasure. IsCorrelatedEq includes IntegrableOn explicitly, because an undefined Bochner integral otherwise evaluates to zero in Lean and could make the equilibrium condition empty.

An f-set has a nonempty finite strategy subset at every coordinate and differs from a singleton at only finitely many coordinates. Finite weighted profiles represent its equilibrium measure; this avoids treating a profile singleton as measurable in an uncountable product. For the cluster-point statements, f-sets contain a fixed anchor profile $\hat s$ . The paper orders all f-sets by inclusion and calls them a net, but that index set is not directed: two singleton products can disagree at infinitely many coordinates. Anchored f-sets are directed and admit every finite coordinate demand used in the argument. This repair is explicit in the milestone statements and audit notes. Neither the goal nor the equilibrium definition depends on the chosen anchor.

The development needs product topology and σ-algebra facts, finite-game correlated-equilibrium existence, compactness for probability measures tested by continuous functions, and finite-sum-to-integral connections. Contributions proving these steps or the main theorem are in scope. The finitely additive conclusion of Theorem 2(i), Peleg's first example, and the paper's noncountably additive example measure are not formalized here. A sorry-free check supplies a concrete two-player coordination game and a correlated equilibrium, demonstrating that the main hypotheses are satisfiable.

Selected references

Sergiu Hart and David Schmeidler, Existence of Correlated Equilibria, Mathematics of Operations Research 14 (1989), 18–25. DOI: 10.1287/moor.14.1.18.
Bezalel Peleg, Equilibrium Points for Games with Infinitely Many Players, Journal of the London Mathematical Society s1-44 (1969), 292–294. DOI: 10.1112/jlms/s1-44.1.292.

7 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Nonlinear Proximal Point Algorithms Using Bregman Functions, with Applications to Convex Programming 1: The Bregman Proximal Point Algorithm Converges to a Zero of a Maximal Monotone OperatorResearch Paper

Motivation

The proximal point algorithm is a way to find a zero of a set-valued monotone operator by repeatedly solving a regularized version of that operator equation. Its classical regularizer is quadratic, so the distance from one iterate to the next is Euclidean. In convex optimization, that geometry can be poorly matched to the domain: the natural iterates may be constrained to a positive orthant, a simplex, or an open set with a meaningful boundary. Eckstein's 1993 paper studies what happens when a Bregman function supplies the regularization instead. The convergence question matters because the later multiplier methods in the same paper are instances of this general iteration. Eckstein (1993) develops the general result before applying it to convex programs.

The result considered here is Theorem 1 of that paper. It concerns an existing infinite run: it states what such a run does, while Theorems 4 and 5 address conditions under which a run can be generated. This separation keeps the convergence assertion precise. The result is known mathematically; the mission asks for a Lean proof of its stated generality, including its alternative when the operator has no zero.

Setting

Work in a finite-dimensional real inner-product space $H$ , representing the paper's $\mathbb R^n$ . A monotone operator $T:H\to 2^H$ associates a set $T(x)$ of vectors with each point. It is monotone when $\langle x-y,u-v\rangle\ge0$ for every $u\in T(x)$ and $v\in T(y)$ , and maximal monotone when its graph has no proper monotone extension. Its domain is $\operatorname{dom}T=\{x:T(x)\ne\varnothing\}$ ; a zero is a point $z$ with $0\in T(z)$ .

Let $S\subseteq H$ be open and $h$ a real function on $\overline S$ . At $y\in S$ , define the Bregman distance

D_h(x,y)=h(x)-h(y)-\langle\nabla h(y),x-y\rangle,\qquad x\in\overline S.

It need not be symmetric and is generally not a metric. Definition 1 requires $h$ to be continuously differentiable on $S$ , strictly convex and continuous on $\overline S$ , and to satisfy boundedness of both kinds of partial $D_h$ sublevel sets. Two sequential conditions connect convergence in $H$ to convergence of Bregman distances, including sequences approaching the boundary of $S$ . These six requirements together define a Bregman function with zone $S$ .

A Bregman proximal-point run uses positive parameters $c_k$ and a sequence $x^k\in S$ satisfying

\frac{\nabla h(x^k)-\nabla h(x^{k+1})}{c_k}\in T(x^{k+1}),\qquad k=0,1,\ldots.

This is the inclusion form (4) of the paper's recursion (3). It permits set-valued $T$ and does not assert that a next iterate exists for arbitrary starting data. The model also uses the paper's standing domain condition $\operatorname{dom}T\subseteq\overline S$ .

Formalization targets

The main target is Theorem 1. Assume that the positive parameters have a common positive lower bound and that one of the following conditions holds: (C1) $\overline{\operatorname{dom}T}\subseteq S$ , or (C2) $T=\partial f$ for a proper lower semicontinuous convex extended-valued function $f$ . Then

\begin{aligned} T^{-1}(0)\ne\varnothing &\quad\Longrightarrow\quad x^k\longrightarrow z\text{ for some }z\in T^{-1}(0),\\ T^{-1}(0)=\varnothing\text{ and (C1)} &\quad\Longrightarrow\quad \{x^k:k\ge0\}\text{ is unbounded}. \end{aligned}

The second line retains the paper's extra (C1) requirement. The standing inclusion $\operatorname{dom}T\subseteq\overline S$ has a different direction and role. The milestone list follows Lemma 1 and the three labelled steps of Theorem 1's convergence proof: the resolvent inequality, boundedness of the run when a zero exists, identification of every limit point as a zero, and convergence of the full run. The no-zero alternative remains in the goal because restating that conjunct as a separate milestone would add no independent target.

Significance

Theorem 1 says that the nonlinear iteration cannot remain bounded without approaching a zero under (C1), and that when a zero exists the whole sequence converges under either (C1) or (C2). This is stronger than saying only that accumulation points solve the operator equation. It supplies a common convergence result for the paper's later proximal minimization and multiplier algorithms, where the operator is often a subdifferential and the geometry comes from a nonquadratic $h$ . Eckstein (1993) gives those applications after the general theorem.

A formalization would add a reusable interface for Bregman functions with open zones, including their boundary behavior, and for proximal-point runs of set-valued maximal monotone operators. The published platform definitions of monotone operators and extended-valued convex analysis are reused. The new proof work is the Bregman resolvent estimate and the convergence alternative at Theorem 1's level of generality. No machine-checked proof of this specific theorem is claimed here.

Difficulty

The usual Euclidean proximal-point theorem does not apply directly after changing coordinates by $y=\nabla h(x)$ : the transformed operator need not remain monotone, as the paper observes after Theorem 1. A proof must account for the nonsymmetric $D_h$ , the possible boundary of $S$ , and two distinct ways to identify a limit point as a zero. Under (C1), the point lies where the gradient is continuous; under (C2), the argument uses the subdifferential structure instead. The no-zero case has its own difficulty because boundedness would have to contradict maximal monotonicity without first assuming that a zero exists. The proof cites a closed-graph result for maximal monotone operators and a zero-existence fact for operators with bounded domain; those external facts are groundwork for solvers, not invented milestones.

Formalization scope

Lean uses a finite-dimensional real inner-product space rather than a coordinate-fixed $\mathbb R^n$ . The total function $h:H\to\mathbb R$ is constrained only on $\overline S$ ; its gradient is evaluated only on the open zone $S$ . The Bregman distance is used on $\overline S\times S$ . Definition 1's condition (vi) explicitly places its first sequence in $\overline S$ , the natural domain stated immediately after the definition. The run explicitly keeps every $x^k$ in $S$ and encodes recursion (3) using the equivalent inclusion (4). A positive lower bound on $c_k$ is expressed by one $\varepsilon>0$ with $c_k\ge\varepsilon$ for every $k$ .

The operator $T$ is a published set-valued operator object, with its published notions of monotonicity, maximality, domain, and zeros. The proper and convex extended-valued function in (C2) uses the published epigraph and subgradient definitions, with EReal able to express $+\infty$ . Subdifferentials are built from those definitions. A limit point means a limit along a strictly increasing subsequence, and unboundedness means that the full set of iterates is not bounded. The proof step on p. 207 prints $T^{-1}(0)\subseteq S$ ; the formal Step 1 uses the standing condition $T^{-1}(0)\subseteq\overline S$ , which is sufficient for the Bregman distance and also covers (C2).

The run relation cannot be satisfied by an arbitrary constant sequence: its inclusion must hold at every step, and a zero-free operator under (C1) triggers the unbounded conclusion. Nor does the theorem replace convergence by existence of one convergent subsequence. Reusable contributions include properties of the Bregman resolvent and maximal-monotone graph limits. Theorem 5's separate existence and minimization claims are outside this mission's core.

Selected references

Jonathan Eckstein, Nonlinear proximal point algorithms using Bregman functions, with applications to convex programming, Mathematics of Operations Research 18(1), 202–226, 1993. DOI: 10.1287/moor.18.1.202.

8 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Convex Programming in Hilbert Space: Gradient Projection x_{k+1} = P(x_k − ρ_k∇f(x_k)) with σ ≤ ρ_k ≤ 2ρ₀ − σ Stays in the Level Set, and for Convex f Drives f(x_k) to inf_C fResearch Paper

Motivation

Minimizing a smooth function over a closed convex set is the basic problem of constrained continuous optimization. When the constraint set is simple enough that the nearest point of the set to any given point can be computed (a ball, a box, an orthant, an affine subspace), the most direct method is the gradient projection method: take a gradient step and project back onto the set. The method is the ancestor of the projected gradient and proximal gradient algorithms used today in signal processing, machine learning, and optimal control, where the variable is often a function, so that the natural setting is an infinite-dimensional Hilbert space rather than $\mathbb R^n$ .

A. A. Goldstein's 1964 note in the Bulletin of the AMS (Goldstein 1964) is one of the two founding papers of the method, alongside the independent work of Levitin and Polyak (1966). It states, in a Hilbert space and with an explicit step-size window, that the iterates stay in the initial level set, that the objective values converge, and that under convexity they converge to the optimal value, with weak and strong convergence of the iterates under further hypotheses. Goldstein motivates the method by applications to control theory (Balakrishnan 1963; Goldstein, Minimizing functionals on Hilbert space, 1964).

Timeline.

1959: Cheney and Goldstein study proximity maps (metric projections) onto convex sets and a fixed-point construction for the distance between two convex sets (Cheney–Goldstein 1959, cited by the note as [1]).
1964: Goldstein, this note: the gradient projection method in Hilbert space with steps in $[\sigma, 2\rho_0 - \sigma]$ .
1966: Levitin and Polyak give the same method and convergence rates for constrained minimization.
1987: Calamai and Moré extend the analysis to Armijo-type step rules and identification of the active constraints in $\mathbb R^n$ (Calamai–Moré 1987).

Setting

Let $H$ be a real Hilbert space with inner product $[x, y]$ and norm $\|x\|$ . Let $C \subseteq H$ be closed and convex, and let $P : H \to H$ be the projection onto $C$ : $P(x)$ is the point of $C$ closest to $x$ . In Lean, IsProjection C P says that $P(x) \in C$ and $\|x - P(x)\| \le \|x - y\|$ for all $y \in C$ .

Let $f : H \to \mathbb R$ , $x_0 \in C$ , and let

S = \{x \in C : f(x) \le f(x_0)\}

be the level set (levelSet f C x0). Let $\hat S$ be an open set containing the convex hull of $S$ . Write $f'(x, h)$ for the Fréchet derivative of $f$ at $x$ applied to $h$ , $\nabla f(x)$ for the gradient (so $f'(x, h) = [\nabla f(x), h]$ ), and

f''(x, h, h) = \frac{d}{dt}\Big|_{t=0} f'(x + th, h)

for the directional second derivative in the sense of Gâteaux (d2 f x h). The curvature hypothesis is that for some $\rho_0 > 0$ , at every $x \in \hat S$ and for every $h \in H$ , these derivatives exist and

|f''(x, h, h)| \le \frac{\|h\|^2}{\rho_0}.

Choose $0 < \sigma \le \rho_0$ and step sizes $\sigma \le \rho_k \le 2\rho_0 - \sigma$ . The method is

x_{k+1} = P\big(x_k - \rho_k \nabla f(x_k)\big), \qquad k \ge 0.

A point $z \in C$ is stationary if $P(z - \rho \nabla f(z)) = z$ for every $\rho > 0$ .

Formalization targets

Goal: the THEOREM, parts (i)–(v)

Assume $f$ is bounded below and continuous on $C$ . There is $L \in \mathbb R$ such that

(i) $x_k \in S$ for all $k$ , $x_{k+1} - x_k \to 0$ , and $f(x_k)$ decreases to $L$ ;
(ii) if $S$ is compact, every cluster point $z$ of $(x_k)$ near which $\nabla f$ is continuous is stationary, and a unique cluster point is the limit of $(x_k)$ ;
(iii) if $S$ is convex and $f''(x, h, h) \ge \mu \|h\|^2$ on $S$ for some $\mu \ge 0$ , then

L = \inf\{f(x) : x \in C\};

(iv) under (iii) with $S$ bounded, every weak cluster point of $(x_k)$ minimizes $f$ on $C$ ;
(v) under (iii) with $\mu > 0$ and $\nabla f$ bounded on $S$ , there is $z \in S$ with $f(z) = L$ , $x_k \to z$ in norm, and $z$ is the unique minimizer of $f$ on $C$ .

The goal is the whole theorem, because its five parts share one limit $L$ and one standing setting.

Milestones

The projection inequality $[x - y, P(x) - y] \ge \|P(x) - y\|^2$ for $y \in C$ ; the Lipschitz property of $P$ ; the characterization of stationarity for convex $f$ at a differentiability point; the one-step Taylor estimate; the step lemma (for $\sigma \le \rho \le 2\rho_0 - \sigma$ the new point stays in $S$ and the decrease is at least $\|x_{k+1} - x_k\|^2 \sigma / 4\rho_0^2$ ); parts (i) and (ii); the strong-convexity bound $f(x) \ge f(y) + [\nabla f(y), x - y] + \frac12\mu\|x - y\|^2$ on $S$ ; the supporting-hyperplane inequality of the proof of (iii); parts (iii), (iv) and (v). A companion item states the last clause of (ii) under convexity of $f$ on $C$ .

Significance

The result. The theorem gives a step-size rule that needs only a curvature bound near the level set, not a global Lipschitz constant of the gradient, and it covers the infinite-dimensional case directly: (iii) gives convergence of the objective values to the optimal value without assuming that a minimizer exists, (iv) yields minimizers as weak cluster points when the level set is bounded, and (v) gives strong convergence of the iterates under strong convexity on the level set. These are the prototypes of the convergence statements now proved for projected and proximal gradient methods.

Formalizing it. The result is classical and proved on paper; it has no machine-checked proof. The note is two pages long and its proof is terse ("The proof of (ii) being straightforward"), and checking it in Lean exposes two places where the printed statement needs repair (see Formalization scope). A complete development also produces reusable infrastructure: the variational inequality and Lipschitz property of the metric projection in a Hilbert space, a one-dimensional Taylor estimate from a Gâteaux second derivative along a segment, and weak lower semicontinuity of convex continuous functions on closed convex sets used through cluster points in WeakSpace.

Difficulty

The obvious argument for (i) applies a quadratic upper bound for $f$ along the segment from $x_k$ to $x_{k+1}$ . That bound is only available where the curvature hypothesis holds, on $\hat S$ , and nothing guarantees in advance that $x_{k+1}$ , or the segment, lies in $\hat S$ . Ruling this out requires control of $f$ up to the boundary of the level set, which the printed hypotheses do not give; this is where the added continuity hypothesis enters. In (iii) the iterates may be unbounded and no minimizer need exist, so compactness arguments are unavailable. In (iv) the cluster points are weak, so norm-closedness arguments do not apply directly.

Formalization scope

$H$ is a real Hilbert space: [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]. The inner product $[x, y]$ is ⟪x, y⟫_ℝ, and $\nabla f$ is Mathlib's gradient f.
$P$ is any map with IsProjection C P; there is no chosen projection and no junk value.
$f''(x, h, h)$ is the derivative at $t = 0$ of $t \mapsto f'(x + th, h)$ . The hypothesis on $\hat S$ (SecondDerivBound) states both differentiabilities before the bound, so the bound is never on a junk zero.
The run starts at $x_0$ , and $0 < \sigma \le \rho_0$ makes the step window nonempty.
" $L = \inf$ " is IsGLB (f '' C) L. Weak cluster points are cluster points in WeakSpace ℝ H.
Added hypothesis: $f$ is continuous on $C$ . Part (i) as printed is false without it: on $H = C = \mathbb R$ with $P = \mathrm{id}$ , $f(x) = (x - 2)^2$ for $x < 1$ and $f(x) = 100$ for $x \ge 1$ , $x_0 = 0$ , $\hat S = (-1, 1)$ , $\rho_0 = 1/2$ , $\sigma = 1/4$ , $\rho_k = 1/2$ , the first step lands at $x_1 = 2$ with $f(x_1) = 100 > f(x_0)$ .
Moved clause. The last clause of (ii), " $z$ minimizes $f$ on $C$ ", is false for nonconvex $f$ (a unique cluster point can be a stationary point that is not a minimizer). The goal omits it, and a companion item states it under convexity of $f$ on $C$ .
The goal assumes nothing about the step decrease, the step size $\hat\rho$ of the proof, or the iterates beyond the run's definition. A formalization that adds such facts as hypotheses, or that proves only one of the five parts, does not count as closing the goal.

Contributions welcome: proofs of any milestone, in particular the projection inequality and Lipschitz property (independent of the rest), the Taylor estimate from the Gâteaux second derivative, and the weak-closedness argument of (iv).

Selected references

A. A. Goldstein, Convex programming in Hilbert space, Bull. Amer. Math. Soc. 70 (1964), 709–710. https://doi.org/10.1090/s0002-9904-1964-11178-2
E. W. Cheney and A. A. Goldstein, Proximity maps for convex sets, Proc. Amer. Math. Soc. 10 (1959), 448–450.
A. V. Balakrishnan, An operator theoretic formulation of a class of control problems and a steepest descent method of solution, J. SIAM Control Ser. A 1 (1963), 109–127.
E. S. Levitin and B. T. Polyak, Constrained minimization methods, USSR Comput. Math. Math. Phys. 6(5) (1966), 1–50.
P. H. Calamai and J. J. Moré, Projected gradient methods for linearly constrained problems, Math. Programming 39 (1987), 93–116. https://doi.org/10.1007/BF02592073

14 thms2 active usersReviewed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

A Variational Inequality Formulation of the Dynamic Network User Equilibrium Problem I: Route-Departure Equilibria Are Exactly the Solutions of the Path-Integral Variational InequalityResearch Paper

Motivation

Commuters choose not only a route but also a departure time, trading travel delay against the penalty of arriving early or late. Static traffic assignment, in the tradition of Wardrop's user-equilibrium principle, ignores the time dimension; dynamic traffic assignment adds it, and its central modelling question is what "equilibrium" means when flows, delays and costs all vary over a time horizon. Friesz, Bernstein, Smith, Tobin and Wie (Oper. Res. 41(1), 1993) proposed the simultaneous route-departure (SRD) equilibrium of a path-based dynamic model and showed that it is equivalent to an infinite-dimensional variational inequality. That equivalence is the starting point of a large literature on dynamic user equilibrium: existence theory, solution algorithms and differential-variational formulations all take the variational inequality as their definition of the problem.

Timeline, as far as this mission is concerned:

1952: Wardrop states the static user-equilibrium criterion (equal and minimal travel times on used routes).
1979–1980: Smith and Dafermos formulate static user equilibrium as a finite-dimensional variational inequality.
1989: Friesz, Luque, Tobin and Wie treat dynamic route choice with a fixed departure schedule as an optimal-control problem.
1993: Friesz et al. (this paper) formulate simultaneous route and departure-time equilibrium and prove its equivalence with a variational inequality on $(L^2[0,T])^{|P|}$ (Theorem 2, p. 187).

Setting

A traffic network has a finite set $P$ of paths. Each path $p$ connects exactly one origin–destination (OD) pair $kl$ ; $P_{kl}$ denotes the paths of pair $kl$ . Travellers depart during the horizon $[0,T]$ , $T>0$ , which carries Lebesgue measure $\nu$ ; " $\forall_\nu(t)$ " means "for $\nu$ -almost every $t\in[0,T]$ ".

A vector of departure-time densities $h=(h_p)_{p\in P}$ assigns to each path a square-integrable, almost everywhere nonnegative function $h_p$ on $[0,T]$ : $h_p(t)$ is the rate at which travellers depart at time $t$ on path $p$ . The set of such vectors is $H_+$ . Each OD pair has a fixed travel demand $Q_{kl}$ , and the feasible set is

\Lambda=\Big\{h\in H_+ : \sum_{p\in P_{kl}}\int_0^T h_p(t)\,d\nu(t)=Q_{kl}\ \text{for every OD pair } kl\Big\}.\qquad(38)

A cost operator gives the effective delay $C_p(t,h)\ge 0$ of departing at time $t$ on path $p$ when the densities are $h$ : travel time plus a penalty for early or late arrival (13). Because densities are defined only up to null sets, the relevant lowest achievable cost on a path is an essential infimum,

\mu_p(h)=\operatorname{ess\,inf}\{C_p(t,h):t\in[0,T]\}=\sup\{x\in\mathbb R:\ \nu\{t: C_p(t,h)<x\}=0\},

and the lowest achievable cost for pair $kl$ is $\mu_{kl}(h)=\min_{p\in P_{kl}}\mu_p(h)$ .

Definition 3. For $h\in\Lambda$ and a nonnegative vector $\mu=(\mu_{kl})$ , the pair $(h,\mu)$ is an SRD equilibrium if for every OD pair $kl$ and every $p\in P_{kl}$ :

h_p(t)>0\ \Rightarrow\ C_p(t,h)=\mu_{kl}\quad\forall_\nu(t),\qquad C_p(t,h)\ge\mu_{kl}\quad\forall_\nu(t).

No positive-measure set of travellers can lower its cost by switching route or departure time.

Formalization targets

Goal: Theorem 2 (PIE VIP)

For $h^*$ with nonnegative, square-integrable costs $C_p(\cdot,h^*)$ :

\big(\exists\,\mu^*:\ (h^*,\mu^*)\ \text{SRD equilibrium}\big)\ \Longrightarrow\ h^*\in\Lambda\ \text{and}\ \sum_{p\in P}\int_0^T C_p(t,h^*)\,[h_p(t)-h^*_p(t)]\,d\nu(t)\ge 0\ \ \forall h\in\Lambda,\qquad(39)

and conversely, if $h^*\in\Lambda$ solves (39), then $(h^*,\mu(h^*))$ with $\mu^*_{kl}=\mu_{kl}(h^*)$ is an SRD equilibrium. The formal goal states the two directions as two conjuncts; the second names the equilibrium cost vector explicitly, which is stronger than an equivalence with an existential $\mu^*$ .

Milestones

Lemma 2: a measurable function positive on a set of positive measure exceeds some $\varepsilon_0>0$ on a set of positive measure.
The pointwise inequality (42) at an equilibrium, and the necessity half of Theorem 2.
Condition (17) holds by construction for $\mu^*=\mu(h^*)$ .
The positive-measure sets (44)–(46) and (47) produced by a failure of (16).
Feasibility (50) of the mass-shifted vector (48)–(49), the value bound (54), and the sufficiency half of Theorem 2.

Significance

The result. Theorem 2 converts an equilibrium defined by almost-everywhere complementarity conditions into a single variational inequality over a convex subset of a Hilbert space. This is what makes dynamic user equilibrium accessible to the general theory of variational inequalities: existence via monotonicity or compactness arguments, and projection-type algorithms in function space or after time discretization. The sufficiency half also identifies the equilibrium cost levels: they are the essential infima $\mu_{kl}(h^*)$ , so the multiplier $\mu^*$ need not be found separately.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known. A formal proof requires essential infima, the shifting of mass between paths on sets of prescribed measure (the paper cites Halmos, Proposition 41.2, for the nonatomicity of Lebesgue measure), and careful integrability bookkeeping. The development is a self-contained template for "complementarity conditions a.e. ⇔ variational inequality in $L^2$ " arguments, which recur in continuous-time equilibrium models.

Difficulty

Necessity is routine once integrability is in place, though the paper's text asserts the per-path identity $\int_0^T[h_p-h^*_p]\,d\nu=0$ , which is false; only the sum over $P_{kl}$ vanishes, and that suffices. Sufficiency is the substantive half. The obvious approach, testing (39) against a perturbation that moves flow from an expensive to a cheap route, has to be carried out with sets rather than points: the costs are only defined almost everywhere, the minimal cost is an essential infimum that need not be attained at any time, and the perturbation must keep the demand constraints exact. This forces the choice of sets of exactly equal positive measure inside the positive-measure sets $S_p(\varepsilon,\delta)$ and $T_q(\varepsilon)$ , a nonatomicity argument that a pointwise proof would miss.

Formalization scope

Densities are plain functions $\mathbb R\to\mathbb R$ with a square-integrability condition with respect to $\nu=$ Lebesgue measure restricted to $[0,T]$ , not $L^2$ equivalence classes; every pointwise condition is $\nu$ -almost everywhere, and values outside $[0,T]$ are unconstrained. Paths and OD pairs are finite types, with a map sending each path to its OD pair. The essential infimum is the literal formula (12), a real supremum; it is not the pointwise infimum, which changes when $C$ is altered on a null set and makes sufficiency false. $\mu_{kl}$ is a real infimum over $P_{kl}$ ; for a pair with no paths it is an unused default value.

The cost operator C is abstract, with the paper's measurability assumption strengthened to square-integrability so that every integral in (39) is a genuine Lebesgue integral. The network dynamics (3)–(11) that produce C in the paper are not formalized. Nonnegativity (the codomain $\mathbb R_+$ of (13)) and square-integrability are assumed only at $h^*$ , which makes the formal statements stronger than the paper's. Without integrability, Lean's integral of a non-integrable function is $0$ , so (39) could hold vacuously; the added hypothesis excludes that trivialization. The goal quantifies over every cost operator satisfying these hypotheses and never fixes one. In the milestones, the reduction from $p=q$ to $p\ne q$ (p. 188) is taken as the hypothesis $p\ne q$ .

A complete development needs: properties of the real essential infimum (12) on a finite measure space; Lemma 2 (continuity of measure from below); the existence of measurable subsets of prescribed measure in Lebesgue measure (nonatomicity, available in Mathlib in some form); and integral bookkeeping for products of $L^2$ functions on a finite measure. The essential-infimum and mass-shift lemmas are reusable for other continuous-time equilibrium models. Proofs of any milestone, and cleaner restatements of the essential-infimum API, are welcome.

Selected references

T. L. Friesz, D. Bernstein, T. E. Smith, R. L. Tobin and B. W. Wie, A variational inequality formulation of the dynamic network user equilibrium problem, Operations Research 41(1):179–191, 1993. https://doi.org/10.1287/opre.41.1.179
J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers 1(3):325–362, 1952. https://doi.org/10.1680/ipeds.1952.11259
M. J. Smith, The existence, uniqueness and stability of traffic equilibria, Transportation Research B 13(4):295–304, 1979. https://doi.org/10.1016/0191-2615(79)90022-5
S. Dafermos, Traffic equilibrium and variational inequalities, Transportation Science 14(1):42–54, 1980. https://doi.org/10.1287/trsc.14.1.42
T. L. Friesz, J. Luque, R. L. Tobin and B. W. Wie, Dynamic network traffic assignment considered as a continuous time optimal control problem, Operations Research 37(6):893–901, 1989. https://doi.org/10.1287/opre.37.6.893
P. R. Halmos, Measure Theory, Van Nostrand, 1950 (Proposition 41.2, nonatomicity of Lebesgue measure).

11 thms2 active usersReviewed

Completed

Captain: moona3k

Sharp diagonal Hlawka constants: lower the cutoff to 87Open Problem

This completed entry lowers the sufficient exponent cutoff for the sharp diagonal Hlawka formula from 90 to 87. The goal is already proved in Lean on Prove2Me: for every real p ≥ 87, the foundation's cyclic constant K_p is the least constant that works for every triple of complex coordinate vectors in every finite dimension.

The statement includes arbitrary unequal-norm and zero triples, as well as dimension zero. It uses the foundation's unchanged definitions and combines admissibility with uniform optimality. This concerns complex diagonal matrices; it does not claim the corresponding result for general matrices or settle the conjecture for all p ≥ 2.

Proved goal and supporting result

Sharp complex coordinate Hlawka constant for p ≥ 87: the goal, already Proved.
The real coordinate Hlawka bound for p ≥ 87: the supporting milestone, already Proved.

The campaign template is instantiated with value 87. Both items reference the existing accepted theorems.

Proof route and attribution

The proof extends the accepted cutoff-90 Lean development by BrunoDCDO, adapting Ezzeri Esa's construction and analytic argument. The contributions at cutoffs 89, 88 and 87 were submitted by moona3k.

For p ≥ 88, the proof uses the accepted cutoff-88 result. On 87 ≤ p ≤ 88, it retains the localization, box-convexity and cyclic-averaging argument, with confinement parameter q₀ = 5351/15000, an improved cyclic witness (3/(4p))^(1/p), sharper Taylor estimates and exact rational polynomial certificates.

Campaign context

The foundation established cutoff 256; the supplied argument was formalized at cutoff 90. The subsequent accepted results extend the same formula to cutoffs 89, 88 and 87. This entry records the proved cutoff 87 on the campaign timeline; the campaign's cutoff-85 mission remains open.

5 thms2 active usersReviewed

Completed

Captain: savarin

Sharp diagonal Hlawka constants: lower the cutoff to 85Open Problem

The Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. The question is how large a comparison constant is needed to make this inequality hold.

This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real $p\ge87$ , also holds for every real $p\ge85$ . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three $3\times3$ diagonal matrices. Because the accepted cutoff-87 theorem already covers every $p\ge87$ , the new work is the range from 85 to 87.

The cutoff came down from 90 to 87 in a day, through moona3k's proofs at 89, 88 and 87. The 89 proof reran the cutoff-90 argument with sharper, second-order estimates. A numerical model of that argument with retuned constants puts its limit between about 86.6 and 87.5: two of its steps pull the same parameter in opposite directions, and below that point no setting satisfies both. So reaching 85 is expected to need a new idea, not just tighter numbers. The goal theorem below gives the exact statement.

This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 85 or lower also settles this mission.

The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.

References

K. M. R. Audenaert and F. Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, arXiv preprint, 2012, §8.2, Problem 7. arXiv:1201.5232
Ezzeri Esa, Hlawka–Schatten inequalities: sharp diagonal construction, Lean source repository, 2026, revision 79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source library
Ezzeri Esa and project contributors, The cyclic bound for every real p ≥ 90, research note with appendices and exact certificates, 2026. Research note

Established results on Prove2Me

63 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

A Primal–Dual Splitting Method for Convex Optimization Involving Lipschitzian, Proximable and Linear Composite Terms II: With F = 0, Iterates Converge Weakly to a Primal–Dual Solution When στ‖L‖² < 1Research Paper

Motivation

Many problems in imaging, signal processing and statistics are convex minimizations of the form

\min_{x\in\mathcal X}\ F(x)+G(x)+H(Lx),

where $F$ is smooth, $G$ and $H$ are nonsmooth but have computable proximity operators, and $L$ is a bounded linear operator, for example a discrete gradient in total-variation denoising. Primal–dual splitting methods solve such problems using only $\nabla F$ , the proximity operators of $G$ and $H^*$ , and applications of $L$ and $L^*$ , without ever inverting $L$ or computing the proximity operator of $H\circ L$ .

Condat's 2013 paper (JOTA 158(2):460–479; final author's version HAL hal-00609728v5) introduced Algorithms 3.1 and 3.2, which handle all three kinds of terms at once, allow relaxation and summable errors, and contain earlier methods as special cases. Together with the closely related work of Vũ (Adv. Comput. Math. 2013), it is the standard reference for the "Condat–Vũ" algorithm.

Timeline. Chambolle and Pock (2011) proved convergence of their primal–dual algorithm, without a smooth term and without relaxation, under $\sigma\tau\|L\|^2<1$ (J. Math. Imaging Vis. 40). He and Yuan (2012) interpreted it as a proximal point algorithm in a modified metric (SIAM J. Imaging Sci. 5). Condat (2013) added the smooth term $F$ , relaxation and errors (Theorem 3.1), and, for $F=0$ , proved weak convergence for relaxation parameters up to $2$ (Theorem 3.2), the result of this mission.

Setting

Let $\mathcal X$ and $\mathcal Y$ be real Hilbert spaces and $L:\mathcal X\to\mathcal Y$ a bounded linear operator with adjoint $L^*$ and operator norm $\|L\|$ . Write $\Gamma_0(\mathcal H)$ for the proper, lower semicontinuous, convex functions $\mathcal H\to\mathbb R\cup\{+\infty\}$ . For $J\in\Gamma_0(\mathcal H)$ , the conjugate is $J^*(s)=\sup_{s'}[\langle s,s'\rangle-J(s')]$ , the proximity operator is $\mathrm{prox}_J(s)=\arg\min_{s'}[J(s')+\tfrac12\|s-s'\|^2]$ , and the subdifferential is $\partial J(u)=\{v:\ J(u)+\langle v,u'-u\rangle\le J(u')\ \forall u'\}$ .

Fix $G\in\Gamma_0(\mathcal X)$ , $H\in\Gamma_0(\mathcal Y)$ and $F:\mathcal X\to\mathbb R$ . The primal–dual inclusion (6) asks for $(\hat x,\hat y)$ with

0\in\partial G(\hat x)+L^*\hat y+\nabla F(\hat x),\qquad 0\in-L\hat x+\partial H^*(\hat y);

then $\hat x$ minimizes $F+G+H\circ L$ and $\hat y$ solves the dual problem. The paper assumes this inclusion has a solution.

Given $\tau,\sigma>0$ , relaxation parameters $(\rho_n)$ and error terms $e_{F,n},e_{G,n}\in\mathcal X$ , $e_{H,n}\in\mathcal Y$ , Algorithm 3.1 iterates, from any $(x_0,y_0)$ ,

\tilde x_{n+1}=\mathrm{prox}_{\tau G}\big(x_n-\tau(\nabla F(x_n)+e_{F,n})-\tau L^*y_n\big)+e_{G,n},

\tilde y_{n+1}=\mathrm{prox}_{\sigma H^*}\big(y_n+\sigma L(2\tilde x_{n+1}-x_n)\big)+e_{H,n},

(x_{n+1},y_{n+1})=\rho_n(\tilde x_{n+1},\tilde y_{n+1})+(1-\rho_n)(x_n,y_n).

Algorithm 3.2 exchanges the roles: it computes $\tilde y_{n+1}$ from $y_n+\sigma Lx_n$ first, then $\tilde x_{n+1}$ using $L^*(2\tilde y_{n+1}-y_n)$ .

Formalization targets

Goal: Theorem 3.2

Suppose $F=0$ and $e_{F,n}=0$ , $\tau,\sigma>0$ , and

\sigma\tau\|L\|^2<1,\qquad \rho_n\in\,]0,2[,\qquad \sum_n\rho_n(2-\rho_n)=+\infty,\qquad \sum_n\rho_n\|e_{G,n}\|<+\infty,\ \ \sum_n\rho_n\|e_{H,n}\|<+\infty.

Then for every run of Algorithm 3.1, and for every run of Algorithm 3.2, there is a solution $(\hat x,\hat y)$ of (6) with $x_n\rightharpoonup\hat x$ and $y_n\rightharpoonup\hat y$ weakly.

Milestones

Lemma 4.1 (Krasnosel'skii–Mann): relaxed inexact iterates of a nonexpansive map converge weakly to a fixed point.
Lemma 4.2 (proximal point algorithm): for maximally monotone $M$ , $s_{n+1}=s_n+\rho_n((I+M)^{-1}s_n+e_n-s_n)$ converges weakly to a zero of $M$ under the same conditions on $\rho_n$ , $e_n$ as the goal.
$P$ bounded from below: if $\sigma\tau\|L\|^2<1$ , the operators $P=\begin{pmatrix}\tau^{-1}I&-L^*\\-L&\sigma^{-1}I\end{pmatrix}$ and $P'$ (with $+L^*$ , $+L$ ) satisfy $\langle z,Pz\rangle\ge c\|z\|^2$ .
Inclusions (22) and (44): each error-free step satisfies $-(\nabla F(x_n),0)\in A(\tilde z_{n+1})+P(\tilde z_{n+1}-z_n)$ (resp. $P'$ ), where $A(x,y)=(\partial G(x)+L^*y)\times(-Lx+\partial H^*(y))$ ; with $F=0$ the left side is $0$ .
$A$ is maximally monotone on $\mathcal X\times\mathcal Y$ .

Further items

Remark 3.2 (the goal with $F$ affine, $\beta=0$ , instead of $F=0$ ) and Theorem 5.2 (the version with $m\ge2$ composite terms $\sum_iH_i(L_ix)$ and condition $\sigma\tau\|\sum_iL_i^*L_i\|<1$ ).

Significance

The result. Theorem 3.2 covers the Chambolle–Pock algorithm with relaxation $\rho_n\in\,]0,2[$ and summable errors, in arbitrary real Hilbert spaces. Over-relaxation $\rho_n>1$ often speeds the method up in practice, and the error terms justify inexact proximity operators. Theorem 5.2 extends it to any finite number of composite terms by full splitting. The convergence statement makes no reference to a Lipschitz constant, so it applies whenever the problem has no smooth part.

Formalizing it. The result is proved on paper; no machine-checked version of Theorem 3.2, of the Krasnosel'skii–Mann lemma with errors, or of the proximal point algorithm under the condition $\sum\rho_n(2-\rho_n)=+\infty$ is known to exist. A formal proof would supply reusable pieces of monotone-operator theory in Hilbert spaces: weak convergence of Fejér-type iterations, the change of metric induced by a positive operator, and maximal monotonicity of sums with a skew operator.

Difficulty

The algorithm is not a fixed-point iteration of a nonexpansive map in the original inner product: the coupling between the primal and dual steps breaks nonexpansiveness. The difficulty is to find a metric in which it becomes one, to show this metric is equivalent to the original one (which is where $\sigma\tau\|L\|^2<1$ , strictly, is needed), and to transfer maximal monotonicity, zeros and summability of the errors to the new metric. Weak convergence in infinite dimension also requires an Opial-type argument rather than compactness. Mathlib provides inner product spaces, the operator norm and adjoints, but neither maximal monotone operators nor resolvents nor Krasnosel'skii–Mann iteration theory.

Formalization scope

The spaces are real Hilbert spaces (InnerProductSpace ℝ and CompleteSpace). Functions valued in $\mathbb R\cup\{+\infty\}$ are EReal-valued, with $\Gamma_0$ the published IsProperClosedConvex. The conjugate is an EReal supremum, so $H^*$ can take the value $+\infty$ . Proximity operators enter as maps with the published IsProx property; the subdifferential is the published IsSubgradient. The product $\mathcal X\times\mathcal Y$ with the inner product $\langle x,x'\rangle+\langle y,y'\rangle$ is WithLp 2 (X × Y). Weak convergence is $\langle x_n,v\rangle\to\langle\hat x,v\rangle$ for all $v$ . " $\sum a_n=+\infty$ " means partial sums tend to $+\infty$ , and " $\sum\rho_n\|e_n\|<+\infty$ " means summability of a nonnegative series.

Standing assumptions are hypotheses: $G,H\in\Gamma_0$ , and (6) has a solution. With $F=0$ the smoothness assumption on $F$ is automatic. The paper's assumption that (1) has a minimizer follows from the solvability of (6) and is not stated. The goal is a conjunction over the two algorithms, and the limit $(\hat x,\hat y)$ is chosen after the run.

The condition is strict, $\sigma\tau\|L\|^2<1$ , and relaxation is open, $\rho_n\in\,]0,2[$ . A goal quantifying over no run, assuming the limit exists, or fixing $(\hat x,\hat y)$ before the initial point would be a different and weaker statement. Proofs of the milestones, of Theorem 5.2 via the product-space identities (49)–(52), and general results on monotone operators are welcome.

Selected references

L. Condat, A primal–dual splitting method for convex optimization involving Lipschitzian, proximable and linear composite terms, J. Optim. Theory Appl. 158(2):460–479, 2013. https://doi.org/10.1007/s10957-012-0245-9 (author's version: https://hal.science/hal-00609728)
A. Chambolle, T. Pock, A first-order primal-dual algorithm for convex problems with applications to imaging, J. Math. Imaging Vis. 40:120–145, 2011. https://doi.org/10.1007/s10851-010-0251-1
B. He, X. Yuan, Convergence analysis of primal-dual algorithms for a saddle-point problem: from contraction perspective, SIAM J. Imaging Sci. 5(1):119–149, 2012. https://doi.org/10.1137/100814494
B. C. Vũ, A splitting algorithm for dual monotone inclusions involving cocoercive operators, Adv. Comput. Math. 38:667–681, 2013. https://doi.org/10.1007/s10444-011-9254-8
H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011. https://doi.org/10.1007/978-1-4419-9467-7
P. L. Combettes, Solving monotone inclusions via compositions of nonexpansive averaged operators, Optimization 53:475–504, 2004. https://doi.org/10.1080/02331930412331327157

15 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

A Primal–Dual Splitting Method for Convex Optimization Involving Lipschitzian, Proximable and Linear Composite Terms III: In Finite Dimension with F = 0, Iterates Converge When στ‖L‖² ≤ 1Research Paper

Motivation

Many problems in imaging, signal processing and statistics take the form

\min_{x\in\mathcal X}\ F(x)+G(x)+H(Lx),

where $G$ and $H$ are convex functions whose proximity operators can be computed cheaply, $L$ is a linear operator such as a finite-difference gradient, and $F$ is smooth. Total-variation denoising, the lasso with a structured penalty, and constrained least squares are of this type. Because $H\circ L$ is generally not proximable even when $H$ is, practical methods split the problem so that each step uses only $\mathrm{prox}_{\tau G}$ , $\mathrm{prox}_{\sigma H^*}$ , $L$ and $L^*$ , without inverting any operator.

L. Condat (J. Optim. Theory Appl. 158 (2013)) introduced a relaxed, inexact primal–dual iteration of this kind; B. C. Vũ (Adv. Comput. Math. 38 (2013)) studied the same structure for monotone inclusions. With $F=0$ the iteration is exactly the method of Chambolle and Pock (J. Math. Imaging Vis. 40 (2011)). They proved convergence in finite dimension assuming $\tau\sigma\|L\|^2<1$ , $\rho_n\equiv1$ and no errors. He and Yuan (SIAM J. Imaging Sci. 5 (2012)) extended this to a constant relaxation $\rho_n\equiv\rho\in\,]0,2[$ under the same other hypotheses (Condat, §3.1.1). Condat's paper proves three convergence theorems. This mission is the third: in finite dimension and with $F=0$ , the iterates converge under the step-size condition $\sigma\tau\|L\|^2\le1$ , equality included. Equality matters in practice: one can set $\sigma=1/(\tau\|L\|^2)$ and tune a single parameter, as in the Douglas–Rachford method.

Setting

Let $\mathcal X$ and $\mathcal Y$ be real Hilbert spaces and $L:\mathcal X\to\mathcal Y$ a bounded linear operator with adjoint $L^*$ and operator norm $\|L\|$ . Write $\Gamma_0(\mathcal H)$ for the proper, lower semicontinuous, convex functions $\mathcal H\to\mathbb R\cup\{+\infty\}$ , and let $G\in\Gamma_0(\mathcal X)$ , $H\in\Gamma_0(\mathcal Y)$ . The Fenchel conjugate is $H^*(s)=\sup_{s'}[\langle s,s'\rangle-H(s')]$ , the proximity operator is $\mathrm{prox}_J(s)=\operatorname{argmin}_{s'}[J(s')+\tfrac12\|s-s'\|^2]$ , and the subdifferential is $\partial J(u)=\{v:\ \langle u'-u,v\rangle+J(u)\le J(u')\ \forall u'\}$ .

The primal–dual inclusion (6) asks for $(\hat x,\hat y)\in\mathcal X\times\mathcal Y$ with

0\in\partial G(\hat x)+L^*\hat y+\nabla F(\hat x),\qquad 0\in-L\hat x+\partial H^*(\hat y).

A solution gives a minimiser $\hat x$ of the primal problem and a solution $\hat y$ of its dual.

Algorithm 3.1 chooses $\tau>0$ , $\sigma>0$ , relaxation parameters $(\rho_n)$ , error terms $(e_{F,n}),(e_{G,n}),(e_{H,n})$ and an initial estimate $(x_0,y_0)$ , then iterates

\tilde x_{n+1}=\mathrm{prox}_{\tau G}\big(x_n-\tau(\nabla F(x_n)+e_{F,n})-\tau L^*y_n\big)+e_{G,n},\qquad \tilde y_{n+1}=\mathrm{prox}_{\sigma H^*}\big(y_n+\sigma L(2\tilde x_{n+1}-x_n)\big)+e_{H,n},

(x_{n+1},y_{n+1})=\rho_n(\tilde x_{n+1},\tilde y_{n+1})+(1-\rho_n)(x_n,y_n).

Algorithm 3.2 swaps the roles of the primal and dual variables: the dual step comes first, and the primal step uses $2\tilde y_{n+1}-y_n$ . Section 5 extends both to $\sum_{i=1}^mH_i(L_ix)$ (Algorithms 5.1 and 5.2), with the inclusion (48) in place of (6).

Formalization targets

Goal: Theorem 3.3 (p. 6)

Let $\mathcal X$ , $\mathcal Y$ be finite-dimensional, $F=0$ , $e_{F,n}=0$ , and assume (6) has a solution. If

\text{(i)}\ \sigma\tau\|L\|^2\le1,\qquad \text{(ii)}\ \rho_n\in[\varepsilon,2-\varepsilon]\ \ \forall n,\ \text{for some }\varepsilon>0,\qquad \text{(iii)}\ \textstyle\sum_n\|e_{G,n}\|<\infty,\ \sum_n\|e_{H,n}\|<\infty,

then for every run of Algorithm 3.1, and for every run of Algorithm 3.2, $(x_n,y_n)$ converges to a solution $(\hat x,\hat y)$ of (6).

Milestones (from the proof, pp. 8–13)

With $P(x,y)=(\tfrac1\tau x-L^*y,\,-Lx+\tfrac1\sigma y)$ the operator (20) and $T(x,y)=(\tilde x,\tilde y)$ the error-free step of Algorithm 3.1:

$P$ (and $P'$ of (44)) is positive under (i): $\langle z,Pz\rangle\ge0$ ;
$T$ depends on $z$ only through $Pz$ (the paper's $T\circ S=T$ , (32)–(33));
on solutions of (6), $PT(z)=Pz$ ((41)–(42));
$PT(z)=Pz$ implies that $T(z)$ solves (6) (via (35));
$T$ is continuous;
Lemma 4.1 (Krasnosel'skii–Mann iteration) and Lemma 4.6 (Polyak's lemma).

Further statements

Remark 3.2 (Theorem 3.3 with $F$ affine, i.e. $\beta=0$ in (2)) and Theorem 5.3 (the analogue for $m\ge2$ composite terms, with (i) replaced by $\sigma\tau\|\sum_iL_i^*L_i\|\le1$ ) are included as draft theorems.

Significance

Theorem 3.3 is the convergence guarantee behind the common practice of running the Chambolle–Pock iteration and its relaxed variants at the critical step size $\sigma\tau\|L\|^2=1$ . It covers relaxation parameters up to $2-\varepsilon$ and summable errors in both proximity operators. It applies directly to the discrete models of imaging and statistics, which are finite-dimensional. Theorem 5.3 extends it to any finite number of composite terms in parallel.

None of the statements of this paper is formalized on the platform. Machine-checked convergence proofs for primal–dual splitting are not available in Mathlib. The mission would produce the first ones, together with two standalone tools of general use: the inexact Krasnosel'skii–Mann theorem (Lemma 4.1), and Polyak's recursive-inequality lemma (Lemma 4.6), which is a standard tool for stochastic and inexact iterations.

Difficulty

The usual proof treats the iteration as a proximal-point or forward–backward step in the space $\mathcal X\times\mathcal Y$ with the inner product $\langle z,Pz'\rangle$ . That argument needs $P$ strictly positive, which is exactly what fails when $\sigma\tau\|L\|^2=1$ : then $P$ has a nontrivial kernel, $\langle z,Pz\rangle$ is only a seminorm, and weak convergence in the $P$ -geometry says nothing about the components of $z$ in $\ker P$ . The proof replaces the iteration by its "shadow" $Sz_n$ on $\operatorname{ran}P$ , uses that $T$ factors through $S$ , and recovers the full iterates through continuity of $T$ and a recursive inequality. The last step requires strong convergence of the shadow sequence, which is where finite dimension enters. Infinite-dimensional versions require different arguments and are not claimed here.

Formalization scope

Spaces are real inner product spaces with CompleteSpace; the goal and Theorem 5.3 add FiniteDimensional. Functions in $\Gamma_0$ take values in EReal and satisfy the published predicate IsProperClosedConvex (never $-\infty$ , finite somewhere, lower semicontinuous, convex epigraph). The conjugate is an EReal supremum. Proximity operators are maps $P_G$ , $P_H$ satisfying the published minimisation predicate IsProx for $\tau G$ and $\sigma H^*$ ; such maps exist and are unique for $\Gamma_0$ functions. The subdifferential is the published IsSubgradient. Runs of the algorithms are predicates on pairs of sequences with arbitrary initial point, and the limit is chosen after the run. " $=+\infty$ " for a series is divergence of its partial sums, " $<+\infty$ " is summability of a nonnegative series, and convergence in the goal is norm convergence.

The standing assumptions of pp. 3–4 are hypotheses: $G,H\in\Gamma_0$ , and (6) has a solution. The paper's other standing assumption, that problem (1) has a minimiser, follows from the second and is omitted. In the milestones, the operators $P$ and $T$ are plain maps on $\mathcal X\times\mathcal Y$ . The projector $S$ is not built: " $T\circ S=T$ " is stated as " $Pz=Pz'\Rightarrow T(z)=T(z')$ ", which is equivalent because $P$ is self-adjoint. Each milestone drops finite dimension, so it is stated at least as strongly as on the page.

The strict inequality $\sigma\tau\|L\|^2<1$ would make the goal a corollary of the weaker Theorem 3.2 with an extra finite-dimensional upgrade. The goal keeps $\le$ . Weak convergence in place of norm convergence, an $\varepsilon$ chosen after $n$ , or a solution of (6) fixed before the run would each weaken the theorem, and all are excluded.

Useful infrastructure includes: firm nonexpansiveness of $\mathrm{prox}$ for EReal-valued $\Gamma_0$ functions; $\Gamma_0$ -ness of the conjugate and Moreau's identity; maximal monotonicity of $\partial G\times\partial H^*$ plus a skew operator; and the inexact Krasnosel'skii–Mann theorem. All of it can be reused for Theorems 3.1 and 3.2 of the same paper, and for Douglas–Rachford and three-operator splitting. Proofs of individual milestones are welcome independently of the goal.

Selected references

L. Condat, A primal–dual splitting method for convex optimization involving Lipschitzian, proximable and linear composite terms, J. Optim. Theory Appl. 158(2):460–479, 2013. https://doi.org/10.1007/s10957-012-0245-9 (author's version: https://hal.science/hal-00609728v5)
B. C. Vũ, A splitting algorithm for dual monotone inclusions involving cocoercive operators, Adv. Comput. Math. 38:667–681, 2013. https://doi.org/10.1007/s10444-011-9254-8
A. Chambolle, T. Pock, A first-order primal–dual algorithm for convex problems with applications to imaging, J. Math. Imaging Vis. 40:120–145, 2011. https://doi.org/10.1007/s10851-010-0251-1
P. L. Combettes, Solving monotone inclusions via compositions of nonexpansive averaged operators, Optimization 53:475–504, 2004. https://doi.org/10.1080/02331930412331327157
H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011. https://doi.org/10.1007/978-1-4419-9467-7
B. T. Polyak, Introduction to Optimization, Optimization Software, New York, 1987.

13 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

A Primal–Dual Splitting Method for Convex Optimization Involving Lipschitzian, Proximable and Linear Composite Terms I: Iterates Converge Weakly to a Primal–Dual Solution When 1/τ − σ‖L‖² ≥ β/2Research Paper

Motivation

Many convex optimization models combine a smooth loss, a nonsmooth penalty whose proximity operator is easy to compute, and a second penalty applied after a linear map. Imaging models, for example, often place a data-fitting term on the image and a regularizer on its transformed coefficients. The resulting objective has the form $F(x)+G(x)+H(Lx)$ . Condat's primal–dual method evaluates the smooth gradient and two proximity operators separately, without requiring a proximity operator for the composite $H\circ L$ . Condat, 2013 establishes weak convergence with relaxation and summably weighted computational errors. This mission targets its main positive-smoothness theorem, Theorem 3.1, in the final author's version.

The theorem matters when a computed gradient or proximal point is inexact, as is common when a proximal subproblem is itself solved numerically. Its conditions account for these errors directly rather than treating the displayed algorithm as exact. It also gives one parameter regime for two orders of updating the primal and dual variables. These two algorithms share an objective and a solution inclusion, but have distinct recursions.

Setting

Let $\mathcal X$ and $\mathcal Y$ be real Hilbert spaces and let $L:\mathcal X\to\mathcal Y$ be bounded linear, with adjoint $L^*$ . The smooth term $F:\mathcal X\to\mathbb R$ is convex and differentiable. Its gradient is $\beta$ -Lipschitz when $\|\nabla F(x)-\nabla F(x')\|\le\beta\|x-x'\|$ for all $x,x'$ . The nonsmooth terms $G$ and $H$ are proper, lower semicontinuous, convex functions with values in $\mathbb R\cup\{+\infty\}$ . Such functions form the class $\Gamma_0$ . An infinite value may encode a constraint.

For a convex function $J$ , its proximity operator $\operatorname{prox}_{\gamma J}(s)$ minimizes $J(u)+\|u-s\|^2/(2\gamma)$ over $u$ , where $\gamma>0$ . The Fenchel conjugate is $J^*(v)=\sup_u\{\langle v,u\rangle-J(u)\}$ . A subgradient $v\in\partial J(u)$ obeys $J(u)+\langle v,u'-u\rangle\le J(u')$ for every $u'$ . The sought primal–dual solution $(\hat x,\hat y)$ satisfies

-L^*\hat y-\nabla F(\hat x)\in\partial G(\hat x),\qquad L\hat x\in\partial H^*(\hat y).

Algorithms 3.1 and 3.2 maintain sequences $x_n\in\mathcal X$ and $y_n\in\mathcal Y$ . Algorithm 3.1 updates the primal proximity step before the dual one; Algorithm 3.2 reverses that order. Each uses positive step sizes $\tau,\sigma$ , positive relaxation weights $\rho_n$ , and errors $e_{F,n}$ , $e_{G,n}$ and $e_{H,n}$ in the gradient and the two proximal evaluations. Their full recursions are part of the Lean setting, so a run is determined by its initial pair. The paper specifies the problem in §2 and both algorithms in §3.

Formalization targets

The goal is Theorem 3.1 on p. 5. Suppose $\beta>0$ , the primal–dual solution set is nonempty, and $G,H\in\Gamma_0$ . Set

\delta=2-\frac{\beta}{2}\left(\frac1\tau-\sigma\|L\|^2\right)^{-1}.

For $\tau,\sigma>0$ , the theorem assumes

\frac1\tau-\sigma\|L\|^2\ge\frac\beta2,\qquad 0<\rho_n<\delta\quad\text{for every }n,

\sum_{n\ge0}\rho_n(\delta-\rho_n)=+\infty,\qquad\sum_{n\ge0}\rho_n\|e_{F,n}\|<\infty,\quad\sum_{n\ge0}\rho_n\|e_{G,n}\|<\infty,\quad\sum_{n\ge0}\rho_n\|e_{H,n}\|<\infty.

Under these conditions, both sequences of each algorithm converge weakly to the components of a primal–dual solution. The solution may depend on the initial pair and on the run. The milestone list includes Lemmas 4.1 and 4.3–4.5, the strict positivity claim for the block operator $P$ , estimate (29), and the error-free optimality inclusions (22) and (44), ordered as preliminary results followed by the two algorithm-specific claims. These targets match the results stated in §4 of the source version.

Significance

The result supplies a convergence guarantee for a composite objective under an explicit coupling condition on $\tau$ , $\sigma$ , and $\|L\|$ . It permits relaxation weights that vary with $n$ and errors that are summable only after weighting by those same relaxation values. The dual conclusion is substantive: convergence of the primal sequence alone would not give convergence of the dual certificate produced by the algorithm. The weak topology is appropriate in general Hilbert spaces; norm convergence would assert more than the paper proves.

The theorem is proved in the 2013 paper. The present formalization task is to give its statement and the selected operator lemmas machine-checked proofs in Lean. Related platform definitions for proximal maps, monotone operators, nonexpansive maps, subgradients and weak convergence already exist; the paper-specific convergence theorem and its selected milestones are new targets in this proposal. The resulting definitions and abstract Lemmas 4.1, 4.3–4.5 can be reused in later operator-splitting developments.

Difficulty

The displayed recursions involve three errors, two proximal evaluations, a linear map and its adjoint, and two different update orders. A direct estimate on $\|x_{n+1}-\hat x\|$ does not by itself control the coupled dual variable, while a bound on only the combined objective value would not establish weak convergence of either iterate. The relaxation condition permits weights without a fixed positive lower bound, so a convergence argument cannot replace the stated divergent series by a simpler constant-step assumption. The abstract lemmas must also retain the endpoints $\alpha_2=1$ and $\gamma=2\kappa$ present in the source.

Formalization scope

Lean uses complete real inner-product spaces for $\mathcal X$ and $\mathcal Y$ , a continuous linear map for $L$ , and EReal for $G$ , $H$ and their conjugates. The conjugate supremum is taken in EReal. The paper's $\Gamma_0$ class and proximity maps use published definitions; the latter are parameters constrained to be the actual proximal minimizers. Positive step sizes and proper closed convex data ensure such maps exist and are unique. The subgradient predicate explicitly requires a finite value at the base point; this follows from the source's properness assumptions when a subgradient exists.

Both algorithms are represented by recursion predicates on every natural-number index, with all error terms present. The goal quantifies over every run and chooses its weak limit afterwards. Divergence to $+\infty$ means finite partial sums tend to atTop; a finite weighted error sum means the corresponding nonnegative real sequence is summable. These choices prevent a default value of an infinite sum from satisfying the hypotheses. The nonempty solution set is an explicit standing assumption from p. 4 and implies the earlier nonempty-primal-minimizer assumption. A condition that made all runs impossible, or one that discarded either the primal or dual conclusion, would not represent Theorem 3.1.

The block operator $P$ is represented through its quadratic form $q_P$ ; $P'$ is recorded for Algorithm 3.2. The complete development will need the abstract iteration lemmas, proximal optimality conditions, block-metric estimates, and the links from each algorithm's inclusion to the solution set. Contributions proving those results, or building reusable Hilbert-space operator infrastructure needed by them, are in scope. The several-composite-functions extension in Theorem 5.1 is reserved for separate work.

Selected references

Laurent Condat, A primal–dual splitting method for convex optimization involving Lipschitzian, proximable and linear composite terms, Journal of Optimization Theory and Applications 158(2):460–479, 2013. DOI; final author's version, hal-00609728v5.

15 thms2 active usersReviewed

Completed

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

Functional Analysis

Missions

Backward intertwiners and a transitive commutantResearch Paper

Motivation

Timeline

Setting

Formalization targets

Goal: Corollary 1.2

Significance

Difficulty

Formalization scope

Selected references

Unitarizability implies amenability for discrete groupsResearch Paper

Motivation

Timeline

Setting

Formalization targets

Milestone: countable case

Goal: Theorem 1.1

Significance

Difficulty

Formalization scope

Selected references

Thompson's group F is nonamenableResearch Paper

Motivation

Background

Setting

Formalization targets

Goal: Theorem 1.1 (p. 1)

Significance

Difficulty

Formalization scope

Selected references

Finite-Circle Obstructions, Binary Codes, and Histogram Embeddings for Edit DistanceResearch Paper

Motivation

Background

Setting

Formalization targets

Goal: finiteCircle_fullMain

Significance

Difficulty

Formalization scope

Selected references

A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embeddingResearch Paper

Motivation

Timeline

Setting

Formalization targets

Corollary 6 (milestone)

Goal: Theorem 1

Significance

Difficulty

Formalization scope

Selected references

Subpolynomial dimension reduction in LpResearch Paper

Motivation

Timeline

Setting

Formalization targets

Goal: Theorem 1.1

Significance

Difficulty

Formalization scope

Selected references

A Monotone+Skew Splitting Model for Composite Monotone Inclusions in Duality: The Inexact Primal–Dual Forward–Backward–Forward Iterates Converge Weakly to a Primal and a Dual SolutionResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Logarithmic Sobolev Inequalities for Finite Markov Chains 3: Lower Bound α ≥ (1 − 2/q)λ / 2(λt_q + log M_q + (q − 2)/q) from a Bound on ‖H_{t_q}‖_{2→q}Research Paper

Motivation

Setting

Formalization targets

Theorem 3.9: a single heat-operator estimate bounds α\alphaα

Companion results

Goal: `finiteCircle_fullMain`

Theorem 3.9: a single heat-operator estimate bounds $\alpha$