ShellRange

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

Range dependence of one scaled shell

This is the J1-to-one-shell step for the exact integral-local sigma-fields. It is kept separate from the countable lower-tail aggregation.

theorem Algsuperdiff.Section3.Cutoff.indep_shellLocal_of_cutoff_separation {d : ℕ} (M : ABKModel d) (m n : ℤ) (hnm : n ≤ m) (U V : Set (HCPolySupport.Vec d)) (hU : MeasurableSet U) (hV : MeasurableSet V) (hsep : ∀ ⦃x y : HCPolySupport.Vec d⦄, x ∈ U → y ∈ V → √↑d * 3 ^ m ≤ HCPolySupport.Book.Ch02.vecNorm (x - y)) : ProbabilityTheory.Indep (MeasurableSpace.comap (fun (omega : ℤ → Frozen.Assumptions.ShellField d) => omega n) (Frozen.Assumptions.ShellField.lihLocalSigma U)) (MeasurableSpace.comap (fun (omega : ℤ → Frozen.Assumptions.ShellField d) => omega n) (Frozen.Assumptions.ShellField.lihLocalSigma V)) ↑M.P

A shell at index n ≤ m has integral-local range at most the cutoff's natural range sqrt(d) * 3^m, solely from J1 and marginal scaling.