DeGiorgiOneSided

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Dimension-complete one-sided De Giorgi core

This file joins the local two-dimensional endpoint to the upstream core for dimensions at least three.

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

The one-sided De Giorgi core in every dimension at least two.