theorem
ProbabilityTheory.iIndepFun.inv
{Ω : Type u_10}
{ι : Type u_11}
[MeasurableSpace Ω]
{α : ι → Type u_13}
[n : (i : ι) → MeasurableSpace (α i)]
{f : (i : ι) → Ω → α i}
{μ : MeasureTheory.Measure Ω}
(i : ι)
[Inv (α i)]
[MeasurableInv (α i)]
[DecidableEq ι]
(h : iIndepFun f μ)
:
iIndepFun (Function.update f i (f i)⁻¹) μ
theorem
ProbabilityTheory.iIndepFun.neg
{Ω : Type u_10}
{ι : Type u_11}
[MeasurableSpace Ω]
{α : ι → Type u_13}
[n : (i : ι) → MeasurableSpace (α i)]
{f : (i : ι) → Ω → α i}
{μ : MeasureTheory.Measure Ω}
(i : ι)
[Neg (α i)]
[MeasurableNeg (α i)]
[DecidableEq ι]
(h : iIndepFun f μ)
:
iIndepFun (Function.update f i (-f i)) μ
theorem
ProbabilityTheory.iIndepFun.finsets
{Ω : Type u_10}
{ι : Type u_11}
[MeasurableSpace Ω]
{β : ι → Type u_14}
[m : (i : ι) → MeasurableSpace (β i)]
{μ : MeasureTheory.Measure Ω}
{f : (i : ι) → Ω → β i}
{J : Type u_15}
[Fintype J]
(S : J → Finset ι)
(h_disjoint : Set.univ.PairwiseDisjoint S)
(hf_Indep : iIndepFun f μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
:
If f is a family of mutually independent random variables, (S j)ⱼ are pairwise disjoint
finite index sets, then the tuples formed by f i for i ∈ S j are mutually independent,
when seen as a family indexed by J.
theorem
ProbabilityTheory.iIndepFun.finsets_comp
{Ω : Type u_10}
{ι : Type u_11}
[MeasurableSpace Ω]
{β : ι → Type u_14}
[m : (i : ι) → MeasurableSpace (β i)]
{μ : MeasureTheory.Measure Ω}
{f : (i : ι) → Ω → β i}
{J : Type u_15}
[Fintype J]
(S : J → Finset ι)
(h_disjoint : Set.univ.PairwiseDisjoint S)
(hf_Indep : iIndepFun f μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
{γ : J → Type u_16}
{mγ : (j : J) → MeasurableSpace (γ j)}
(φ : (j : J) → ((i : { x : ι // x ∈ S j }) → β ↑i) → γ j)
(hφ : ∀ (j : J), Measurable (φ j))
:
If f is a family of mutually independent random variables, (S j)ⱼ are pairwise disjoint
finite index sets, and φ j is a function that maps the tuple formed by f i for i ∈ S j to a
measurable space γ j, then the family of random variables formed by φ j (f i)_{i ∈ S j} and
indexed by J is iIndep.
@[simp]
theorem
ProbabilityTheory.indepFun_zero_measure
{Ω : Type u_1}
{β : Type u_6}
{mΩ : MeasurableSpace Ω}
{α : Type u_11}
[MeasurableSpace α]
[MeasurableSpace β]
{f : Ω → α}
{g : Ω → β}
:
IndepFun f g 0
theorem
ProbabilityTheory.indepFun_const
{Ω : Type u_1}
{β : Type u_6}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{f : Ω → β}
{α : Type u_11}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(c : α)
:
IndepFun f (fun (x : Ω) => c) μ
Random variables are always independent of constants.
theorem
ProbabilityTheory.indepFun_fst_snd
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{Ω' : Type u_10}
[MeasurableSpace Ω']
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
{μ' : MeasureTheory.Measure Ω'}
[MeasureTheory.IsZeroOrProbabilityMeasure μ']
:
theorem
ProbabilityTheory.IndepFun.comp_right
{Ω : Type u_1}
{β : Type u_6}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{Ω' : Type u_10}
{α : Type u_11}
[MeasurableSpace Ω']
[MeasurableSpace α]
[MeasurableSpace β]
{f : Ω → α}
{g : Ω → β}
{i : Ω' → Ω}
(hi : MeasurableEmbedding i)
(hi' : ∀ᵐ (a : Ω) ∂μ, a ∈ Set.range i)
(hf : Measurable f)
(hg : Measurable g)
(hfg : IndepFun f g μ)
:
IndepFun (f ∘ i) (g ∘ i) (MeasureTheory.Measure.comap i μ)
Composing independent functions with a measurable embedding of conull range gives independent functions.
theorem
ProbabilityTheory.iIndepFun_iff'
{Ω : Type u_1}
{ι : Type u_2}
[MeasurableSpace Ω]
{β : ι → Type u_12}
(m : (i : ι) → MeasurableSpace (β i))
(f : (i : ι) → Ω → β i)
(μ : MeasureTheory.Measure Ω)
:
theorem
ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map'
{Ω : Type u_1}
{β' : Type u_7}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{β : Type u_12}
{mβ : MeasurableSpace β}
{mβ' : MeasurableSpace β'}
{f : Ω → β}
{g : Ω → β'}
[MeasureTheory.IsFiniteMeasure μ]
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
:
IndepFun f g μ ↔ MeasureTheory.Measure.map (fun (ω : Ω) => (f ω, g ω)) μ = (MeasureTheory.Measure.map f μ).prod (MeasureTheory.Measure.map g μ)
theorem
ProbabilityTheory.iIndepFun_iff_pi_map_eq_map
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{ι : Type u_12}
{β : ι → Type u_13}
[Fintype ι]
(f : (x : ι) → Ω → β x)
[m : (x : ι) → MeasurableSpace (β x)]
[MeasureTheory.IsProbabilityMeasure μ]
(hf : ∀ (x : ι), Measurable (f x))
:
iIndepFun f μ ↔ (MeasureTheory.Measure.pi fun (i : ι) => MeasureTheory.Measure.map (f i) μ) = MeasureTheory.Measure.map (fun (ω : Ω) (i : ι) => f i ω) μ
theorem
ProbabilityTheory.measurable_sigmaCurry
{ι : Type u_1}
{κ : ι → Type u_3}
{α : (i : ι) → κ i → Type u_4}
[m : (i : ι) → (j : κ i) → MeasurableSpace (α i j)]
:
theorem
Finset.prod_univ_prod'
{ι : Type u_1}
{κ : ι → Type u_3}
[Fintype ι]
[(i : ι) → Fintype (κ i)]
{β : Type u_5}
[CommMonoid β]
(f : (i : ι) × κ i → β)
:
theorem
Finset.sum_univ_sum'
{ι : Type u_1}
{κ : ι → Type u_3}
[Fintype ι]
[(i : ι) → Fintype (κ i)]
{β : Type u_5}
[AddCommMonoid β]
(f : (i : ι) × κ i → β)
:
theorem
ProbabilityTheory.iIndepFun.pi
{Ω : Type u_2}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{ι : Type u_5}
{κ : ι → Type u_6}
[(i : ι) → Fintype (κ i)]
{α : (i : ι) → κ i → Type u_7}
{f : (i : ι) → (j : κ i) → Ω → α i j}
[m : (i : ι) → (j : κ i) → MeasurableSpace (α i j)]
(f_meas : ∀ (i : ι) (j : κ i), Measurable (f i j))
(hf : iIndepFun (fun (ij : (i : ι) × κ i) => f ij.fst ij.snd) μ)
:
iIndepFun (fun (i : ι) (ω : Ω) (j : κ i) => f i j ω) μ
If a family of functions (i, j) ↦ f i j is independent, then the family of function tuples
i ↦ (f i j)ⱼ is independent.
theorem
ProbabilityTheory.iIndepFun.pi'
{Ω : Type u_2}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{ι : Type u_5}
{κ : ι → Type u_6}
[(i : ι) → Fintype (κ i)]
{α : (i : ι) → κ i → Type u_7}
[m : (i : ι) → (j : κ i) → MeasurableSpace (α i j)]
{f : (ij : (i : ι) × κ i) → Ω → α ij.fst ij.snd}
(f_meas : ∀ (i : (i : ι) × κ i), Measurable (f i))
(hf : iIndepFun f μ)
:
iIndepFun (fun (i : ι) (ω : Ω) (j : κ i) => f ⟨i, j⟩ ω) μ
If a family of functions (i, j) ↦ f i j is independent, then the family of function tuples
i ↦ (f i j)ⱼ is independent.
theorem
ProbabilityTheory.iIndepFun.prod
{Ω : Type u_2}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{ι : Type u_8}
{ι' : Type u_9}
{α : ι → Type u_10}
{n : (i : ι) → MeasurableSpace (α i)}
{f : (i : ι) → Ω → α i}
{hf : ∀ (i : ι), Measurable (f i)}
{ST : ι' → Finset ι}
(hS : Pairwise (Function.onFun Disjoint ST))
(h : iIndepFun f μ)
:
theorem
ProbabilityTheory.iIndepFun.ae_eq
{Ω : Type u_13}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{ι : Type u_14}
{β : ι → Type u_15}
{m : (i : ι) → MeasurableSpace (β i)}
{f g : (i : ι) → Ω → β i}
(hf_Indep : iIndepFun f μ)
(hfg : ∀ (i : ι), f i =ᵐ[μ] g i)
:
iIndepFun g μ
TODO: a kernel version of this theorem