CutoffSampleRange

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

Transfer of lower-stream independence to the genuine cutoff carrier

The cutoff carrier is a full-measure subtype. This module transfers completed lower-stream independence to it using Borel local representatives, so no unjustified claim that a completion is contained in the ambient Borel sigma field is needed.

theorem Algsuperdiff.Section3.Cutoff.indep_cutoffSampleLocalSigma_of_indep_completion {d : ℕ} (M : ABKModel d) (m : ℤ) (U V : Set (HCPolySupport.Vec d)) (h : ProbabilityTheory.Indep (lowerShellLocalCompletion M m U) (lowerShellLocalCompletion M m V) ↑M.P) : ProbabilityTheory.Indep (cutoffSampleLocalSigma M m U) (cutoffSampleLocalSigma M m V) ↑(cutoffSampleLaw M)

A.e.-completed lower-stream independence descends faithfully to the full-measure cutoff subtype.