DeGiorgiOneSidedTwo

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

The two-dimensional one-sided De Giorgi core

The endpoint recurrence has coefficient C² L E₀². The additional factor L exactly cancels against the square volume and a threshold of size Cd L E₀ in the iteration admissibility condition.

theorem DivergenceFormProcess.Regularity.deGiorgi_admissible_two {C Cd L E₀ : ℝ} (hC : 0 ≤ C) (hCd : 0 < Cd) (hchoice : 4 * C ≤ Cd) (hL : 0 < L) (hE₀ : 0 < E₀) : (C ^ 2 * L * E₀ ^ 2 / (Cd * L * E₀) ^ 2) ^ 2 * 16 * (L ^ 2) ^ 1 ≤ 16 ^ (-(1 / 1))

The direct endpoint admissibility calculation. It replaces the dimension-dependent calculation used by the d ≥ 3 core.

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

The dimension-two one-sided De Giorgi core.