RootProviderFinal

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

1. The degenerate zero-dimensional energy

2. The endpoint at every dimension

theorem Algsuperdiff.Section4.Provider.Regularity.anomalous_regularity_provider_final (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (C : ℝ), 0 < gamma0 ∧ 0 < C ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (alpha : ℝ), 0 < alpha → alpha ≤ 1 - C * √M.gamma → ∀ (m : ℤ), ∃ (X : Section3.Cutoff.CutoffSample d → ℕ∞), Measurable X ∧ (∀ (N : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | ↑N ≤ X omega} ≤ ENNReal.ofReal (C * Real.exp (-((1 - alpha) ^ 2 * (↑N - C)) / (C * M.gamma)))) ∧ ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (L : ℤ), m ≤ L → ∀ (u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg Kh : ℝ), Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u h g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad → (∀ y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad y‖ ≤ Real.rpow 3 (↑m / 2) * Kh) → Support.HasGradientOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) h.toFun h.grad → ∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ∀ n ≤ m, X omega ≤ ↑(m - n).toNat → ENNReal.ofReal √M.nu * MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (u.grad y))) 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ≤ ENNReal.ofReal (C * Real.rpow 3 ((1 - alpha) * (↑m - ↑n))) * (ENNReal.ofReal √M.nu * MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (u.grad y))) 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) + ENNReal.ofReal (√(↑(Section3.Annealed.sigmaBar M m))⁻¹ * Real.rpow 3 (↑m / 2) * Kg) + ENNReal.ofReal (√↑(Section3.Annealed.sigmaBar M m) * Real.rpow 3 (↑m / 2) * Kh)) ∧ (x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)) → ENNReal.ofReal √M.nu * MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (u.grad y))) 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ≤ ENNReal.ofReal (C * Real.rpow 3 ((1 - alpha) * (↑m - ↑n))) * (ENNReal.ofReal √M.nu * MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (u.grad y))) 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) + ENNReal.ofReal (√(↑(Section3.Annealed.sigmaBar M m))⁻¹ * Real.rpow 3 (↑m / 2) * Kg)))