Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Mathlib/Probability/HasLaw.lean
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ lemma HasLaw.fun_comp {𝒴 : Type*} {m𝒴 : MeasurableSpace 𝒴} {ν : Measur
@[to_additive]
lemma IndepFun.hasLaw_mul {M : Type*} [Monoid M] {mM : MeasurableSpace M} [MeasurableMul₂ M]
{μ ν : Measure M} [SigmaFinite μ] [SigmaFinite ν] {X Y : Ω → M}
(hX : HasLaw X μ P) (hY : HasLaw Y ν P) (hXY : IndepFun X Y P) :
(hX : HasLaw X μ P) (hY : HasLaw Y ν P) (hXY : X ⟂ᵢ[P] Y) :
HasLaw (X * Y) (μ ∗ₘ ν) P where
map_eq := by
rw [hXY.map_mul_eq_map_mconv_map₀' hX.aemeasurable hY.aemeasurable, hX.map_eq, hY.map_eq]
Expand All @@ -90,7 +90,7 @@ lemma IndepFun.hasLaw_mul {M : Type*} [Monoid M] {mM : MeasurableSpace M} [Measu
@[to_additive]
lemma IndepFun.hasLaw_fun_mul {M : Type*} [Monoid M] {mM : MeasurableSpace M} [MeasurableMul₂ M]
{μ ν : Measure M} [SigmaFinite μ] [SigmaFinite ν] {X Y : Ω → M}
(hX : HasLaw X μ P) (hY : HasLaw Y ν P) (hXY : IndepFun X Y P) :
(hX : HasLaw X μ P) (hY : HasLaw Y ν P) (hXY : X ⟂ᵢ[P] Y) :
HasLaw (fun ω ↦ X ω * Y ω) (μ ∗ₘ ν) P := hXY.hasLaw_mul hX hY

lemma HasLaw.integral_comp {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Probability/IdentDistrib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -332,9 +332,9 @@ end UniformIntegrable
then `X'` and `Y'` are independent. -/
lemma indepFun_of_identDistrib_pair
{μ : Measure γ} {μ' : Measure δ} [IsFiniteMeasure μ] [IsFiniteMeasure μ']
{X : γ → α} {X' : δ → α} {Y : γ → β} {Y' : δ → β} (h_indep : IndepFun X Y μ)
{X : γ → α} {X' : δ → α} {Y : γ → β} {Y' : δ → β} (h_indep : X ⟂ᵢ[μ] Y)
(h_ident : IdentDistrib (fun ω ↦ (X ω, Y ω)) (fun ω ↦ (X' ω, Y' ω)) μ μ') :
IndepFun X' Y' μ' := by
X' ⟂ᵢ[μ'] Y' := by
rw [indepFun_iff_map_prod_eq_prod_map_map _ _, ← h_ident.map_eq,
(indepFun_iff_map_prod_eq_prod_map_map _ _).1 h_indep]
· exact congr (congrArg Measure.prod <| (h_ident.comp measurable_fst).map_eq)
Expand Down
72 changes: 43 additions & 29 deletions Mathlib/Probability/Independence/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,13 @@ import Mathlib.MeasureTheory.Group.Convolution
measurable space structures they generate are independent.
* `IndepSets.indep`: variant with two π-systems.

## Notation

* `X ⟂ᵢ[μ] Y` for `IndepFun X Y μ`, independence of two random variables.
* `X ⟂ᵢ Y` for `IndepFun X Y volume`.

These notations are scoped in the `ProbabilityTheory` namespace.

## Implementation notes

The definitions of independence in this file are a particular case of independence with respect to a
Expand Down Expand Up @@ -128,13 +135,20 @@ def iIndepFun {_mΩ : MeasurableSpace Ω} {β : ι → Type*} [m : ∀ x : ι, M

/-- Two functions are independent if the two measurable space structures they generate are
independent. For a function `f` with codomain having measurable space structure `m`, the generated
measurable space structure is `MeasurableSpace.comap f m`. -/
measurable space structure is `MeasurableSpace.comap f m`.
We use the notation `f ⟂ᵢ[μ] g` for `IndepFun f g μ` (scoped in `ProbabilityTheory`). -/
def IndepFun {β γ} {_mΩ : MeasurableSpace Ω} [MeasurableSpace β] [MeasurableSpace γ]
(f : Ω → β) (g : Ω → γ) (μ : Measure Ω := by volume_tac) : Prop :=
Kernel.IndepFun f g (Kernel.const Unit μ) (Measure.dirac () : Measure Unit)

end Definitions

@[inherit_doc ProbabilityTheory.IndepFun]
scoped[ProbabilityTheory] notation3 X:50 " ⟂ᵢ[" μ "] " Y:50 => ProbabilityTheory.IndepFun X Y μ

@[inherit_doc ProbabilityTheory.IndepFun]
scoped[ProbabilityTheory] notation3 X:50 " ⟂ᵢ " Y:50 => ProbabilityTheory.IndepFun X Y volume

section Definition_lemmas
variable {π : ι → Set (Set Ω)} {m : ι → MeasurableSpace Ω} {_ : MeasurableSpace Ω} {μ : Measure Ω}
{S : Finset ι} {s : ι → Set Ω}
Expand Down Expand Up @@ -250,17 +264,17 @@ lemma iIndepFun.meas_iInter [Fintype ι] {m : ∀ i, MeasurableSpace (κ i)} {f

lemma IndepFun_iff_Indep [mβ : MeasurableSpace β]
[mγ : MeasurableSpace γ] (f : Ω → β) (g : Ω → γ) (μ : Measure Ω) :
IndepFun f g μ ↔ Indep (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) μ := by
f ⟂ᵢ[μ] g ↔ Indep (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) μ := by
simp only [IndepFun, Indep, Kernel.IndepFun]

lemma IndepFun_iff {β γ} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ]
(f : Ω → β) (g : Ω → γ) (μ : Measure Ω) :
IndepFun f g μ ↔ ∀ t1 t2, MeasurableSet[MeasurableSpace.comap f mβ] t1
f ⟂ᵢ[μ] g ↔ ∀ t1 t2, MeasurableSet[MeasurableSpace.comap f mβ] t1
→ MeasurableSet[MeasurableSpace.comap g mγ] t2 → μ (t1 ∩ t2) = μ t1 * μ t2 := by
rw [IndepFun_iff_Indep, Indep_iff]

lemma IndepFun.meas_inter [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] {f : Ω → β} {g : Ω → γ}
(hfg : IndepFun f g μ) {s t : Set Ω} (hs : MeasurableSet[mβ.comap f] s)
(hfg : f ⟂ᵢ[μ] g) {s t : Set Ω} (hs : MeasurableSet[mβ.comap f] s)
(ht : MeasurableSet[mγ.comap g] t) :
μ (s ∩ t) = μ s * μ t :=
(IndepFun_iff _ _ _).1 hfg _ _ hs ht
Expand Down Expand Up @@ -366,7 +380,7 @@ theorem iIndep.indep
theorem iIndepFun.indepFun {β : ι → Type*}
{m : ∀ x, MeasurableSpace (β x)} {f : ∀ i, Ω → β i} (hf_Indep : iIndepFun f μ) {i j : ι}
(hij : i ≠ j) :
IndepFun (f i) (f j) μ :=
f i ⟂ᵢ[μ] f j :=
Kernel.iIndepFun.indepFun hf_Indep hij

end FromIndepToIndep
Expand Down Expand Up @@ -563,7 +577,7 @@ variable {β β' γ γ' : Type*} {_mΩ : MeasurableSpace Ω} {μ : Measure Ω} {

theorem indepFun_iff_measure_inter_preimage_eq_mul {mβ : MeasurableSpace β}
{mβ' : MeasurableSpace β'} :
IndepFun f g μ
f ⟂ᵢ[μ] g
∀ s t, MeasurableSet s → MeasurableSet t
→ μ (f ⁻¹' s ∩ g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t) := by
simp only [IndepFun, Kernel.indepFun_iff_measure_inter_preimage_eq_mul, ae_dirac_eq,
Expand Down Expand Up @@ -600,14 +614,14 @@ nonrec lemma iIndepFun.comp₀ {β γ : ι → Type*} {mβ : ∀ i, MeasurableSp

theorem indepFun_iff_indepSet_preimage {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
[IsZeroOrProbabilityMeasure μ] (hf : Measurable f) (hg : Measurable g) :
IndepFun f g μ
f ⟂ᵢ[μ] g
∀ s t, MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) μ := by
simp only [IndepFun, IndepSet, Kernel.indepFun_iff_indepSet_preimage hf hg]

theorem indepFun_iff_map_prod_eq_prod_map_map' {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
(hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
(σf : SigmaFinite (μ.map f)) (σg : SigmaFinite (μ.map g)) :
IndepFun f g μ ↔ μ.map (fun ω ↦ (f ω, g ω)) = (μ.map f).prod (μ.map g) := by
f ⟂ᵢ[μ] g ↔ μ.map (fun ω ↦ (f ω, g ω)) = (μ.map f).prod (μ.map g) := by
rw [indepFun_iff_measure_inter_preimage_eq_mul]
have h₀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) :
μ (f ⁻¹' s) * μ (g ⁻¹' t) = μ.map f s * μ.map g t ∧
Expand All @@ -622,7 +636,7 @@ theorem indepFun_iff_map_prod_eq_prod_map_map' {mβ : MeasurableSpace β} {mβ'

theorem indepFun_iff_map_prod_eq_prod_map_map {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
[IsFiniteMeasure μ] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
IndepFun f g μ ↔ μ.map (fun ω ↦ (f ω, g ω)) = (μ.map f).prod (μ.map g) := by
f ⟂ᵢ[μ] g ↔ μ.map (fun ω ↦ (f ω, g ω)) = (μ.map f).prod (μ.map g) := by
apply indepFun_iff_map_prod_eq_prod_map_map' hf hg <;> apply IsFiniteMeasure.toSigmaFinite

theorem iIndepFun_iff_map_fun_eq_pi_map [Fintype ι] {β : ι → Type*}
Expand Down Expand Up @@ -655,11 +669,11 @@ theorem iIndepFun_iff_map_fun_eq_pi_map [Fintype ι] {β : ι → Type*}

@[symm]
nonrec theorem IndepFun.symm {_ : MeasurableSpace β} {_ : MeasurableSpace β'}
(hfg : IndepFun f g μ) : IndepFun g f μ := hfg.symm
(hfg : f ⟂ᵢ[μ] g) : g ⟂ᵢ[μ] f := hfg.symm

theorem IndepFun.congr {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
{f' : Ω → β} {g' : Ω → β'} (hfg : IndepFun f g μ)
(hf : f =ᵐ[μ] f') (hg : g =ᵐ[μ] g') : IndepFun f' g' μ := by
{f' : Ω → β} {g' : Ω → β'} (hfg : f ⟂ᵢ[μ] g) (hf : f =ᵐ[μ] f') (hg : g =ᵐ[μ] g') :
f' ⟂ᵢ[μ] g' := by
refine Kernel.IndepFun.congr' hfg ?_ ?_ <;> simpa

@[deprecated (since := "2025-03-18")] alias IndepFun.ae_eq := IndepFun.congr
Expand All @@ -673,7 +687,7 @@ variable {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'
/-- Given random variables `X : Ω → 𝓧` and `Y : Ω' → 𝓨`, they are independent when viewed as random
variables defined on the product space `Ω × Ω'`. -/
lemma indepFun_prod (mX : Measurable X) (mY : Measurable Y) :
IndepFun (fun ω ↦ X ω.1) (fun ω ↦ Y ω.2) (μ.prod ν) := by
(fun ω ↦ X ω.1) ⟂ᵢ[μ.prod ν] (fun ω ↦ Y ω.2) := by
refine indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop) |>.2 ?_
convert Measure.map_prod_map μ ν mX mY |>.symm
· rw [← Function.comp_def, ← Measure.map_map mX measurable_fst, Measure.map_fst_prod,
Expand All @@ -684,8 +698,8 @@ lemma indepFun_prod (mX : Measurable X) (mY : Measurable Y) :
/-- Given random variables `X : Ω → 𝓧` and `Y : Ω' → 𝓨`, they are independent when viewed as random
variables defined on the product space `Ω × Ω'`. -/
lemma indepFun_prod₀ (mX : AEMeasurable X μ) (mY : AEMeasurable Y ν) :
IndepFun (fun ω ↦ X ω.1) (fun ω ↦ Y ω.2) (μ.prod ν) := by
have : IndepFun (fun ω ↦ mX.mk X ω.1) (fun ω ↦ mY.mk Y ω.2) (μ.prod ν) :=
(fun ω ↦ X ω.1) ⟂ᵢ[μ.prod ν] (fun ω ↦ Y ω.2) := by
have : (fun ω ↦ mX.mk X ω.1) ⟂ᵢ[μ.prod ν] (fun ω ↦ mY.mk Y ω.2) :=
indepFun_prod mX.measurable_mk mY.measurable_mk
refine this.congr ?_ ?_
· rw [← Function.comp_def, ← Function.comp_def]
Expand Down Expand Up @@ -722,34 +736,34 @@ end Prod

theorem IndepFun.comp {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'}
{_mγ : MeasurableSpace γ} {_mγ' : MeasurableSpace γ'} {φ : β → γ} {ψ : β' → γ'}
(hfg : IndepFun f g μ) (hφ : Measurable φ) (hψ : Measurable ψ) :
IndepFun (φ ∘ f) (ψ ∘ g) μ :=
(hfg : f ⟂ᵢ[μ] g) (hφ : Measurable φ) (hψ : Measurable ψ) :
(φ ∘ f) ⟂ᵢ[μ] ψ ∘ g :=
Kernel.IndepFun.comp hfg hφ hψ

theorem IndepFun.comp₀ {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'}
{_mγ : MeasurableSpace γ} {_mγ' : MeasurableSpace γ'} {φ : β → γ} {ψ : β' → γ'}
(hfg : IndepFun f g μ) (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
(hfg : f ⟂ᵢ[μ] g) (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
(hφ : AEMeasurable φ (μ.map f)) (hψ : AEMeasurable ψ (μ.map g)) :
IndepFun (φ ∘ f) (ψ ∘ g) μ :=
(φ ∘ f) ⟂ᵢ[μ] (ψ ∘ g) :=
Kernel.IndepFun.comp₀ hfg (by simp [hf]) (by simp [hg]) (by simp [hφ]) (by simp [hψ])

lemma indepFun_const_left {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
[IsZeroOrProbabilityMeasure μ] (c : β) (X : Ω → β') :
IndepFun (fun _ ↦ c) X μ :=
(fun _ ↦ c) ⟂ᵢ[μ] X :=
Kernel.indepFun_const_left c X

lemma indepFun_const_right {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
[IsZeroOrProbabilityMeasure μ] (X : Ω → β) (c : β') :
IndepFun X (fun _ ↦ c) μ :=
X ⟂ᵢ[μ] (fun _ ↦ c) :=
Kernel.indepFun_const_right X c

theorem IndepFun.neg_right {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [Neg β']
[MeasurableNeg β'] (hfg : IndepFun f g μ) :
IndepFun f (-g) μ := hfg.comp measurable_id measurable_neg
[MeasurableNeg β'] (hfg : f ⟂ᵢ[μ] g) :
f ⟂ᵢ[μ] (-g) := hfg.comp measurable_id measurable_neg

theorem IndepFun.neg_left {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [Neg β]
[MeasurableNeg β] (hfg : IndepFun f g μ) :
IndepFun (-f) g μ := hfg.comp measurable_neg measurable_id
[MeasurableNeg β] (hfg : f ⟂ᵢ[μ] g) :
(-f) ⟂ᵢ[μ] g := hfg.comp measurable_neg measurable_id

section iIndepFun
variable {β : ι → Type*} {m : ∀ i, MeasurableSpace (β i)} {f : ∀ i, Ω → β i}
Expand Down Expand Up @@ -1042,7 +1056,7 @@ variable {M : Type*} [Monoid M] [MeasurableSpace M] [MeasurableMul₂ M]
@[to_additive]
theorem IndepFun.map_mul_eq_map_mconv_map₀'
{f g : Ω → M} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
(σf : SigmaFinite (μ.map f)) (σg : SigmaFinite (μ.map g)) (hfg : IndepFun f g μ) :
(σf : SigmaFinite (μ.map f)) (σg : SigmaFinite (μ.map g)) (hfg : f ⟂ᵢ[μ] g) :
μ.map (f * g) = (μ.map f) ∗ₘ (μ.map g) := by
conv in f * g => change (fun x ↦ x.1 * x.2) ∘ (fun ω ↦ (f ω, g ω))
rw [← measurable_mul.aemeasurable.map_map_of_aemeasurable (hf.prodMk hg),
Expand All @@ -1051,22 +1065,22 @@ theorem IndepFun.map_mul_eq_map_mconv_map₀'
@[to_additive]
theorem IndepFun.map_mul_eq_map_mconv_map'
{f g : Ω → M} (hf : Measurable f) (hg : Measurable g)
(σf : SigmaFinite (μ.map f)) (σg : SigmaFinite (μ.map g)) (hfg : IndepFun f g μ) :
(σf : SigmaFinite (μ.map f)) (σg : SigmaFinite (μ.map g)) (hfg : f ⟂ᵢ[μ] g) :
μ.map (f * g) = (μ.map f) ∗ₘ (μ.map g) :=
hfg.map_mul_eq_map_mconv_map₀' hf.aemeasurable hg.aemeasurable σf σg

@[to_additive]
theorem IndepFun.map_mul_eq_map_mconv_map₀
[IsFiniteMeasure μ] {f g : Ω → M} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
(hfg : IndepFun f g μ) :
(hfg : f ⟂ᵢ[μ] g) :
μ.map (f * g) = (μ.map f) ∗ₘ (μ.map g) := by
apply hfg.map_mul_eq_map_mconv_map₀' hf hg
<;> apply IsFiniteMeasure.toSigmaFinite

@[to_additive]
theorem IndepFun.map_mul_eq_map_mconv_map
[IsFiniteMeasure μ] {f g : Ω → M} (hf : Measurable f) (hg : Measurable g)
(hfg : IndepFun f g μ) :
(hfg : f ⟂ᵢ[μ] g) :
μ.map (f * g) = (μ.map f) ∗ₘ (μ.map g) :=
hfg.map_mul_eq_map_mconv_map₀ hf.aemeasurable hg.aemeasurable

Expand Down
6 changes: 3 additions & 3 deletions Mathlib/Probability/Independence/CharacteristicFunction.lean
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ variable [InnerProductSpace ℝ E] [InnerProductSpace ℝ F]
to the product of the characteristic functions. This is the version for Hilbert spaces, see
`indepFun_iff_charFunDual_prod` for the Banach space version. -/
lemma indepFun_iff_charFun_prod (hX : AEMeasurable X P) (hY : AEMeasurable Y P) :
IndepFun X Y P ↔ ∀ t, charFun (P.map (fun ω ↦ toLp 2 (X ω, Y ω))) t =
X ⟂ᵢ[P] Y ↔ ∀ t, charFun (P.map (fun ω ↦ toLp 2 (X ω, Y ω))) t =
charFun (P.map X) t.ofLp.1 * charFun (P.map Y) t.ofLp.2 := by
rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← charFun_eq_prod_iff,
AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]
Expand All @@ -55,7 +55,7 @@ variable [NormedSpace ℝ E] [NormedSpace ℝ F]
to the product of the characteristic functions. This is the version for Banach spaces, see
`indepFun_iff_charFun_prod` for the Hilbert space version. -/
lemma indepFun_iff_charFunDual_prod (hX : AEMeasurable X P) (hY : AEMeasurable Y P) :
IndepFun X Y P ↔ ∀ L, charFunDual (P.map (fun ω ↦ (X ω, Y ω))) L =
X ⟂ᵢ[P] Y ↔ ∀ L, charFunDual (P.map (fun ω ↦ (X ω, Y ω))) L =
charFunDual (P.map X) (L.comp (.inl ℝ E F)) *
charFunDual (P.map Y) (L.comp (.inr ℝ E F)) := by
rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← charFunDual_eq_prod_iff]
Expand All @@ -64,7 +64,7 @@ lemma indepFun_iff_charFunDual_prod (hX : AEMeasurable X P) (hY : AEMeasurable Y
to the product of the characteristic functions. This is `indepFun_iff_charFunDual_prod` for
`WithLp`. See `indepFun_iff_charFun_prod` for the Hilbert space version. -/
lemma indepFun_iff_charFunDual_prod' (hX : AEMeasurable X P) (hY : AEMeasurable Y P) :
IndepFun X Y P ↔ ∀ L, charFunDual (P.map (fun ω ↦ toLp p (X ω, Y ω))) L =
X ⟂ᵢ[P] Y ↔ ∀ L, charFunDual (P.map (fun ω ↦ toLp p (X ω, Y ω))) L =
charFunDual (P.map X) (L.comp
((prodContinuousLinearEquiv p ℝ E F).symm.toContinuousLinearMap.comp
(.inl ℝ E F))) *
Expand Down
30 changes: 25 additions & 5 deletions Mathlib/Probability/Independence/Conditional.lean
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,14 @@ as for a family, but without the starting `i`, for example `CondIndepFun` is the
of sets, then the measurable space structures they generate are conditionally independent.
* `ProbabilityTheory.condIndepSets.condIndep`: variant with two π-systems.

## Notation

* `X ⟂ᵢ[Z, hZ; μ] Y` for `CondIndepFun (MeasurableSpace.comap Z inferInstance) hZ.comap_le X Y μ`,
independence of `X` and `Y` given `Z`.
* `X ⟂ᵢ[Z, hZ] Y` for the cases of `μ = volume`.

These notations are scoped in the `ProbabilityTheory` namespace.

## Implementation notes

The definitions of conditional independence in this file are a particular case of independence with
Expand Down Expand Up @@ -136,7 +144,9 @@ def iCondIndepFun {β : ι → Type*} [m : ∀ x : ι, MeasurableSpace (β x)]
/-- Two functions are conditionally independent if the two measurable space structures they generate
are conditionally independent. For a function `f` with codomain having measurable space structure
`m`, the generated measurable space structure is `m.comap f`.
See `ProbabilityTheory.condIndepFun_iff`. -/
See `ProbabilityTheory.condIndepFun_iff`.
We use the notation `X ⟂ᵢ[Z, hZ; μ] Y` to write that `X` and `Y` are conditionally independent
given (the σ-algebra generated by) `Z` (scoped in `ProbabilityTheory`). -/
def CondIndepFun {β γ : Type*} [MeasurableSpace β] [MeasurableSpace γ]
(f : Ω → β) (g : Ω → γ) (μ : Measure Ω := by volume_tac) [IsFiniteMeasure μ] : Prop :=
Kernel.IndepFun f g (condExpKernel μ m') (μ.trim hm')
Expand All @@ -145,6 +155,16 @@ end

end Definitions

@[inherit_doc ProbabilityTheory.CondIndepFun]
scoped[ProbabilityTheory] notation3 X:50 " ⟂ᵢ[" Z ", " hZ "; " μ "] " Y:50 =>
ProbabilityTheory.CondIndepFun (MeasurableSpace.comap Z inferInstance) (Measurable.comap_le hZ)
X Y μ

@[inherit_doc ProbabilityTheory.CondIndepFun]
scoped[ProbabilityTheory] notation3 X:50 " ⟂ᵢ[" Z ", " hZ "] " Y:50 =>
ProbabilityTheory.CondIndepFun (MeasurableSpace.comap Z inferInstance) (Measurable.comap_le hZ)
X Y volume

section DefinitionLemmas

section
Expand Down Expand Up @@ -731,12 +751,12 @@ lemma condIndepFun_of_measurable_right {mβ : MeasurableSpace β} {mβ' : Measur

lemma condIndepFun_self_left {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
{X : Ω → β} {Z : Ω → β'} (hX : Measurable X) (hZ : Measurable Z) :
CondIndepFun (mβ'.comap Z) hZ.comap_le Z X μ :=
Z ⟂ᵢ[Z, hZ; μ] X :=
condIndepFun_of_measurable_left (comap_measurable Z) hX

lemma condIndepFun_self_right {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
{X : Ω → β} {Z : Ω → β'} (hX : Measurable X) (hZ : Measurable Z) :
CondIndepFun (mβ'.comap Z) hZ.comap_le X Z μ :=
X ⟂ᵢ[Z, hZ; μ] Z :=
condIndepFun_of_measurable_right hX (comap_measurable Z)

/-- Two random variables are conditionally independent iff they satisfy the almost sure equality
Expand Down Expand Up @@ -797,7 +817,7 @@ theorem condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib
{γ : Type*} {mγ : MeasurableSpace γ} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
[StandardBorelSpace β] [Nonempty β] [StandardBorelSpace β'] [Nonempty β']
(hf : Measurable f) (hg : Measurable g) {k : Ω → γ} (hk : Measurable k) :
CondIndepFun _ hk.comap_le f g μ
f ⟂ᵢ[k, hk; μ] g
μ.map (fun ω ↦ (k ω, f ω, g ω)) =
(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ μ.map k := by
rw [condIndepFun_iff_map_prod_eq_prod_comp_trim hf hg]
Expand Down Expand Up @@ -847,7 +867,7 @@ theorem condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft
{γ : Type*} {mγ : MeasurableSpace γ} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
[StandardBorelSpace β] [Nonempty β] [StandardBorelSpace β'] [Nonempty β']
(hf : Measurable f) (hg : Measurable g) {k : Ω → γ} (hk : Measurable k) :
CondIndepFun (mγ.comap k) hk.comap_le g f μ
g ⟂ᵢ[k, hk; μ] f
condDistrib f (fun ω ↦ (k ω, g ω)) μ =ᵐ[μ.map (fun ω ↦ (k ω, g ω))]
(condDistrib f k μ).prodMkRight _ := by
rw [condDistrib_ae_eq_iff_measure_eq_compProd (μ := μ) _ hf.aemeasurable,
Expand Down
Loading