Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.Proportion.ShellColumnIndep

ShellColumnIndep #

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

Columns that read a single shell are independent, for every dependence range #

p.concentration.for.scales consumes the hypothesis e.independent.columns.twosided: for some r ∈ ℕ, the columns of the Appendix-D array, taken along any residue class modulo r, are mutually independent as ℤ → ℝ-valued random variables.

So ColumnsIndep holds for every r ≥ 1, with no separation geometry — in contrast to the 𝒢₀/𝒢₂ lanes, whose columns read overlapping truncations and therefore need the annulus separation.

Carrier transfer #

(J1) is stated on Cutoff.ShellSeq d under M.P; the arrays live on Cutoff.CutoffSample d under Cutoff.cutoffSampleLaw. Independence descends because Subtype.val is a measurable embedding preserving the mass of every subset (measure_preimage_val_cutoffSampleLaw), so no null-set bookkeeping and no measurability side condition is needed.

References #

1. Mutual independence of arbitrary-valued observables #

source
theorem Algsuperdiff.Section4.Provider.Proportion.iIndepFun_of_iIndep_sigma_pi {Omega : Type u_1} {iota : Type u_2} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {m : iota → MeasurableSpace Omega} (h : ProbabilityTheory.iIndep m mu) {beta : iota → Type u_3} [mbeta : (i : iota) → MeasurableSpace (beta i)] {f : (i : iota) → Omega → beta i} (hf : ∀ (i : iota), Measurable (f i)) :
ProbabilityTheory.iIndepFun f mu

The arbitrary-codomain form of Algsuperdiff.Section4.Probability.iIndepFun_of_iIndep_sigma. The 𝒢₁ columns are ℤ → ℝ-valued (a whole column at a time), so the real-valued form proved in LayerIndependence does not apply directly.

2. Independence descends to the cutoff carrier #

source
theorem Algsuperdiff.Section4.Provider.Proportion.iIndepFun_comp_val_cutoffSampleLaw {d : ℕ} (M : Section3.ABKModel d) {iota : Type u_1} {beta : iota → Type u_2} [(i : iota) → MeasurableSpace (beta i)] {f : (i : iota) → Section3.Cutoff.ShellSeq d → beta i} (h : ProbabilityTheory.iIndepFun f ↑M.P) :
ProbabilityTheory.iIndepFun (fun (i : iota) (omega : Section3.Cutoff.CutoffSample d) => f i ↑omega) ↑(Section3.Cutoff.cutoffSampleLaw M)

Mutual independence transfers along the cutoff inclusion. The inclusion Subtype.val : CutoffSample d → ShellSeq d preserves the mass of every subset, so the product formula for the generated sigma-fields is preserved verbatim; no measurability of the observables and no null-set enlargement enter.

3. The single-shell sigma-fields of a cutoff sample #

source
@[reducible, inline]
noncomputable abbrev Algsuperdiff.Section4.Provider.Proportion.shellSigma (d : ℕ) (k : ℤ) :
MeasurableSpace (Section3.Cutoff.CutoffSample d)

The sigma-field generated by reading the single shell k of a cutoff sample. Every 𝒢₁ column is measurable for exactly one of these.

Equations
Instances For
    source
    theorem Algsuperdiff.Section4.Provider.Proportion.measurable_shellSigma_coord {d : ℕ} (k : ℤ) :
    Measurable fun (omega : Section3.Cutoff.CutoffSample d) => ↑omega k
    source
    theorem Algsuperdiff.Section4.Provider.Proportion.shellSigma_le {d : ℕ} (k : ℤ) :
    shellSigma d k ≤ inferInstance
    source
    theorem Algsuperdiff.Section4.Provider.Proportion.measurable_shellSigma_comp {d : ℕ} {beta : Type u_1} [MeasurableSpace beta] (k : ℤ) {F : Frozen.Assumptions.ShellField d → beta} (hF : Measurable F) :
    Measurable fun (omega : Section3.Cutoff.CutoffSample d) => F (↑omega k)

    Any measurable functional of the single shell k is shellSigma d k measurable.

    source
    theorem Algsuperdiff.Section4.Provider.Proportion.iIndep_shellSigma {d : ℕ} (M : Section3.ABKModel d) :
    ProbabilityTheory.iIndep (shellSigma d) ↑(Section3.Cutoff.cutoffSampleLaw M)

    (J1) on the cutoff carrier. The single-shell sigma-fields are mutually independent under cutoffSampleLaw.

    4. The ColumnsIndep producer at the two-index shape #

    source
    theorem Algsuperdiff.Section4.Provider.Proportion.columnsIndep_of_shellColumn {d : ℕ} (M : Section3.ABKModel d) (X : ℤ → ℤ → Section3.Cutoff.CutoffSample d → ℝ) {r : ℕ} (hr : 1 ≤ r) (hcol : ∀ (m j : ℤ), Measurable (X m j)) :
    Probability.ScalesConcentration.ColumnsIndep (↑(Section3.Cutoff.cutoffSampleLaw M)) X r

    The 𝒢₁ independence hypothesis, discharged at every r ≥ 1. If every entry X m j of a two-index array is a functional of the single shell j, then the array's columns are r-dependent for every r ≥ 1.