AnomalousRegularity

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

Anomalous regularity — [ABK] Theorem C (t.regularity)

For a disorder model of strength gamma small enough, and every Hölder exponent alpha below 1 - C sqrt gamma, there is an almost surely finite minimal scale X with an exponential tail such that, above X, every Dirichlet solution on a triadic cube with C^{0,1/2} force g and C^{1,1/2} boundary datum h satisfies the C^{0,alpha} large-scale excess decay 3^{(1-alpha)(m-n)} between any two scales n <= m.

Proved; reduces to the standard axioms.

theorem Algsuperdiff.Frozen.Section4.anomalous_regularity (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 : ℝ), Section4.Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u h g → Section4.Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → Section4.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) → Section4.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 (Section4.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 (Section4.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 (Section4.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 (Section4.Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) + ENNReal.ofReal (√(↑(Section3.Annealed.sigmaBar M m))⁻¹ * Real.rpow 3 (↑m / 2) * Kg)))