Alexandrov Upper Touching Determinant Inequality

Let $u,f:\mathbb R^n\to\mathbb R$, let $\Omega$ be open, and assume $u$ is convex. Suppose that for every open $G\subseteq\Omega$,

with the integral interpreted in $[0,\infty]$. If $x_0\in\Omega$, $f$ is continuous at $x_0$, $\psi\in C^2$ at $x_0$, $u(x_0)=\psi(x_0)$, and $u\le\psi$ near $x_0$, then

This is the stated Alexandrov-to-viscosity determinant inequality.

Original Lean declaration header

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

theorem le_det_hessianMatrix_of_upper_touch {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₀)
    (hψ : ContDiffAt ℝ 2 ψ x₀) (hcontact : u x₀ = ψ x₀) (htouch : ∀ᶠ x in 𝓝 x₀, u x ≤ ψ x) :
    f x₀ ≤ (hessianMatrix ψ x₀).det

Module navigation

Module: Analysis/Convex/Viscosity.

Definition modules: Analysis/BakryEmery/HessianOperator, Analysis/Convex/Subgradient.

Selected supporting theorems: convexOn_quadraticAt, posSemidef_hessianMatrix_of_upper_touch, subgradientImage_subset_of_le, volume_subgradientImage_quadraticAt_aux, hessianMatrix_quadratic.

Previous: local_taylor_two · Next: det_hessianMatrix_le_of_lower_touch.

Source excerpt, lines 551–558 · Frozen source 408915f.