Constructs a real reflexive Banach space with an asymptotically midpoint uniformly convex norm but no equivalent asymptotically uniformly convex norm, extending Baudier's separation to reflexive spaces. In the same space, depth-k countably branching diamonds require distortion at least \sqrt{1+k/12}, so midpoint uniform convexity does not force uniformly bounded diamond distortion even under reflexivity. (Lean)
Manuscripts (7)
Asymptotic midpoint uniform convexity and unbounded diamond distortion in a reflexive tree space
September 27, 2026 · source · Lean formalization available · cite as \cite{OAI:Asymptotic-midpoint-uniform-convexity-and-unbounded-diamond-distortion-in-a-reflexive-tree-space-September-27-2026}
We construct a separable reflexive real Banach space whose given norm is asymptotically midpoint uniformly convex but which admits no asymptotically uniformly convex equivalent norm. Its averaged midpoint modulus is at least \sqrt{1+t^2/12}-1, and the countably branching diamond of depth k has distortion at least \sqrt{1+k/12} in this space. This gives a negative answer to the reflexive diamond converse for asymptotic uniform convexifiability.
Midpoint lenses in segment spaces
September 27, 2026 · source · Lean formalization available · cite as \cite{OAI:Midpoint-lenses-in-segment-spaces-September-27-2026}
For a real segment-forest dual with unbounded finite component heights and the real infinite-height coordinate predual, we bound the tail of an arbitrary displacement in a symmetric lens by 2\sqrt{R^2-\|x\|^2}, where R is the lens radius and x is its finitely supported center. Both given norms are asymptotically midpoint uniformly convex, although neither space admits an equivalent asymptotically uniformly convex norm. The finite-height forest dual is reflexive.
Distortion of countably branching diamonds from midpoint and tree energies
September 27, 2026 · source · Lean formalization available · cite as \cite{OAI:Diamond-distortion-from-midpoint-and-tree-energies-September-27-2026}
We derive quantitative distortion bounds for countably branching diamond graphs from midpoint estimates and direct tree energies. In the dual of a finite-height segment forest, every distortion-D embedding of the depth-k diamond satisfies D^2\ge1+k/4. The same bound holds in the infinite-height coordinate predual. We also obtain power-type distortion bounds for path-cost and recursive tree norms.
Exact asymptotic moduli in a Daugavet subspace of L1
September 27, 2026 · source · Lean formalization available · cite as \cite{OAI:Exact-asymptotic-moduli-in-a-Daugavet-subspace-of-L1-September-27-2026}
For an infinite-dimensional real subspace of L1 whose unit ball is totally bounded in measure and whose norm has the Daugavet property, we compute the averaged midpoint and one-sided asymptotic moduli at every unit center. They are \max\{t/2,t-1\} and \max\{0,t-2\}, respectively. The same weak-neighborhood geometry excludes every equivalent asymptotically uniformly convex norm. A quantitative realization of the Kadets–Werner construction supplies a space with both hypotheses.
Midpoint convexity from bounded tree potentials and path costs
September 27, 2026 · source · Lean formalization available · cite as \cite{OAI:Midpoint-convexity-from-bounded-tree-potentials-and-path-costs-September-27-2026}
Four real Banach spaces defined by bounded tree potentials satisfy the averaged asymptotic midpoint bound \widehat\delta(t)\ge\sqrt{1+t^2/4}-1 for 0\lt t\lt 1, while none admits an asymptotically uniformly convex (AUC) renorming. On finite-height trees, the globally constrained norm equals the least additive cost of a Hilbert vector and root paths. The quadratic path and segment-start outer Hilbert sums are reflexive and asymptotically midpoint uniformly convex, and admit no equivalent AUC norm.
Independent products in real L1: asymptotic midpoint convexity without AUC renormings
September 27, 2026 · source · Lean formalization available · cite as \cite{OAI:Independent-products-in-real-L1-asymptotic-midpoint-convexity-without-AUC-renormings-September-27-2026}
For a countably branching tree, the closed real L1 spans of products of independent exponential or Gaussian-square multipliers along its paths have positive averaged asymptotic midpoint moduli and admit no equivalent asymptotically uniformly convex norm. The renorming obstruction holds for every positive nonconstant mean-one multiplier with finite second moment.
Midpoint convexity from two recursive potentials
September 27, 2026 · source · Lean formalization available · cite as \cite{OAI:Midpoint-convexity-from-two-recursive-potentials-September-27-2026}
We study tree norms computed by two least nonnegative fields whose difference is the vector. For Euclidean child aggregation, two root-sum spaces have an averaged asymptotic midpoint modulus of at least t^3/128 for 0\lt t\lt 1, including a reflexive joining-root space. A reflexive construction with a fixed zero root also satisfies a homogeneous cubic estimate. These spaces admit no equivalent asymptotically uniformly convex norm. We also obtain sixth-power and cubic estimates when the aggregation exponent depends on the height of a finite component.
Result 331 · Functional analysis. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.
Source: https://github.com/openai/math/blob/main/CONTENTS.md