DeGiorgiCore

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

The generic one-sided De Giorgi core

The purely analytic heart of the coupled Stampacchia estimate on an axis cube U = axisCube z L. Given two H¹ functions w₁, w₂ sharing a boundary trace, a median m₀ with the one-sided median inequality, and the level-energy estimate in F4-RHS shape, the essential supremum of w₁ − m₀ over U is bounded by C_d · L · E₀.

The proof combines the truncation toolbox (D1, D4), the matched-pair Sobolev inequality (F4), Chebyshev (real_chebyshev_level), the squared level recursion (sq_level_recursion_of_le), the admissibility algebra (deGiorgi_admissible) and the iteration engine (deGiorgi_levelVolume_tendsto_zero).

theorem HCPolySupport.deGiorgi_one_sided_core {d : ℕ} (hd : 3 ≤ d) : ∃ (Cd : ℝ), 0 ≤ Cd ∧ ∀ (z : Vec d) (L : ℝ), 0 < L → ∀ (w₁ w₂ : H1Function (axisCube z L)), Measurable w₁.toFun → Measurable w₂.toFun → (MemH10 (axisCube z L) fun (x : Vec d) => w₁.toFun x - w₂.toFun x) → ∀ (m₀ E₀ : ℝ), 0 ≤ E₀ → MeasureTheory.volume {x : Vec d | x ∈ axisCube z L ∧ m₀ < w₁.toFun x} + MeasureTheory.volume {x : Vec d | x ∈ axisCube z L ∧ m₀ < w₂.toFun x} ≤ MeasureTheory.volume (axisCube z L) → (∀ (k : ℝ), 0 ≤ k → ∑ i : Fin d, (MeasureTheory.eLpNorm ({x : Vec d | x ∈ axisCube z L ∧ m₀ + k < w₁.toFun x}.indicator fun (x : Vec d) => w₁.grad x i) 2 (volumeMeasureOn (axisCube z L))).toReal + ∑ i : Fin d, (MeasureTheory.eLpNorm ({x : Vec d | x ∈ axisCube z L ∧ m₀ + k < w₂.toFun x}.indicator fun (x : Vec d) => w₂.grad x i) 2 (volumeMeasureOn (axisCube z L))).toReal ≤ E₀ * √((MeasureTheory.volume {x : Vec d | x ∈ axisCube z L ∧ m₀ + k < w₁.toFun x}).toReal + (MeasureTheory.volume {x : Vec d | x ∈ axisCube z L ∧ m₀ + k < w₂.toFun x}).toReal)) → ∀ᵐ (x : Vec d) ∂volumeMeasureOn (axisCube z L), w₁.toFun x ≤ m₀ + Cd * L * E₀

Generic one-sided De Giorgi core.

There is a dimensional constant Cd ≥ 0 such that: for every axis cube U = axisCube z L of side L > 0, every pair w₁ w₂ : H1Function U with measurable representatives sharing a trace (w₁ − w₂ ∈ H¹₀), every median level m₀ obeying the one-sided median inequality, and every level-energy bound with constant E₀ ≥ 0 in F4-RHS shape, one has w₁ ≤ m₀ + Cd·L·E₀ almost everywhere on U.