Stage 2, Route C: quantitative ell_p convexity

This file isolates the Clarkson / Ball--Carlen--Lieb route to O3.belowGeometry. The key point of the investigation is that Mathlib's abstract UniformConvexSpace class exposes only an existential modulus. The exact quantitative input needed here is therefore recorded explicitly below, but only as a proposition carrier, never as an assumption or an axiom.

theorem O3.Stage2RouteC.lpNorm_eq_piLpNorm {p : ℝ} (hp : 1 ≤ p) {d : ℕ} (x : Point d) : lpNorm p x = ‖WithLp.toLp (ENNReal.ofReal p) x‖

The literal O3 norm is definitionally the finite PiLp norm after the standard ENNReal.ofReal exponent conversion.

theorem O3.Stage2RouteC.lpNorm_smul {p : ℝ} (hp : 1 ≤ p) {d : ℕ} (a : ℝ) (x : Point d) : lpNorm p (a • x) = |a| * lpNorm p x

Homogeneity of the literal O3 norm, obtained without changing norms by transporting to Mathlib's finite PiLp norm.

theorem O3.Stage2RouteC.lpNorm_two_sq {d : ℕ} (x : Point d) : lpNorm 2 x ^ 2 = ∑ i : Fin d, x i ^ 2

At the endpoint p = 2, the transport reduces the literal O3 norm to the usual finite sum of coordinate squares.

theorem O3.Stage2RouteC.ballCarlenLieb_at_two {d : ℕ} (u v : Point d) : lpNorm 2 (u + v) ^ 2 + (2 - 1) * lpNorm 2 (u - v) ^ 2 ≤ 2 * (lpNorm 2 u ^ 2 + lpNorm 2 v ^ 2)

Endpoint sanity check: BCL is the parallelogram identity at p = 2. This covers arbitrary dimension and all zero cases.

theorem O3.Stage2RouteC.lpNorm_fin_one {p : ℝ} (hp : 0 < p) (x : Point 1) : lpNorm p x = |x 0|

In one dimension the literal ell_p norm is absolute value for every positive real exponent.

theorem O3.Stage2RouteC.ballCarlenLieb_fin_one {p : ℝ} (hp : 1 < p) (hp2 : p ≤ 2) (u v : Point 1) : lpNorm p (u + v) ^ 2 + (p - 1) * lpNorm p (u - v) ^ 2 ≤ 2 * (lpNorm p u ^ 2 + lpNorm p v ^ 2)

One-dimensional sanity check for the whole real range 1 < p ≤ 2. The exact coefficient follows from a scalar square identity.

noncomputable def O3.Stage2RouteC.BallCarlenLiebStatement : Prop

The exact Ball--Carlen--Lieb inequality needed by Route C. This is a transparent proposition describing the first missing quantitative input; it is not registered as a theorem and is not used as a hidden hypothesis of the O3 target.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def O3.Stage2RouteC.ExactMidpointStatement : Prop

Exact midpoint form of (p-1)-strong convexity for the squared ell_p norm. It is the quantitative form that an unspecified uniform-convexity modulus cannot supply.

Equations

• One or more equations did not get rendered due to their size.

theorem O3.Stage2RouteC.ballCarlenLieb_implies_exactMidpoint (hBCL : BallCarlenLiebStatement) : ExactMidpointStatement

The exact BCL inequality implies the exact midpoint strong-convexity inequality with no loss in the coefficient.