The following describes the scope of the Lean formalization related to the following accompanying paper(s):
Scope
The paper constructs a Banach space whose midpoint geometry is asymptotically uniformly convex even though no equivalent norm is asymptotically uniformly convex in the usual one-sided sense. The formalization proves that the full dual of the specified segment-norm completion is infinite-dimensional, separable, and reflexive; its averaged midpoint modulus is at least \(\sqrt{1+t^2/12}-1\) for every \(t>0\), while every equivalent norm fails asymptotic uniform convexity. It also proves that an embedding of a depth-\(k\) countably branching diamond has distortion at least \(\sqrt{1+k/12}\).
The general-forest and word-forest results use the closed span of the coordinate functionals. Their conclusions retain the finite-ancestor and equivalent-norm hypotheses, including the scale \(\alpha/(2\beta)\) when \(0<\alpha\le\beta\) and the new norm lies between \(\alpha\) and \(\beta\) times the original norm; they do not identify that span with the full dual or assert reflexivity for every forest.
The paper controls midpoint lenses in Banach spaces defined by tree-segment norms. The formalization proves the following estimate in both the full dual of the finite-height forest space and the coordinate predual of the infinite-tree space. If \(x\) is supported on a finite ancestral set \(H\), \(R\ge0\), and \(\|x+y\|,\|x-y\|\le R\), then the part of \(y\) outside \(H\) has norm at most \(2\sqrt{R^2-\|x\|^2}\).
The formalization also covers selected consequences for averaged midpoint moduli and separated families of vectors, together with reflexivity and renorming obstructions. This scope concerns the segment-space results; the companion results on diamond energies remain separate.
The paper studies embeddings of countably branching diamond graphs into Banach spaces built from tree segments. The formalization proves that every embedding of the depth-\(k\) diamond with distortion \(D\), at any positive scale, satisfies \(1+k/4\le D^2\) in either of two spaces: the full dual of the completed finite-height forest space and the closed coordinate span in the dual of the infinite-tree space. The bound applies to all pairs of vertices and is unconditional.
The formalization also contains selected graph deductions under explicit companion assumptions. Twenty-two of those companion inputs are assumed in these deductions; the diamond distortion bound above does not require them.
The paper exhibits a real \(L_1\) subspace with positive averaged midpoint convexity but no equivalent asymptotically uniformly convex norm. For every closed infinite-dimensional subspace whose unit ball is precompact in measure and which has the Daugavet property, the formalization computes the moduli at every unit vector: the averaged midpoint modulus is \(\max(t/2,t-1)\) and the usual one-sided asymptotic modulus is \(\max(0,t-2)\) for every \(t>0\). The same formulas hold after taking the infimum over unit vectors, and every equivalent norm fails asymptotic uniform convexity.
The formalization also constructs such a subspace on a countable product of unit intervals and proves that it has the stated measure-precompactness and Daugavet properties, so the modulus formulas apply to an actual example.
The paper constructs Banach spaces from bounded tree potentials and path costs to separate averaged midpoint convexity from asymptotic uniform convexity. For the specified tree-potential completions, the formalization proves completeness, separability, infinite dimension, and an averaged midpoint modulus of at least \(\sqrt{1+t^2/4}-1\) for \(0<t<1\). No space linearly isomorphic to one of these completions is asymptotically uniformly convex.
The formalization also covers selected path-cost duality and comparison results, clipping and energy estimates, and further renorming obstructions. These retain their stated support, head, and tail hypotheses; the remaining auxiliary assertions of the paper are outside this scope.
The paper forms a real \(L_1\) space from the closed span of products of independent multipliers along tree paths. For a positive, nonconstant multiplier of mean one and finite second moment, the formalization proves that this space is infinite-dimensional and has no equivalent asymptotically uniformly convex norm.
For every \(t>0\), the averaged midpoint modulus nevertheless has explicit positive lower bounds. If \(G\) is a standard real Gaussian, the exponential-multiplier bound is \(\frac{7t}{480}\mathbb E[(|G|-20/t)_+]\), where \(u_+=\max(u,0)\). For squared-Gaussian multipliers, the bounds are \(\frac18\Pr(|G|\ge4\sqrt2(2+\sqrt2)/t)\) and \(\frac14\Pr(|G|\ge8\sqrt6/t)\).
The paper constructs three Banach spaces from recursive tree potentials: a root-sum space, a zero-root space, and a joined space. The formalization proves that all three are infinite-dimensional and have no equivalent asymptotically uniformly convex norm. The root-sum and joined spaces have averaged midpoint modulus at least \(t^3/128\) for \(0<t<1\), and the root-sum modulus is positive for every \(t>0\). The zero-root estimate retains its finite ancestral support and tail hypotheses, and the zero-root and joined spaces are reflexive.
The formalization also covers a separated-midpoint result for the joined space and a variable-exponent model with its recursive norm, duality, projections, renorming obstruction, and sixth- and third-order stability estimates. The separation, sequence, support, and head assumptions in these results are essential parts of their statements.
Comparator links
