ProbabilityTheory.iCondIndepFun.condIndepFun_finset
theorem ProbabilityTheory.iCondIndepFun.condIndepFun_finset :
∀ {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
[inst_1 : Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsFiniteMeasure μ]
{β : ι → Type u_6} {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i} (S T : Finset ι),
Disjoint S T →
ProbabilityTheory.iCondIndepFun m' hm' m f μ →
(∀ (i : ι), Measurable (f i)) →
ProbabilityTheory.CondIndepFun m' hm' (fun a i => f (↑i) a) (fun a i => f (↑i) a) μ
The theorem `ProbabilityTheory.iCondIndepFun.condIndepFun_finset` states that if `f` is a family of mutually conditionally independent random variables, and `S` and `T` are two disjoint finite index sets, then the tuple formed by `f i` for `i` in `S` is conditionally independent of the tuple `(f i)_i` for `i` in `T`. This is under the assumption that every `f i` is measurable. The notation `ProbabilityTheory.iCondIndepFun m' hm' m f μ` refers to the condition that `f` is a family of mutually conditionally independent random variables, and `ProbabilityTheory.CondIndepFun m' hm' (fun a i => f (↑i) a) (fun a i => f (↑i) a) μ` denotes the condition that the tuples are conditionally independent.
More concisely: If `f` is a family of mutually conditionally independent random variables and `S` and `T` are disjoint finite index sets, then the sub-vectors `(f i)_i for i in S` and `(f i)_i for i in T` are conditionally independent given the index set.
|
ProbabilityTheory.iCondIndepSets.iCondIndep
theorem ProbabilityTheory.iCondIndepSets.iCondIndep :
∀ {Ω : Type u_1} {ι : Type u_2} {m' : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
[inst_1 : Nonempty Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [inst_2 : MeasureTheory.IsFiniteMeasure μ]
(m : ι → MeasurableSpace Ω),
(∀ (i : ι), m i ≤ mΩ) →
∀ (π : ι → Set (Set Ω)),
(∀ (n : ι), IsPiSystem (π n)) →
(∀ (i : ι), m i = MeasurableSpace.generateFrom (π i)) →
ProbabilityTheory.iCondIndepSets m' hm' π μ → ProbabilityTheory.iCondIndep m' hm' m μ
This theorem states that the σ-algebras generated by conditionally independent pi-systems are themselves conditionally independent. In the context of probability theory, given a measurable space `Ω`, an index type `ι`, a measure `μ` on `Ω`, and a function `m` from `ι` to the measurable spaces of `Ω` such that for all `i` in `ι`, `m i` is a sub-measurable space of `Ω`. Also given is a function `π` mapping each `i` from `ι` to a set of subsets of `Ω` which forms a pi-system. If for each `i` in `ι`, the measurable space `m i` is generated from the pi-system `π i`, and these pi-systems are conditionally independent, then the σ-algebras generated by these pi-systems are also conditionally independent.
More concisely: If for each index `i`, the sub-σ-algebras of a measurable space generated by conditionally independent pi-systems on measurable spaces `m i` are equal to the pi-systems `π i`, then the generated σ-algebras are conditionally independent.
|