LocalLimit

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

Integral-local measurability of the genuine lower cutoff

This module promotes finite lower-cutoff locality to the genuine lower-infinite cutoff. The target is the manuscript/CoarseGraining integral-local sigma-field LocalSigmaR U: compactly supported entry tests in U are limits of the corresponding finite lower-cutoff tests. The limit is taken on the public CutoffSample carrier, where lower-tail convergence is genuine, while the domain sigma-field is the explicit lower-shell completion.

This proves local observability. Spatial independence and its exact range remain separate consequences, and are not asserted here.

@[reducible, inline]

abbrev Algsuperdiff.Section3.Cutoff.cutoffSampleLocalSigma {d : ℕ} (M : ABKModel d) (m : ℤ) (U : Set (HCPolySupport.Vec d)) : MeasurableSpace (CutoffSample d)

The local information on the public cutoff carrier induced from the completed lower-shell local sigma-field on the canonical shell sequence.

Equations

• Algsuperdiff.Section3.Cutoff.cutoffSampleLocalSigma M m U = MeasurableSpace.comap Subtype.val (Algsuperdiff.Section3.Cutoff.lowerShellLocalCompletion M m U)

theorem Algsuperdiff.Section3.Cutoff.measurable_entryTestR_cutoff_local {d : ℕ} (M : ABKModel d) (m : ℤ) (U : Set (HCPolySupport.Vec d)) (i j : Fin d) {phi : HCPolySupport.Vec d → ℝ} (hphi : HCPolySupport.IsProbeR phi) (hphiSupport : Function.support phi ⊆ U) : Measurable fun (omega : CutoffSample d) => HCPolySupport.entryTestR i j phi (cutoff m omega)

Every supported integral observation of the genuine lower-infinite cutoff is measurable from the completed lower-shell local sigma-field.

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

The genuine cutoff is measurable into CoarseGraining's integral-local sigma-field from the completed lower-shell information. This is the local observable A needed for the eventual range proof; it is not a pointwise restriction claim.