LayerIndependence

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

Mutual independence of joins of row-wise independent sigma-fields

This file is carrier-neutral: it works over an abstract probability space and uses nothing but Mathlib's independence A. It supplies the one purely measure-theoretic brick that the varying-truncation-level independence producer of Section 4.1 needs and that Mathlib does not have.

The situation is the following. A doubly indexed family of sub-sigma-fields A : ι → L → MeasurableSpace Ω is given, together with a mutually independent family κ : L → MeasurableSpace Ω dominating it row by row (A i l ≤ κ l). Each row — the family (A i l)_i at a fixed l — is mutually independent. The conclusion needed downstream is that the joins (⨆ l, A i l)_i are mutually independent: one index i may read every l, and the reads at different i must still decouple.

Mathlib's ProbabilityTheory.indep_iSup_of_disjoint splits a mutually independent family into two disjoint blocks; iterating it over a Finset of indices is exactly what turns the refined ι × L-family into the ι-indexed join statement.

Main results

• iIndep_prod_of_iIndep_rows: the ι × L-refinement of a doubly indexed family with independent rows is mutually independent.
• iIndep_iSup_of_iIndep_rows: the ι-indexed joins of row-wise independent families over an independent L-family are mutually independent.
• iIndep_of_le: mutual independence passes to smaller sigma-fields.
• iIndepFun_of_iIndep_sigma: real observables measurable for a mutually independent family of sigma-fields are mutually independent.

theorem Algsuperdiff.Section4.Probability.iIndep_prod_of_iIndep_rows {Omega : Type u_1} [mOmega : MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {iota : Type u_2} {L : Type u_3} {kappa : L → MeasurableSpace Omega} {A : iota → L → MeasurableSpace Omega} (hkappa : ProbabilityTheory.iIndep kappa mu) (hle : ∀ (i : iota) (l : L), A i l ≤ kappa l) (hrow : ∀ (l : L), ProbabilityTheory.iIndep (fun (i : iota) => A i l) mu) : ProbabilityTheory.iIndep (fun (p : iota × L) => A p.1 p.2) mu

The ι × L-refinement of a doubly indexed family is mutually independent. If kappa : L → MeasurableSpace Omega is mutually independent, every A i l is contained in kappa l, and each row (A i l)_i at a fixed l is mutually independent, then the whole family (A p.1 p.2)_{p : ι × L} is mutually independent.

A finite intersection is regrouped by the second (layer) coordinate: the independence of kappa multiplies across distinct layers, and the row independence multiplies inside a single layer.

theorem Algsuperdiff.Section4.Probability.iIndep_iSup_of_iIndep_rows {Omega : Type u_1} [mOmega : MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {iota : Type u_2} {L : Type u_3} {kappa : L → MeasurableSpace Omega} {A : iota → L → MeasurableSpace Omega} (hkappa : ProbabilityTheory.iIndep kappa mu) (hkappale : ∀ (l : L), kappa l ≤ mOmega) (hle : ∀ (i : iota) (l : L), A i l ≤ kappa l) (hrow : ∀ (l : L), ProbabilityTheory.iIndep (fun (i : iota) => A i l) mu) : ProbabilityTheory.iIndep (fun (i : iota) => ⨆ (l : L), A i l) mu

The ι-indexed join of row-wise independent families is mutually independent. Let kappa : L → MeasurableSpace Omega be mutually independent with every kappa l a sub-sigma-field of the ambient one, and let A : ι → L → MeasurableSpace Omega satisfy A i l ≤ kappa l with every row mutually independent. Then the joins (⨆ l, A i l)_i are mutually independent.

Proof: iIndep_prod_of_iIndep_rows gives mutual independence of the refined ι × L-family; the ι-blocks {p | p.1 = i} are pairwise disjoint, so Mathlib's indep_iSup_of_disjoint splits off one block at a time along a Finset induction.

theorem Algsuperdiff.Section4.Probability.iIndep_of_le {Omega : Type u_1} [mOmega : MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {iota : Type u_2} {m m' : iota → MeasurableSpace Omega} (h : ProbabilityTheory.iIndep m mu) (hle : ∀ (i : iota), m' i ≤ m i) : ProbabilityTheory.iIndep m' mu

Mutual independence is inherited by any pointwise smaller family of sigma-fields.

theorem Algsuperdiff.Section4.Probability.iIndepFun_of_iIndep_sigma {Omega : Type u_1} [mOmega : MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {iota : Type u_2} {m : iota → MeasurableSpace Omega} (h : ProbabilityTheory.iIndep m mu) {f : iota → Omega → ℝ} (hf : ∀ (i : iota), Measurable (f i)) : ProbabilityTheory.iIndepFun f mu

Real observables measurable for a mutually independent family of sigma-fields are mutually independent. The comap sigma-field of f i is contained in m i, so the mutual independence of the m i passes to the functions.