IndexSigma

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

Sigma-fields generated by indexed coordinates

This file defines the sigma-field generated by coordinates in an index set and records its elementary measurability and independence A.

Main definitions

• indexSigma: the sigma-field generated by a chosen set of coordinates.

Main results

• measurable_coordinate_of_mem: a selected coordinate is measurable with respect to its index sigma-field.
• indep_indexSigma_of_disjoint: mutually independent measurable coordinates generate independent sigma-fields on disjoint index sets.

@[reducible, inline]

abbrev Algsuperdiff.Probability.indexSigma {ι : Type u_1} {Ω : Type u_2} {β : Type u_3} [MeasurableSpace β] (coordinates : Ω → ι → β) (I : Set ι) : MeasurableSpace Ω

The sigma-field on Ω generated by the coordinates of coordinates whose indices belong to I.

Equations

• Algsuperdiff.Probability.indexSigma coordinates I = ⨆ i ∈ I, MeasurableSpace.comap (fun (ω : Ω) => coordinates ω i) inferInstance

theorem Algsuperdiff.Probability.comap_coordinate_le_indexSigma {ι : Type u_1} {Ω : Type u_2} {β : Type u_3} [MeasurableSpace β] (coordinates : Ω → ι → β) {I : Set ι} {i : ι} (hi : i ∈ I) : MeasurableSpace.comap (fun (ω : Ω) => coordinates ω i) inferInstance ≤ indexSigma coordinates I

The sigma-field generated by one coordinate is contained in the sigma-field generated by every index set containing that coordinate.

theorem Algsuperdiff.Probability.measurable_coordinate_of_mem {ι : Type u_1} {Ω : Type u_2} {β : Type u_3} [MeasurableSpace β] (coordinates : Ω → ι → β) {I : Set ι} {i : ι} (hi : i ∈ I) : Measurable fun (ω : Ω) => coordinates ω i

Coordinates indexed by I are measurable with respect to indexSigma coordinates I.

theorem Algsuperdiff.Probability.indep_indexSigma_of_disjoint {ι : Type u_1} {Ω : Type u_2} {β : Type u_3} [MeasurableSpace β] [MeasurableSpace Ω] (coordinates : Ω → ι → β) (μ : MeasureTheory.Measure Ω) (h_measurable : ∀ (i : ι), Measurable fun (ω : Ω) => coordinates ω i) (h_indep : ProbabilityTheory.iIndepFun (fun (i : ι) (ω : Ω) => coordinates ω i) μ) {I J : Set ι} (hIJ : Disjoint I J) : ProbabilityTheory.Indep (indexSigma coordinates I) (indexSigma coordinates J) μ

Mutually independent measurable coordinates generate independent sigma-fields on disjoint index sets.