Coordinate Alexandrov Expansion

This is the coordinate form of an almost-everywhere second-order expansion.

Let $n\in\mathbb N$, let $u:\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))\to\mathbb R$ be convex on the whole space, and use the coordinate quadratic polynomial quadraticAt. For almost every $x$, there exist a real matrix $B$ and a vector $g$ such that:

1. $B$ is Hermitian, equivalently symmetric over $\mathbb R$.
2. For every $\varepsilon>0$, for all $y$ sufficiently near $x$,

The declaration ae_exists_quadraticAt_expansion_readable translates the abstract symmetric linear operator in ae_exists_secondOrder_expansion_readable into a matrix on EuclideanSpace ℝ (Fin n). It makes no restriction such as $n\ge1$.

Original Lean declaration header

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

theorem ae_exists_quadraticAt_expansion {n : ℕ} {u : EuclideanSpace ℝ (Fin n) → ℝ}
    (hconv : ConvexOn ℝ univ u) :
    ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      ∃ B : Matrix (Fin n) (Fin n) ℝ, B.IsHermitian ∧ ∃ g : EuclideanSpace ℝ (Fin n),
        ∀ ε > 0, ∀ᶠ y in 𝓝 x, |u y - quadraticAt B x g (u x) y| ≤ ε * ‖y - x‖ ^ 2

Module navigation

Module: Analysis/Convex/Viscosity.

Definition modules: Analysis/Convex/Alexandrov.

Supporting theorems: ae_exists_secondOrder_expansion.

Previous: posDef_and_convolution_le_log_det_hessianMatrix · Next: exists_penalized_maximum_with_comparison.

Source excerpt, lines 1412–1416 · Frozen source 408915f.