SeedControl

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

Seed control for localized regularity

The volume-normalized mean oscillation of a rough-field solution is controlled by its essential-supremum distance from the constant-coefficient comparator and the uniform bound for that comparator.

theorem Algsuperdiff.Section5.Provider.exists_seedControl (d : ℕ) (hdim : 2 ≤ d) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) (g : HCPolySupport.Vec d → HCPolySupport.Vec d), Support.NormalizedForceAt y n g → ∀ (u : HCPolySupport.H1Function (Support.cubeSetAt y n)), Support.IsDirichletSolutionAt (Section3.Cutoff.coefficientCutoff M.nu n omega).toCoeffField y n u g → ENNReal.ofReal (↑(Section3.Annealed.sigmaBar M n) * Real.rpow 3 (-↑n)) * MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => u.toFun x - HCPolySupport.volumeAverage (Support.cubeSetAt y n) u.toFun) 2 (Section4.Support.normalizedVolumeMeasureOn (Support.cubeSetAt y n)) ≤ ENNReal.ofReal C * (1 + Support.localizedError M n y omega)

The normalized seed at every scale is bounded by the localized error and a dimension-dependent constant.