theorem
ProbabilityTheory.iIndepFun.reindex_of_injective
{Ω : Type u_10}
{ι : Type u_11}
{ι' : Type u_12}
[MeasurableSpace Ω]
{α : ι → Type u_13}
[n : (i : ι) → MeasurableSpace (α i)]
{f : (i : ι) → Ω → α i}
{μ : MeasureTheory.Measure Ω}
(h : ProbabilityTheory.iIndepFun n f μ)
(g : ι' → ι)
(hg : Function.Injective g)
:
ProbabilityTheory.iIndepFun ((fun {x : ι'} => n) ∘' g) ((fun {x : ι'} => f) ∘' g) μ
theorem
ProbabilityTheory.iIndepFun.reindex
{Ω : Type u_10}
{ι : Type u_11}
{ι' : Type u_12}
[MeasurableSpace Ω]
{α : ι → Type u_13}
[n : (i : ι) → MeasurableSpace (α i)]
{f : (i : ι) → Ω → α i}
{μ : MeasureTheory.Measure Ω}
(g : ι' ≃ ι)
(h : ProbabilityTheory.iIndepFun ((fun {x : ι'} => n) ∘' ⇑g) ((fun {x : ι'} => f) ∘' ⇑g) μ)
:
theorem
ProbabilityTheory.iIndepFun.reindex_symm
{Ω : Type u_10}
{ι : Type u_11}
{ι' : Type u_12}
[MeasurableSpace Ω]
{α : ι → Type u_13}
[n : (i : ι) → MeasurableSpace (α i)]
{f : (i : ι) → Ω → α i}
{μ : MeasureTheory.Measure Ω}
(g : ι' ≃ ι)
(h : ProbabilityTheory.iIndepFun n f μ)
:
ProbabilityTheory.iIndepFun ((fun {x : ι'} => n) ∘' ⇑g) ((fun {x : ι'} => f) ∘' ⇑g) μ
theorem
ProbabilityTheory.iIndepFun_reindex_iff
{Ω : Type u_10}
{ι : Type u_11}
{ι' : Type u_12}
[MeasurableSpace Ω]
{α : ι → Type u_13}
[n : (i : ι) → MeasurableSpace (α i)]
{f : (i : ι) → Ω → α i}
{μ : MeasureTheory.Measure Ω}
(g : ι' ≃ ι)
:
ProbabilityTheory.iIndepFun ((fun {x : ι'} => n) ∘' ⇑g) ((fun {x : ι'} => f) ∘' ⇑g) μ ↔ ProbabilityTheory.iIndepFun n f μ
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 : ProbabilityTheory.iIndepFun n f μ)
:
ProbabilityTheory.iIndepFun n (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 : ProbabilityTheory.iIndepFun n f μ)
:
ProbabilityTheory.iIndepFun n (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 : ProbabilityTheory.iIndepFun m f μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
:
ProbabilityTheory.iIndepFun (fun (x : J) => MeasurableSpace.pi)
(fun (j : J) (a : Ω) (i : { x : ι // x ∈ S j }) => f (↑i) a) μ
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 : ProbabilityTheory.iIndepFun m 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))
:
ProbabilityTheory.iIndepFun mγ (fun (j : J) (a : Ω) => φ j fun (i : { x : ι // x ∈ S j }) => f (↑i) a) μ
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.
theorem
ProbabilityTheory.IndepFun.measureReal_inter_preimage_eq_mul
{Ω : Type u_1}
{β : Type u_10}
{β' : Type u_11}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{f : Ω → β}
{g : Ω → β'}
{_mβ : MeasurableSpace β}
{_mβ' : MeasurableSpace β'}
(h : ProbabilityTheory.IndepFun f g μ)
{s : Set β}
{t : Set β'}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
@[simp]
theorem
ProbabilityTheory.indepFun_zero_measure
{Ω : Type u_1}
{β : Type u_6}
{mΩ : MeasurableSpace Ω}
{α : Type u_11}
[MeasurableSpace α]
[MeasurableSpace β]
{f : Ω → α}
{g : Ω → β}
:
theorem
ProbabilityTheory.indepFun_const
{Ω : Type u_1}
{β : Type u_6}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{f : Ω → β}
{α : Type u_11}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasureTheory.IsZeroOrProbabilityMeasure μ]
(c : α)
:
ProbabilityTheory.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 μ']
:
ProbabilityTheory.IndepFun Prod.fst Prod.snd (μ.prod μ')
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 : ProbabilityTheory.IndepFun f g μ)
:
ProbabilityTheory.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 Ω)
:
ProbabilityTheory.iIndepFun m f μ ↔ ∀ (s : Finset ι) ⦃f' : ι → Set Ω⦄, (∀ (i : ι), MeasurableSet (f' i)) → μ (⋂ i ∈ s, f' i) = ∏ i ∈ s, μ (f' i)
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 μ)
:
ProbabilityTheory.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))
:
ProbabilityTheory.iIndepFun m 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)]
:
Measurable Sigma.curry
theorem
Finset.prod_univ_prod
{ι : Type u_1}
{κ : ι → Type u_3}
[Fintype ι]
[(i : ι) → Fintype (κ i)]
{β : Type u_5}
[CommMonoid β]
(f : (i : ι) → κ i → β)
:
∏ ij : (i : ι) × κ i, f ij.fst ij.snd = ∏ i : ι, ∏ j : κ i, f i j
theorem
Finset.sum_univ_sum
{ι : Type u_1}
{κ : ι → Type u_3}
[Fintype ι]
[(i : ι) → Fintype (κ i)]
{β : Type u_5}
[AddCommMonoid β]
(f : (i : ι) → κ i → β)
:
∑ ij : (i : ι) × κ i, f ij.fst ij.snd = ∑ i : ι, ∑ j : κ i, f i j
theorem
Finset.prod_univ_prod'
{ι : Type u_1}
{κ : ι → Type u_3}
[Fintype ι]
[(i : ι) → Fintype (κ i)]
{β : Type u_5}
[CommMonoid β]
(f : (i : ι) × κ i → β)
:
∏ ij : (i : ι) × κ i, f ij = ∏ i : ι, ∏ j : κ i, f ⟨i, j⟩
theorem
Finset.sum_univ_sum'
{ι : Type u_1}
{κ : ι → Type u_3}
[Fintype ι]
[(i : ι) → Fintype (κ i)]
{β : Type u_5}
[AddCommMonoid β]
(f : (i : ι) × κ i → β)
:
∑ ij : (i : ι) × κ i, f ij = ∑ i : ι, ∑ j : κ i, f ⟨i, j⟩
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 :
ProbabilityTheory.iIndepFun (fun (ij : (i : ι) × κ i) => m ij.fst ij.snd)
(fun (ij : (i : ι) × κ i) => f ij.fst ij.snd) μ)
:
ProbabilityTheory.iIndepFun (fun (x : ι) => MeasurableSpace.pi) (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 : ProbabilityTheory.iIndepFun (fun (ij : (i : ι) × κ i) => m ij.fst ij.snd) f μ)
:
ProbabilityTheory.iIndepFun (fun (_i : ι) => MeasurableSpace.pi) (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 (Disjoint on ST))
(h : ProbabilityTheory.iIndepFun n f μ)
:
let β := fun (k : ι') => (i : { x : ι // x ∈ ST k }) → α ↑i;
ProbabilityTheory.iIndepFun (fun (x : ι') => MeasurableSpace.pi)
(fun (k : ι') (x : Ω) (i : { x : ι // x ∈ ST k }) => f (↑i) x) μ
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 : ProbabilityTheory.iIndepFun m f μ)
(hfg : ∀ (i : ι), f i =ᵐ[μ] g i)
:
TODO: a kernel version of this theorem