feat(Probability/Independence): relate conditional independence and factorization of a kernel (#29884)

```lean
CondIndepFun m' hm' f g μ
  ↔ (condExpKernel μ m').map (fun ω ↦ (f ω, g ω))
    =ᵐ[μ.trim hm'] (condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g
```

From the LeanBandits project.

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

Author: RemyDegenne

Mathlib/Probability/Independence/Conditional.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
 import Mathlib.Probability.Independence.Kernel
+import Mathlib.Probability.Kernel.CompProdEqIff
+import Mathlib.Probability.Kernel.Composition.Lemmas
 import Mathlib.Probability.Kernel.Condexp
 
 /-!
@@ -737,6 +739,57 @@ lemma condIndepFun_self_right {mβ : MeasurableSpace β} {mβ' : MeasurableSpace
     CondIndepFun (mβ'.comap Z) hZ.comap_le X Z μ :=
   condIndepFun_of_measurable_right hX (comap_measurable Z)
 
+/-- Two random variables are conditionally independent iff they satisfy the almost sure equality
+of conditional expectations `μ⟦f ⁻¹' s ∩ g ⁻¹' t | m'⟧ =ᵐ[μ] μ⟦f ⁻¹' s | m'⟧ * μ⟦g ⁻¹' t | m'⟧`
+for all measurable sets `s` and `t` (see `condIndepFun_iff_condExp_inter_preimage_eq_mul`).
+Here, this is phrased with Markov kernels associated to the conditional expectations, and the
+almost sure equality is expressed as equality of the composition-product with the measure, which is
+equivalent to a.e. equality. See `condIndepFun_iff_map_prod_eq_prod_map_map` for the a.e. equality
+version with kernels.
+
+For a random variable `f`, `(condExpKernel μ m').map f` is the law of the conditional expectation
+of `f` given `m'`: almost surely, `(condExpKernel μ m').map f ω s = μ⟦f ⁻¹' s | m'⟧ ω`. -/
+theorem condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map
+    {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} (hf : Measurable f) (hg : Measurable g) :
+    CondIndepFun m' hm' f g μ
+      ↔ (μ.trim hm') ⊗ₘ (condExpKernel μ m').map (fun ω ↦ (f ω, g ω))
+        = (μ.trim hm') ⊗ₘ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g) :=
+  Kernel.indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map hf hg
+
+/-- Two random variables are conditionally independent iff they satisfy the almost sure equality
+of conditional expectations `μ⟦f ⁻¹' s ∩ g ⁻¹' t | m'⟧ =ᵐ[μ] μ⟦f ⁻¹' s | m'⟧ * μ⟦g ⁻¹' t | m'⟧`
+for all measurable sets `s` and `t` (see `condIndepFun_iff_condExp_inter_preimage_eq_mul`).
+Here, this is phrased with Markov kernels associated to the conditional expectations.
+
+For a random variable `f`, `(condExpKernel μ m').map f` is the law of the conditional expectation
+of `f` given `m'`: almost surely, `(condExpKernel μ m').map f ω s = μ⟦f ⁻¹' s | m'⟧ ω`. -/
+theorem condIndepFun_iff_map_prod_eq_prod_map_map
+    {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} [CountableOrCountablyGenerated Ω (β × β')]
+    (hf : Measurable f) (hg : Measurable g) :
+    CondIndepFun m' hm' f g μ
+      ↔ (condExpKernel μ m').map (fun ω ↦ (f ω, g ω))
+        =ᵐ[μ.trim hm'] (condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g := by
+  rw [condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map hf hg, ← Kernel.compProd_eq_iff]
+
+/-- Two random variables are conditionally independent with respect to `m'` iff the law of
+`(id, f, g)` under `μ`, in which the identity is to the space with σ-algebra `m'`, can be written
+as a product involving the conditional expectations of `f` and `g` given `m'`.
+
+For a random variable `f`, `(condExpKernel μ m').map f` is the law of the conditional expectation
+of `f` given `m'`: almost surely, `(condExpKernel μ m').map f ω s = μ⟦f ⁻¹' s | m'⟧ ω`. -/
+lemma condIndepFun_iff_map_prod_eq_prod_comp_trim
+    {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} (hf : Measurable f) (hg : Measurable g) :
+    CondIndepFun m' hm' f g μ
+      ↔ @Measure.map _ _ _ (m'.prod _) (fun ω ↦ (ω, f ω, g ω)) μ
+        = (Kernel.id ×ₖ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g))
+          ∘ₘ μ.trim hm' := by
+  rw [condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map hf hg]
+  congr!
+  · rw [Measure.compProd_map (by fun_prop), compProd_trim_condExpKernel,
+      Measure.map_map (by fun_prop) ((measurable_id.mono le_rfl hm').prodMk measurable_id)]
+    rfl
+  · rw [Measure.compProd_eq_comp_prod]
+
 section iCondIndepFun
 variable {β : ι → Type*} {m : ∀ i, MeasurableSpace (β i)} {f : ∀ i, Ω → β i}
 

Mathlib/Probability/Independence/Kernel.lean

@@ -1019,6 +1019,43 @@ theorem IndepFun.neg_left {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace 
     [MeasurableNeg β] (hfg : IndepFun f g κ μ) :
     IndepFun (-f) g κ μ := hfg.comp measurable_neg measurable_id
 
+/-- Two random variables `f, g` are independent given a kernel `κ` and a measure `μ` iff
+`μ ⊗ₘ κ.map (fun ω ↦ (f ω, g ω)) = μ ⊗ₘ (κ.map f ×ₖ κ.map g)`. -/
+theorem indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map
+    {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
+    [IsFiniteMeasure μ] [IsFiniteKernel κ] {f : Ω → β} {g : Ω → γ}
+    (hf : Measurable f) (hg : Measurable g) :
+    IndepFun f g κ μ ↔ μ ⊗ₘ κ.map (fun ω ↦ (f ω, g ω)) = μ ⊗ₘ (κ.map f ×ₖ κ.map g) := by
+  classical
+  rw [indepFun_iff_measure_inter_preimage_eq_mul]
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · rw [Measure.ext_prod₃_iff]
+    intro u s t hu hs ht
+    rw [Measure.compProd_apply (hu.prod (hs.prod ht)),
+      Measure.compProd_apply (hu.prod (hs.prod ht))]
+    refine lintegral_congr_ae ?_
+    have h_set_eq ω : Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅ := by ext; simp
+    simp_rw [h_set_eq]
+    filter_upwards [h s t hs ht] with ω hω
+    by_cases hωu : ω ∈ u
+    swap; · simp [hωu]
+    simp only [hωu, ↓reduceIte]
+    rw [map_apply _ (by fun_prop), Measure.map_apply (by fun_prop) (hs.prod ht),
+      mk_preimage_prod, hω, prod_apply_prod, map_apply' _ (by fun_prop), map_apply' _ (by fun_prop)]
+    exacts [ht, hs]
+  · intro s t hs ht
+    rw [Measure.ext_prod₃_iff] at h
+    refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite ?_ ?_ ?_
+    · exact Kernel.measurable_coe _ ((hf hs).inter (hg ht))
+    · exact (Kernel.measurable_coe _ (hf hs)).mul (Kernel.measurable_coe _ (hg ht))
+    intro u hu hμu
+    specialize h hu hs ht
+    rw [Measure.compProd_apply_prod hu (hs.prod ht),
+      Measure.compProd_apply_prod hu (hs.prod ht)] at h
+    convert h with ω ω
+    · rw [map_apply' _ (by fun_prop) _ (hs.prod ht), mk_preimage_prod]
+    · rw [prod_apply_prod, map_apply' _ (by fun_prop) _ hs, map_apply' _ (by fun_prop) _ ht]
+
 section iIndepFun
 variable {β : ι → Type*} {m : ∀ i, MeasurableSpace (β i)} {f : ∀ i, Ω → β i}