DeGiorgiIterationTwo

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

The two-dimensional De Giorgi level recurrence

The H¹ ↪ L⁴ matched-pair inequality in dimension two has an additional sqrt L factor. After truncation, Chebyshev, and squaring, this gives the scale-correct coefficient C² L E₀² in the level-volume recurrence.

theorem DivergenceFormProcess.Regularity.deGiorgi_levelRecursion_two : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (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)) → ∀ (k l : ℝ), 0 ≤ k → k < l → (l - k) ^ 2 * ((MeasureTheory.volume {x : HCPolySupport.Vec 2 | x ∈ HCPolySupport.axisCube z L ∧ m₀ + l < w₁.toFun x}).toReal + (MeasureTheory.volume {x : HCPolySupport.Vec 2 | x ∈ HCPolySupport.axisCube z L ∧ m₀ + l < w₂.toFun x}).toReal) ^ (1 / 2) ≤ C ^ 2 * L * E₀ ^ 2 * ((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)

The dimension-two combined upper-level volumes satisfy the De Giorgi recurrence with exponent 1 / 2 and coefficient C² L E₀².