feat(Probability): CondIndepFun lemmas (#29554)

Lemmas about conditional independence of constant random variables and of random variables that are measurable with respect to the sigma-algebra that we are conditioning on.

From the LeanBandits project.

Co-authored-by: Remy Degenne <remydegenne@gmail.com>

Author: RemyDegenne

Mathlib/Probability/Independence/Basic.lean

@@ -733,6 +733,16 @@ theorem IndepFun.comp₀ {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β
     IndepFun (φ ∘ 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 μ :=
+  Kernel.indepFun_const_left c X
+
+lemma indepFun_const_right {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
+    [IsZeroOrProbabilityMeasure μ] (X : Ω → β) (c : β') :
+    IndepFun 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

Mathlib/Probability/Independence/Conditional.lean

@@ -676,8 +676,8 @@ theorem condIndepFun_iff_condIndepSet_preimage {mβ : MeasurableSpace β} {mβ'
   simp only [CondIndepFun, CondIndepSet, Kernel.indepFun_iff_indepSet_preimage hf hg]
 
 @[symm]
-nonrec theorem CondIndepFun.symm {_ : MeasurableSpace β} {f g : Ω → β}
-    (hfg : CondIndepFun m' hm' f g μ) :
+nonrec theorem CondIndepFun.symm {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
+    {f : Ω → β} {g : Ω → β'} (hfg : CondIndepFun m' hm' f g μ) :
     CondIndepFun m' hm' g f μ :=
   hfg.symm
 
@@ -687,6 +687,16 @@ theorem CondIndepFun.comp {γ γ' : Type*} {_mβ : MeasurableSpace β} {_mβ' :
     CondIndepFun m' hm' (φ ∘ f) (ψ ∘ g) μ :=
   Kernel.IndepFun.comp hfg hφ hψ
 
+lemma condIndepFun_const_left {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
+    (c : β) (X : Ω → β') :
+    CondIndepFun m' hm' (fun _ ↦ c) X μ :=
+  Kernel.indepFun_const_left c X
+
+lemma condIndepFun_const_right {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
+    (X : Ω → β) (c : β') :
+    CondIndepFun m' hm' X (fun _ ↦ c) μ :=
+  Kernel.indepFun_const_right X c
+
 theorem CondIndepFun.neg_right {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [Neg β']
     [MeasurableNeg β'] (hfg : CondIndepFun m' hm' f g μ) :
     CondIndepFun m' hm' f (-g) μ := hfg.comp measurable_id measurable_neg
@@ -695,6 +705,38 @@ theorem CondIndepFun.neg_left {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpa
     [MeasurableNeg β] (hfg : CondIndepFun m' hm' f g μ) :
     CondIndepFun m' hm' (-f) g μ := hfg.comp measurable_neg measurable_id
 
+lemma condIndepFun_of_measurable_left {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
+    {X : Ω → β} {Y : Ω → β'} (hX : Measurable[m'] X) (hY : Measurable Y) :
+    CondIndepFun m' hm' X Y μ := by
+  rw [condIndepFun_iff _ hm' _ _ (hX.mono hm' le_rfl) hY]
+  rintro _ _ ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩
+  rw [show (fun ω : Ω ↦ (1 : ℝ)) = 1 from rfl, Set.inter_indicator_one]
+  calc μ[(X ⁻¹' s).indicator 1 * (Y ⁻¹' t).indicator 1|m']
+  _ =ᵐ[μ] (X ⁻¹' s).indicator 1 * μ[(Y ⁻¹' t).indicator 1|m'] := by
+    refine condExp_stronglyMeasurable_mul_of_bound hm' (stronglyMeasurable_const.indicator (hX hs))
+      ((integrable_indicator_iff (hY ht)).2 integrableOn_const) 1 (ae_of_all μ fun ω ↦ ?_)
+    rw [Set.indicator]
+    split_ifs with h <;> simp
+  _ =ᵐ[μ] μ[(X ⁻¹' s).indicator 1|m'] * μ[(Y ⁻¹' t).indicator 1|m'] := by
+    nth_rw 2 [condExp_of_stronglyMeasurable hm']
+    · exact stronglyMeasurable_const.indicator (hX hs)
+    · exact (integrable_indicator_iff ((hX.le hm') hs)).2 integrableOn_const
+
+lemma condIndepFun_of_measurable_right {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
+    {X : Ω → β} {Y : Ω → β'} (hX : Measurable X) (hY : Measurable[m'] Y) :
+    CondIndepFun m' hm' X Y μ :=
+  (condIndepFun_of_measurable_left hY hX).symm
+
+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 μ :=
+  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 μ :=
+  condIndepFun_of_measurable_right hX (comap_measurable Z)
+
 section iCondIndepFun
 variable {β : ι → Type*} {m : ∀ i, MeasurableSpace (β i)} {f : ∀ i, Ω → β i}
 

Mathlib/Probability/Independence/Kernel.lean

@@ -1000,6 +1000,17 @@ theorem IndepFun.comp₀ {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
     filter_upwards [haψ] with ω hωψ
     simp [hωψ]
 
+lemma indepFun_const_left {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
+    [IsZeroOrMarkovKernel κ] (c : β') (X : Ω → β) :
+    IndepFun (fun _ ↦ c) X κ μ := by
+  rw [IndepFun, MeasurableSpace.comap_const]
+  exact indep_bot_left _
+
+lemma indepFun_const_right {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
+    [IsZeroOrMarkovKernel κ] (X : Ω → β) (c : β') :
+    IndepFun X (fun _ ↦ c) κ μ :=
+  (indepFun_const_left c X).symm
+
 theorem IndepFun.neg_right {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} [Neg β']
     [MeasurableNeg β'] (hfg : IndepFun f g κ μ) :
     IndepFun f (-g) κ μ := hfg.comp measurable_id measurable_neg