RangeDependence

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

The natural spatial range of the actual cutoff law

ABK26 records that the lower-infinite cutoff k_m, and hence the actual coefficient a_m = nu I + k_m, has dependence range sqrt(d) * 3^m. This file owns that literal scale vocabulary. The proof of independence itself is intentionally downstream of the local-limit A: it must show that the actual Cutoff.coefficientCutoffLaw reads only the lower-shell restriction sigma-field, and then combine J1 with the prefix's cross-shell independence. It must not be replaced by an assumption on a free coefficient law.

noncomputable def Algsuperdiff.Section3.Cutoff.cutoffNaturalRange (d : ℕ) (m : ℤ) : ℝ

The exact spatial dependence range of the actual cutoff at shell scale m, as stated in ABK26. This is the Euclidean range used by J1; the later proof converts it to CoarseGraining's ambient unit-range condition only after a triadic scale normalization.

Equations

• Algsuperdiff.Section3.Cutoff.cutoffNaturalRange d m = √↑d * 3 ^ m

@[simp]

theorem Algsuperdiff.Section3.Cutoff.cutoffNaturalRange_zero (d : ℕ) : cutoffNaturalRange d 0 = √↑d

At scale zero the natural range is exactly sqrt d, matching the J1 normalization of the zero shell.