Almost-Everywhere Alexandrov Expansion

This formalizes Alexandrov's second-order expansion theorem in the finite-dimensional inner-product setting.

Let $E$ be a finite-dimensional real inner-product space with measurable and Borel structures, and let $f:E\to\mathbb R$ be convex on all of $E$. For almost every $x$ with respect to Lebesgue measure, there exist $p\in E$ and a continuous linear map $B:E\to E$ such that:

1. $B$ is symmetric:

2. $p$ is the unique subgradient of $f$ at $x$.
3. For every $\varepsilon>0$, for all $y$ sufficiently near $x$,

The declaration ae_exists_secondOrder_expansion_readable is the main almost-everywhere second-order expansion interface for later convex-analytic arguments. The almost-everywhere quantifier is with respect to volume.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem ae_exists_secondOrder_expansion {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {f : E → ℝ}
    (hconv : ConvexOn ℝ univ f) :
    ∀ᵐ x ∂(volume : Measure E), ∃ p : E, ∃ B : E →L[ℝ] E,
      (∀ v w, ⟪B v, w⟫ = ⟪v, B w⟫) ∧
      (∀ q : E, (∀ y, f x + ⟪q, y - x⟫ ≤ f y) → q = p) ∧
      ∀ ε > 0, ∀ᶠ y in 𝓝 x,
        |f y - f x - ⟪p, y - x⟫ - (1 / 2) * ⟪B (y - x), y - x⟫| ≤ ε * ‖y - x‖ ^ 2

Module navigation

Module: Analysis/Convex/SecondOrder.

Selected supporting theorems: eventually_abs_sub_quadratic_le_of_subgradient_expansion, exists_subgradient_slope_le_inner_add, inner_hasFDerivAt_resolvent_symm, lipschitzWith_proximalPoint, subgradient_expansion_of_hasFDerivAt_resolvent.

Previous: integral_mul_le_integral_mul_sum_iteratedFDeriv.

Source excerpt, lines 600–607 · Frozen source 408915f.