Alexandrov Maximum Principle

This formalizes the Alexandrov maximum principle, cited as Theorem 1.4.2 in Gutiérrez's treatment of the Monge–Ampère equation.

Let $E$ be a nontrivial finite-dimensional real inner-product space with measurable and Borel structures, and write $n=\dim E$. There exists $c>0$, depending only on $E$, such that for every convex $u:E\to\mathbb R$, every bounded open convex $\Omega$, and every $x_0\in\Omega$ with $u(x_0)<0$ and $u\ge0$ on $\partial\Omega$,

The volume is an ENNReal value and the real factors are embedded with ofReal. The declaration is exists_pos_alexandrov_maximum_principle_readable.

Original Lean declaration header

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

theorem exists_pos_alexandrov_maximum_principle [FiniteDimensional ℝ E] [Nontrivial E] [MeasurableSpace E]
    [BorelSpace E] :
    ∃ c : ℝ, 0 < c ∧ ∀ (u : E → ℝ), ConvexOn ℝ univ u → ∀ (Ω : Set E), IsOpen Ω → Convex ℝ Ω →
      Bornology.IsBounded Ω → (∀ x ∈ frontier Ω, 0 ≤ u x) → ∀ x₀ ∈ Ω, u x₀ < 0 →
      ENNReal.ofReal (c * (-u x₀) ^ Module.finrank ℝ E) ≤
        (volume : Measure E) (subgradientImage u Ω) *
          ENNReal.ofReal (diam Ω ^ (Module.finrank ℝ E - 1) * infDist x₀ (frontier Ω))

Module navigation

Module: Analysis/Convex/Alexandrov.

Definition modules: Analysis/Convex/Subgradient.

Supporting theorems: exists_pos_volume_convexHull_closedBall_union_singleton_ge, exists_unit_inner_le_infDist_frontier, mem_subgradientImage_of_affine_le_of_nonneg_frontier.

Previous: exists_pos_volume_convexHull_closedBall_union_singleton_ge · Next: quadraticAt_subgradient_iff.

Source excerpt, lines 1220–1226 · Frozen source 408915f.