ErrorMoment

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

A renormalization amplitude for the localized error

The generator-renormalization estimate is uniform over the normalized forcing class. This module compares its constant-coefficient solution with the canonical comparator used in localizedError.

Comparator rescaling

theorem Algsuperdiff.Section5.Provider.isDirichletSolutionAt_rescale_constant {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {sigma tau : ℝ} (htau : 0 < tau) {v : HCPolySupport.H1Function (Support.cubeSetAt y n)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hv : Support.IsDirichletSolutionAt (fun (x : HCPolySupport.Vec d) => sigma • 1) y n v g) : Support.IsDirichletSolutionAt (fun (x : HCPolySupport.Vec d) => tau • 1) y n ((sigma / tau) • v) g

A solution for sigma • 1 rescales to a solution with the same forcing for tau • 1.

Reading a pointwise estimate as an essential-supremum estimate

The comparator swap

theorem Algsuperdiff.Section5.Provider.localizedError_origin_le_of_renormalization {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (omega : Section3.Cutoff.CutoffSample d) {sigma E B : ℝ} (hsigma : 0 < sigma) (hE : 0 ≤ E) (hB : 0 ≤ B) (hren : ∀ (g : HCPolySupport.Vec d → HCPolySupport.Vec d), Support.NormalizedForceAt 0 n g → ∀ (u : HCPolySupport.H1Function (Support.cubeSetAt 0 n)), Support.IsDirichletSolutionAt (Section3.Cutoff.coefficientCutoff M.nu n omega).toCoeffField 0 n u g → ∀ (w : HCPolySupport.H1Function (Support.cubeSetAt 0 n)), Support.IsDirichletSolutionAt (fun (x : HCPolySupport.Vec d) => sigma • 1) 0 n w g → ENNReal.ofReal (sigma * Real.rpow 3 (-↑n)) * MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => u.toFun x - w.toFun x) ⊤ (MeasureTheory.volume.restrict (Support.cubeSetAt 0 n)) ≤ ENNReal.ofReal E) (hcomp : ∀ (g : HCPolySupport.Vec d → HCPolySupport.Vec d), Support.NormalizedForceAt 0 n g → ∀ (v : HCPolySupport.H1Function (Support.cubeSetAt 0 n)), Support.IsDirichletSolutionAt (fun (x : HCPolySupport.Vec d) => ↑(Section3.Annealed.sigmaBar M n) • 1) 0 n v g → ENNReal.ofReal (↑(Section3.Annealed.sigmaBar M n) * Real.rpow 3 (-↑n)) * MeasureTheory.eLpNorm v.toFun ⊤ (MeasureTheory.volume.restrict (Support.cubeSetAt 0 n)) ≤ ENNReal.ofReal B) : Support.localizedError M n 0 omega ≤ ENNReal.ofReal (↑(Section3.Annealed.sigmaBar M n) / sigma * E + |↑(Section3.Annealed.sigmaBar M n) / sigma - 1| * B)

The normalized error for the canonical comparator is controlled by the renormalization error and the explicit cost of changing the scalar.

theorem Algsuperdiff.Section5.Provider.exists_comparator_eLpNorm_bound (d : ℕ) (hdim : 2 ≤ d) : ∃ (B : ℝ), 0 < B ∧ ∀ (M : Section3.ABKModel d) (n : ℤ) (g : HCPolySupport.Vec d → HCPolySupport.Vec d), Support.NormalizedForceAt 0 n g → ∀ (v : HCPolySupport.H1Function (Support.cubeSetAt 0 n)), Support.IsDirichletSolutionAt (fun (x : HCPolySupport.Vec d) => ↑(Section3.Annealed.sigmaBar M n) • 1) 0 n v g → ENNReal.ofReal (↑(Section3.Annealed.sigmaBar M n) * Real.rpow 3 (-↑n)) * MeasureTheory.eLpNorm v.toFun ⊤ (MeasureTheory.volume.restrict (Support.cubeSetAt 0 n)) ≤ ENNReal.ofReal B

Every canonical comparator has the explicit normalized essential-supremum bound supplied by the cube Schauder estimate.

theorem Algsuperdiff.Section5.Provider.exists_localizedError_origin_bound (d : ℕ) (cstar : ℝ) (hdim : 2 ≤ d) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (C : ℝ) (K : ℝ) (B : ℝ), 0 < gamma0 ∧ 0 < C ∧ 0 < K ∧ 0 < B ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (n : ℤ), ∃ (sigma : ℝ) (EB : Section3.Cutoff.CutoffSample d → ℝ), 0 < sigma ∧ (∀ (omega : Section3.Cutoff.CutoffSample d), 0 ≤ EB omega) ∧ Measurable EB ∧ (∀ (p : ℝ), 1 ≤ p → p ≤ C⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹ → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (EB omega) ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ p) ∧ ↑(Section3.Annealed.sigmaBar M n) / sigma ≤ 2 ∧ |↑(Section3.Annealed.sigmaBar M n) / sigma - 1| ≤ 4 * K * √M.gamma * |Real.log M.gamma| ∧ ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), Support.localizedError M n 0 omega ≤ ENNReal.ofReal (↑(Section3.Annealed.sigmaBar M n) / sigma * EB omega + |↑(Section3.Annealed.sigmaBar M n) / sigma - 1| * B)

The generator-renormalization estimate, specialized at zero boundary datum and the normalized forcing scale, bounds the localized error at the origin after the canonical-comparator swap.

Moment packaging

theorem Algsuperdiff.Section5.Provider.lintegral_localizedError_rpow_le_of_rescaled_bound {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) {EB : Section3.Cutoff.CutoffSample d → ℝ} {t D R p : ℝ} (hp : 1 ≤ p) (ht : 0 ≤ t) (hD : 0 ≤ D) (hR : 0 ≤ R) (hEB : Measurable EB) (hEBnn : ∀ (omega : Section3.Cutoff.CutoffSample d), 0 ≤ EB omega) (hpoint : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), Support.localizedError M n 0 omega ≤ ENNReal.ofReal (t * EB omega + D)) (hmom : ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (EB omega) ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal R ^ p) : ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.localizedError M n 0 omega ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (t * R + D) ^ p

A uniform almost-everywhere bound by a rescaled random amplitude plus a deterministic comparator cost gives the corresponding two-term moment bound.

theorem Algsuperdiff.Section5.Provider.localizedError_moment_bound (d : ℕ) (cstar : ℝ) (hdim : 2 ≤ d) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (C' : ℝ), 0 < gamma0 ∧ 0 < C' ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (p : ℝ) (n : ℤ) (y : HCPolySupport.Vec d), 1 ≤ p → p ≤ C'⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹ → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.localizedError M n y omega ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C' * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ p

The localized error has the generator-renormalization moment profile, with a new constant absorbing the canonical-comparator swap.