DivergenceDeGiorgiBound

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

theorem DivergenceFormProcess.Regularity.exists_deGiorgi_bound_constant {d : ℕ} (hd : 2 ≤ d) : ∃ (Cd : ℝ), 0 ≤ Cd ∧ ∀ (z : HCPolySupport.Vec d) (L : ℝ), 0 < L → ∀ (a : HCPolySupport.CoeffField d) (lam Lam : ℝ), 0 < lam → HCPolySupport.IsEllipticFieldOn lam Lam (HCPolySupport.axisCube z L) a → ∀ (u : HCPolySupport.H10Function (HCPolySupport.axisCube z L)) (g : HCPolySupport.Vec d → HCPolySupport.Vec d), HCPolySupport.IsZeroTraceDirichletRhsWeakSolution a (HCPolySupport.axisCube z L) u g → Measurable u.toFun → HCPolySupport.MemVectorL2 (HCPolySupport.axisCube z L) g → ∀ (M : ℝ), 0 ≤ M → (∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (HCPolySupport.axisCube z L), √(HCPolySupport.vecNormSq (g x)) ≤ M) → ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (HCPolySupport.axisCube z L), |u.toFun x| ≤ Cd * L * (√↑d / lam * M)

The De Giorgi constant of the dimension. In every dimension at least two there is one nonnegative constant with the following property: on every axis cube, for every coefficient field elliptic there, every measurable zero-trace weak solution with a divergence forcing bounded by M obeys the De Giorgi bound with that constant. The constant stands outside the cube, its side length, the coefficient field, both ellipticity constants, the solution, the forcing and its bound, so it depends on the dimension alone.