CoefficientLocality

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

Integral-locality of the actual coefficient cutoff

The deterministic nu I shift is handled at local entry-test generators. It therefore preserves the exact LocalSigmaR information of the genuine cutoff.

theorem Algsuperdiff.Section3.Cutoff.measurable_const_add_local {d : ℕ} (c : HCPolySupport.RegCoeffField d) (U : Set (HCPolySupport.Vec d)) : Measurable fun (a : HCPolySupport.RegCoeffField d) => c + a

Addition of a deterministic regular field preserves every integral-generated local sigma-field.

theorem Algsuperdiff.Section3.Cutoff.measurable_coefficientCutoff_local {d : ℕ} (M : ABKModel d) (m : ℤ) (U : Set (HCPolySupport.Vec d)) : Measurable (coefficientCutoff M.nu m)

The actual coefficient field a_m = nu I + k_m reads only the same local integral information as the lower-infinite cutoff.