ShellIndependence

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

Cross-shell independence in consumable sigma-field form

ABK26 fixes a sequence {..., j_{-1}, j_0, j_1, ...} of independent antisymmetric matrix-valued random fields. That standing assumption is already carried verbatim by the frozen model surface, as the field Algsuperdiff.Frozen.Assumptions.ShellLawPrefix.independent, namely iIndepFun (fun k : ℤ => fun F => F k) P.toMeasure.

Every downstream consumer of that assumption, however, needs it in a block form: the information carried by one set of shell indices is independent of the information carried by a disjoint set of shell indices. This file provides exactly that translation and nothing more. It introduces no new assumption: each result below is a consequence of ShellLawPrefix.independent together with the purely measure-theoretic engine Algsuperdiff.Probability.indep_indexSigma_of_disjoint.

The distinction with the spatial range-dependence facts is deliberate. The declarations Cutoff.indep_shellLocal_of_cutoff_separation and Cutoff.indep_lowerShellLocalSigma_of_cutoff_separation are consequences of the within-shell finite range of dependence (J1) at a spatial separation; they are not the cross-shell assumption of ABK26 and must never be cited for it. The results in this file are the converse: they never use (J1), only shellPrefix.independent.

Main definitions

• shellIndexSigma: the sigma-field generated by the shells indexed by I.

Main results

• indep_shellIndexSigma_of_disjoint: shells with disjoint index sets generate independent sigma-fields.
• indepFun_of_measurable_shellIndexSigma_of_disjoint: the random-variable form.
• lowerShellLocalSigma_le_shellIndexSigma_Iic: the genuine lower cutoff reads only shells at or below its own index, so it is independent of every fresh block above that index.

The sigma-field of a set of shell indices

@[reducible, inline]

noncomputable abbrev Algsuperdiff.Section3.Cutoff.shellIndexSigma {d : ℕ} (I : Set ℤ) : MeasurableSpace (ShellSeq d)

The sigma-field on the canonical shell-sequence carrier generated by the shells whose index lies in I.

Equations

• Algsuperdiff.Section3.Cutoff.shellIndexSigma I = Algsuperdiff.Probability.indexSigma (fun (omega : Algsuperdiff.Section3.Cutoff.ShellSeq d) => omega) I

theorem Algsuperdiff.Section3.Cutoff.measurable_shellCoordinate_shellIndexSigma {d : ℕ} {I : Set ℤ} {k : ℤ} (hk : k ∈ I) : Measurable fun (omega : ShellSeq d) => omega k

One selected shell is measurable for the sigma-field of any index set containing it.

theorem Algsuperdiff.Section3.Cutoff.shellIndexSigma_le_borel {d : ℕ} (I : Set ℤ) : shellIndexSigma I ≤ inferInstance

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

The line-437 assumption in block form

theorem Algsuperdiff.Section3.Cutoff.indep_shellIndexSigma_of_disjoint {d : ℕ} (M : ABKModel d) {I J : Set ℤ} (hIJ : Disjoint I J) : ProbabilityTheory.Indep (shellIndexSigma I) (shellIndexSigma J) ↑M.P

Cross-shell independence, block form. Shells indexed by disjoint sets generate independent sigma-fields. This is ABK26 and nothing else: the only input is ShellLawPrefix.independent.

theorem Algsuperdiff.Section3.Cutoff.indepFun_of_measurable_shellIndexSigma_of_disjoint {d : ℕ} (M : ABKModel d) {I J : Set ℤ} (hIJ : Disjoint I J) {alpha : Type u_1} {beta : Type u_2} [MeasurableSpace alpha] [MeasurableSpace beta] {X : ShellSeq d → alpha} {Y : ShellSeq d → beta} (hX : Measurable X) (hY : Measurable Y) : ProbabilityTheory.IndepFun X Y ↑M.P

Random-variable form. Any two observables measurable for disjoint shell blocks are independent.

Locating the cutoff and the fresh increment in the shell blocks

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

The genuine lower cutoff at index m reads only shells at or below m.

Null-completion of one side

theorem Algsuperdiff.Section3.Cutoff.indep_lowerShellLocalCompletion_shellIndexSigma_of_disjoint {d : ℕ} (M : ABKModel d) {L : ℤ} {J : Set ℤ} (hJ : Disjoint (Set.Iic L) J) (U : Set (HCPolySupport.Vec d)) : ProbabilityTheory.Indep (lowerShellLocalCompletion M L U) (shellIndexSigma J) ↑M.P

Independence against a fresh block survives null completion. The genuine infinite cutoff is measurable only for the null completion of the lower-shell local sigma-field, so this is the form in which the cutoff can be declared independent of a disjointly indexed shell block.

theorem Algsuperdiff.Section3.Cutoff.indep_lowerShellLocalCompletion_shellIndexSigma_Ioc {d : ℕ} (M : ABKModel d) {L n m : ℤ} (hLn : L ≤ n) (U : Set (HCPolySupport.Vec d)) : ProbabilityTheory.Indep (lowerShellLocalCompletion M L U) (shellIndexSigma (Set.Ioc n m)) ↑M.P

The genuine (null-completed) lower cutoff at index L is independent of every fresh block (n, m] lying strictly above L.