theorem
ProbabilityTheory.IndepFun.measureReal_inter_preimage_eq_mul
{Ω : Type u_1}
{β : Type u_3}
{β' : Type u_4}
{mΩ : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{f : Ω → β}
{g : Ω → β'}
{_mβ : MeasurableSpace β}
{_mβ' : MeasurableSpace β'}
(h : IndepFun f g μ)
{s : Set β}
{t : Set β'}
(hs : MeasurableSet s)
(ht : MeasurableSet t)
:
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))
:
iIndepFun (fun (j : J) (a : Ω) (i : ↥(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 : iIndepFun f μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
{γ : J → Type u_16}
{mγ : (j : J) → MeasurableSpace (γ j)}
(φ : (j : J) → ((i : ↥(S j)) → β ↑i) → γ j)
(hφ : ∀ (j : J), Measurable (φ j))
:
iIndepFun (fun (j : J) (a : Ω) => φ j fun (i : ↥(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.iIndepFun.finsetSum
{β' : Type u_7}
{Ω : Type u_10}
{ι : Type u_11}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[m : MeasurableSpace β']
[AddCommMonoid β']
[MeasurableAdd₂ β']
{f : ι → Ω → β'}
{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))
:
iIndepFun (fun (j : J) (a : Ω) => ∑ i ∈ S j, f i a) μ
theorem
ProbabilityTheory.IndepFun.finsetSum
{β' : Type u_7}
{Ω : Type u_10}
{ι : Type u_11}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[m : MeasurableSpace β']
[AddCommMonoid β']
[MeasurableAdd₂ β']
{f : ι → Ω → β'}
{s t : Finset ι}
(hf_Indep : iIndepFun f μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
(h_disj : Disjoint s t)
:
IndepFun (∑ i ∈ s, f i) (∑ i ∈ t, f i) μ
theorem
ProbabilityTheory.iIndepFun.finsets_comp'
{Ω : Type u_10}
{ι : Type u_11}
[MeasurableSpace Ω]
{β : ι → Type u_14}
[m : (i : ι) → MeasurableSpace (β i)]
{μ : MeasureTheory.Measure Ω}
{f : (i : ι) → Ω → β i}
{S S' : Finset ι}
(h_disjoint : Disjoint S S')
(hf_Indep : iIndepFun f μ)
(hf_meas : ∀ (i : ι), Measurable (f i))
{γ γ' : Type u}
{mγ : MeasurableSpace γ}
{mγ' : MeasurableSpace γ'}
{φ : ((i : ↥S) → β ↑i) → γ}
{φ' : ((i : ↥S') → β ↑i) → γ'}
(hφ : Measurable φ)
(hφ' : Measurable φ')
:
IndepFun (fun (a : Ω) => φ fun (i : ↥S) => f (↑i) a) (fun (a : Ω) => φ' fun (i : ↥S') => f (↑i) a) μ
A variant of iIndepFun.finsets_comp where we conclude the independence of just two functions rather than an entire family.
@[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.measurable_sigmaCurry
{ι : Type u_1}
{κ : ι → Type u_3}
{α : (i : ι) → κ i → Type u_4}
[m : (i : ι) → (j : κ i) → MeasurableSpace (α 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 : 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 μ)
:
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 μ)
:
let β := fun (k : ι') => (i : ↥(ST k)) → α ↑i;
iIndepFun (fun (k : ι') (x : Ω) (i : ↥(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 : iIndepFun f μ)
(hfg : ∀ (i : ι), f i =ᵐ[μ] g i)
:
iIndepFun g μ
TODO: a kernel version of this theorem