Lower Touching Determinant Inequality

This is a lower touching test for an Alexandrov solution.

Let $u,f,\psi:\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin}(n))\to\mathbb R$, let $\Omega$ be open, and assume:

1. $u$ is convex on the whole space;
2. for every open $G\subseteq\Omega$, the volume of its subgradientImage u G equals

$$\int_G \operatorname{ofReal}(f(x))\,d\operatorname{vol}(x);$$

3. $x_0\in\Omega$, $f$ is continuous at $x_0$, and $0\le f(x_0)$;
4. $\psi$ is $C^2$ at $x_0$ and hessianMatrix ψ x₀ is positive semidefinite;
5. $u(x_0)=\psi(x_0)$ and, almost everywhere near $x_0$, $\psi(x)\le u(x)$.

Then

$$\det(\operatorname{hessianMatrix}(\psi,x_0))\le f(x_0).$$

This is the formalized weak Alexandrov/viscosity lower inequality. The volume identity uses ENNReal.ofReal inside an L¹ integral, while the conclusion is an ordinary real inequality.

Original Lean declaration header

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

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

Module navigation

Module: Analysis/Convex/Viscosity.

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

Supporting theorems: convexOn_quadraticAt, subgradientImage_subset_of_le, volume_subgradientImage_quadraticAt_aux, hessianMatrix_quadratic, local_taylor_two.

Previous: le_det_hessianMatrix_of_upper_touch · Next: hessianMatrix_quadraticAt.

Source excerpt, lines 655–663 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Viscosity

open FunctionalInequalities.Probability.Stein
open MeasureTheory Set Metric Filter
open scoped RealInnerProductSpace ENNReal Topology
set_option maxHeartbeats 800000

theorem FunctionalInequalities.Analysis.det_hessianMatrix_le_of_lower_touch_readable {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₀) (hf0 : 0 ≤ f x₀)
    (hψ : ContDiffAt ℝ 2 ψ x₀) (hH : (hessianMatrix ψ x₀).PosSemidef)
    (hcontact : u x₀ = ψ x₀) (htouch : ∀ᶠ x in 𝓝 x₀, ψ x ≤ u x) :
    (hessianMatrix ψ x₀).det ≤ f x₀ := by sorry