Independence of disjoint coordinate restrictions of an infinite product

The restrictions of a product sample to disjoint index sets are independent, and so are its selections along maps with disjoint ranges. The resulting joint-law identities are useful when a conditionally independent process is split into observed and unobserved coordinates.

When one of two factors has no atoms, the two corresponding coordinates of a product sample are moreover almost surely different, so a sample can be used to order the indices it is attached to.

theorem TauCeti.Probability.indepFun_domRestrict_infinitePi {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] (P : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (P i)] {S T : Set ι} (hST : Disjoint S T) : ProbabilityTheory.IndepFun (fun (x : (i : ι) → α i) => S.domRestrict x) (fun (x : (i : ι) → α i) => T.domRestrict x) (MeasureTheory.Measure.infinitePi P)

Restrictions to disjoint coordinate sets are independent under a product probability law.

@[simp]

theorem TauCeti.Probability.infinitePi_map_pair_domRestrict {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] (P : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (P i)] {S T : Set ι} (hST : Disjoint S T) : MeasureTheory.Measure.map (fun (x : (a : ι) → α a) => (S.domRestrict x, T.domRestrict x)) (MeasureTheory.Measure.infinitePi P) = (MeasureTheory.Measure.infinitePi fun (i : ↑S) => P ↑i).prod (MeasureTheory.Measure.infinitePi fun (i : ↑T) => P ↑i)

Under a product probability law, the restrictions to two disjoint sets of coordinates have the product of their marginal laws.

theorem TauCeti.Probability.infinitePi_map_pair_comp {ι : Type u_3} {κ₁ : Type u_4} {κ₂ : Type u_5} {β : Type u_6} [MeasurableSpace β] (P : ι → MeasureTheory.Measure β) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (P i)] {e : κ₁ → ι} {g : κ₂ → ι} (hg : Function.Injective g) (heg : Disjoint (Set.range e) (Set.range g)) : MeasureTheory.Measure.map (fun (x : ι → β) => (fun (a : κ₁) => x (e a), fun (b : κ₂) => x (g b))) (MeasureTheory.Measure.infinitePi P) = (MeasureTheory.Measure.map (fun (x : ι → β) (a : κ₁) => x (e a)) (MeasureTheory.Measure.infinitePi P)).prod (MeasureTheory.Measure.infinitePi fun (b : κ₂) => P (g b))

Under a product law, selections along maps with disjoint ranges are independent, and an injective selection has the product of the selected factors as its law. The first selection need not be injective.

theorem TauCeti.Probability.ae_eval_ne_eval_infinitePi {ι : Type u_3} {β : Type u_4} [MeasurableSpace β] [MeasurableEq β] (P : ι → MeasureTheory.Measure β) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (P i)] {i j : ι} [MeasureTheory.NullSingletonClass (P j)] (hij : i ≠ j) : ∀ᵐ (x : ι → β) ∂MeasureTheory.Measure.infinitePi P, x i ≠ x j

Two coordinates of a product are almost surely distinct when one law is atomless. Under a product of probability laws on a space with a measurable diagonal, two distinct coordinates i and j of a sample almost surely take different values as soon as the law at j has no atoms.