LowerShellRange

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

Range dependence of the lower shell stream

The lower stream is a countable join over the exact indices m-r. Its range proof combines ShellRange with the refined independent-pairs theorem, then uses the explicitly defined a.e. completion needed by the genuine cutoff.

theorem Algsuperdiff.Section3.Cutoff.indep_lowerShellLocalSigma_of_cutoff_separation {d : ℕ} (M : ABKModel d) (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 (lowerShellLocalSigma m U) (lowerShellLocalSigma m V) ↑M.P

The two lower-shell integral-local sigma-fields are independent whenever the observation regions are separated by the literal cutoff range.

theorem Algsuperdiff.Section3.Cutoff.indep_lowerShellLocalCompletion_of_cutoff_separation {d : ℕ} (M : ABKModel d) (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 (lowerShellLocalCompletion M m U) (lowerShellLocalCompletion M m V) ↑M.P

Completion by ambient null sets preserves the lower-stream range independence. This is the input used to make the actual infinite cutoff local, rather than an unproved direct restriction-field assertion.