Positive Hessian and Determinant from Quadratic Expansion

Let $u,f:\mathbb R^n\to\mathbb R$, let $\Omega$ be open, and assume $u$ is convex and satisfies the Alexandrov identity

for every open $G\subseteq\Omega$. If $x_0\in\Omega$, $f$ is continuous at $x_0$ with $f(x_0)>0$, and there are a Hermitian matrix $B$ and vector $g$ such that, for every $\varepsilon>0$,

near $x_0$, then

This is a pointwise Monge–Ampère identification at second-order differentiability points.

Original Lean declaration header

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

theorem posDef_and_det_eq_of_quadratic_expansion {n : ℕ} {u f : EuclideanSpace ℝ (Fin n) → ℝ}
    (hconv : ConvexOn ℝ univ u) {Ω : Set (EuclideanSpace ℝ (Fin n))} (hΩ : IsOpen Ω)
    (hMA : ∀ G : Set (EuclideanSpace ℝ (Fin n)), IsOpen G → G ⊆ Ω →
      (volume : Measure (EuclideanSpace ℝ (Fin n))) (subgradientImage u G) =
        ∫⁻ x in G, ENNReal.ofReal (f x) ∂(volume : Measure (EuclideanSpace ℝ (Fin n))))
    {x₀ : EuclideanSpace ℝ (Fin n)} (hx₀ : x₀ ∈ Ω) (hf : ContinuousAt f x₀) (hfpos : 0 < f x₀)
    {B : Matrix (Fin n) (Fin n) ℝ} (hB : B.IsHermitian) {g : EuclideanSpace ℝ (Fin n)}
    (hexp : ∀ ε > 0, ∀ᶠ x in 𝓝 x₀, |u x - quadraticAt B x₀ g (u x₀) x| ≤ ε * ‖x - x₀‖ ^ 2) :
    B.PosDef ∧ B.det = f x₀

Module navigation

Module: Analysis/Convex/Viscosity.

Definition modules: Analysis/Convex/Alexandrov, Analysis/Convex/Subgradient.

Supporting theorems: det_hessianMatrix_le_of_lower_touch, hessianMatrix_quadraticAt, le_det_hessianMatrix_of_upper_touch, posSemidef_hessianMatrix_of_upper_touch.

Previous: hessianMatrix_quadraticAt · Next: expansion_secondDifference.

Source excerpt, lines 912–920 · Frozen source 408915f.