Independence from disjoint blocks of an independent family

Mathlib's ProbabilityTheory.iIndepFun.indepFun_finset splits an independent family along two disjoint finite index sets. The statement is true for arbitrary index sets, and that is what a random object built from a countably infinite block of independent noise needs: the two objects are independent as soon as the coordinates they read are disjoint, however many of them there are.

TauCeti.Probability.blockSigma names the σ-algebra a block of coordinates generates, and TauCeti.Probability.indepFun_of_measurable_blockSigma is the resulting independence criterion. The proof is Mathlib's ProbabilityTheory.indep_iSup_of_disjoint together with the monotonicity of independence in both σ-algebras.

Main declarations

• TauCeti.Probability.blockSigma — the σ-algebra generated by a set of members of a family of random variables;
• TauCeti.Probability.blockSigma_def — its defining supremum, for use across module boundaries;
• TauCeti.Probability.blockSigma_empty — an empty block generates the bottom σ-algebra;
• TauCeti.Probability.blockSigma_mono — monotonicity in the block;
• TauCeti.Probability.blockSigma_le_iff — the universal property of that σ-algebra;
• TauCeti.Probability.measurable_blockSigma_of_mem — a member of the block is measurable for it;
• TauCeti.Probability.indepFun_of_measurable_blockSigma — two random elements measurable for the σ-algebras of disjoint blocks of an independent family are independent.

@[implicit_reducible]

def TauCeti.Probability.blockSigma {Ω : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] (Z : (i : ι) → Ω → β i) (S : Set ι) : MeasurableSpace Ω

The σ-algebra generated by the members Z i of a family with i in a block S of indices.

Equations

• TauCeti.Probability.blockSigma Z S = ⨆ i ∈ S, MeasurableSpace.comap (Z i) inferInstance

theorem TauCeti.Probability.blockSigma_def {Ω : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] (Z : (i : ι) → Ω → β i) (S : Set ι) : blockSigma Z S = ⨆ i ∈ S, MeasurableSpace.comap (Z i) inferInstance

The defining supremum of blockSigma.

theorem TauCeti.Probability.blockSigma_eq_comap_restrict {Ω : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] (Z : (i : ι) → Ω → β i) (S : Set ι) : blockSigma Z S = MeasurableSpace.comap (fun (ω : Ω) (i : ↑S) => Z (↑i) ω) inferInstance

The block σ-algebra is the σ-algebra pulled back along the restriction of the family to the block.

theorem TauCeti.Probability.blockSigma_coe_eq_comap_finset_restrict {Ω : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] (Z : (i : ι) → Ω → β i) (S : Finset ι) : blockSigma Z ↑S = MeasurableSpace.comap (fun (ω : Ω) => S.restrict fun (i : ι) => Z i ω) inferInstance

The block σ-algebra of a finite block is the σ-algebra pulled back along the Finset restriction of the family to the block.

@[simp]

theorem TauCeti.Probability.blockSigma_empty {Ω : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] (Z : (i : ι) → Ω → β i) : blockSigma Z ∅ = ⊥

The σ-algebra generated by an empty block is the bottom σ-algebra.

theorem TauCeti.Probability.measurable_blockSigma_of_mem {Ω : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] {Z : (i : ι) → Ω → β i} {S : Set ι} {i : ι} (hi : i ∈ S) : Measurable (Z i)

A member of a block is measurable for the σ-algebra that block generates.

theorem TauCeti.Probability.blockSigma_mono {Ω : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] {Z : (i : ι) → Ω → β i} {S T : Set ι} (hST : S ⊆ T) : blockSigma Z S ≤ blockSigma Z T

The σ-algebra of a block grows with the block.

theorem TauCeti.Probability.blockSigma_le_iff {Ω : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] {Z : (i : ι) → Ω → β i} {S : Set ι} {m : MeasurableSpace Ω} : blockSigma Z S ≤ m ↔ ∀ i ∈ S, Measurable (Z i)

The σ-algebra generated by a block is below m exactly when every member of the block is measurable with respect to m.

theorem TauCeti.Probability.blockSigma_le {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] {Z : (i : ι) → Ω → β i} (S : Set ι) (hZ : ∀ i ∈ S, Measurable (Z i)) : blockSigma Z S ≤ inferInstance

The σ-algebra of a block of an independent family sits inside the ambient σ-algebra.

theorem TauCeti.Probability.indepFun_of_measurable_blockSigma {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {β : ι → Type u_3} [(i : ι) → MeasurableSpace (β i)] {μ : MeasureTheory.Measure Ω} {Z : (i : ι) → Ω → β i} {S T : Set ι} (hZ : ProbabilityTheory.iIndepFun (fun (i : ↑(S ∪ T)) => Z ↑i) μ) (hZ_meas : ∀ i ∈ S ∪ T, Measurable (Z i)) (hST : Disjoint S T) {γ : Type u_4} {δ : Type u_5} [MeasurableSpace γ] [MeasurableSpace δ] {U : Ω → γ} {V : Ω → δ} (hU : Measurable U) (hV : Measurable V) : ProbabilityTheory.IndepFun U V μ

Disjoint blocks of an independent family are independent. Two random elements, each measurable for the σ-algebra generated by its own block of an independent family, are independent as soon as the two blocks are disjoint. Unlike ProbabilityTheory.iIndepFun.indepFun_finset, the blocks may be infinite.