Locality

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

Integral-locality of the lower cutoff

The manuscript's local information F(U) is represented by CoarseGraining's integral-generated LocalSigmaR U, pulled back to a shell by ShellField.lihLocalSigma U. This module makes the corresponding information of all shells at or below m explicit. It also supplies the null-set completion needed when a limiting field is recovered only as an almost-everywhere limit of finite local reads.

The finite lower cutoffs are proved local here. The infinite-cutoff promotion belongs in the next range-law module: it must use both the finite local result and the actual lower-tail convergence theorem, rather than postulating locality for the limiting law.

@[reducible, inline]

abbrev Algsuperdiff.Section3.Cutoff.lowerShellLocalSigma {d : ℕ} (m : ℤ) (U : Set (HCPolySupport.Vec d)) : MeasurableSpace (ShellSeq d)

The source local sigma-field generated by the restrictions to U of every shell at or below m. The shell index is written as m-r with r : ℕ so that it is literally the lower-infinite stream used by the cutoff.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Cutoff.lowerShellLocalSigma_le_borel {d : ℕ} (m : ℤ) (U : Set (HCPolySupport.Vec d)) : lowerShellLocalSigma m U ≤ inferInstance

Every local lower-shell sigma-field is contained in the canonical Borel sigma-field of the shell sequence.

theorem Algsuperdiff.Section3.Cutoff.measurable_lowerShellLocal_coordinate {d : ℕ} (m : ℤ) (U : Set (HCPolySupport.Vec d)) (r : ℕ) : Measurable fun (omega : ShellSeq d) => omega (m - ↑r)

The rth lower shell is measurable from the lower-shell local sigma-field, with its own integral-local measurable structure.

theorem Algsuperdiff.Section3.Cutoff.aeEq_iUnion {d : ℕ} {μ : MeasureTheory.Measure (ShellSeq d)} {s t : ℕ → Set (ShellSeq d)} (h : ∀ (n : ℕ), s n =ᵐ[μ] t n) : ⋃ (n : ℕ), s n =ᵐ[μ] ⋃ (n : ℕ), t n

@[reducible, inline]

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

The completion by ambient null sets of the lower-shell local sigma-field. This is a sigma-field, not a changed cutoff definition: its only role is to make genuine representatives of a.e. local limits measurable.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Cutoff.lowerShellLocalSigma_le_completion {d : ℕ} (M : ABKModel d) (m : ℤ) (U : Set (HCPolySupport.Vec d)) : lowerShellLocalSigma m U ≤ lowerShellLocalCompletion M m U

The completed local sigma-field contains its literal lower-shell source sigma-field.

theorem Algsuperdiff.Section3.Cutoff.measurable_lowerShellLocalCompletion_of_ae_eq_completion {d : ℕ} {M : ABKModel d} {m : ℤ} {U : Set (HCPolySupport.Vec d)} {β : Type u_1} [MeasurableSpace β] {f g : ShellSeq d → β} (hg : Measurable g) (hfg : f =ᵐ[↑M.P] g) : Measurable f

The completion is stable under almost-everywhere replacement.

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

Independence is unchanged when each lower-shell local sigma-field is completed by null sets of the ambient shell law.

theorem Algsuperdiff.Section3.Cutoff.measurable_finiteLowerCutoff_local {d : ℕ} (m : ℤ) (q : ℕ) (U : Set (HCPolySupport.Vec d)) : Measurable (finiteLowerCutoff m q)

Every finite lower cutoff is measurable with respect to the lower-shell integral-local sigma-field. This is the exact finite locality statement that the lower-infinite limit later promotes through convergence; it uses neither a point-value restriction sigma-field nor an added locality hypothesis.