refactor(Probability/Kernel/Composition): define compProd for all kernels (#6054)

`compProd` and `prod` make sense only for s-finite kernels and were defined only for those. I define them for all kernels, with default value 0 when one of the kernels is not s-finite. The new definitions allow rewriting a kernel inside a compProd, which was not possible before (it would raise a "motive is not type correct" error due to the s-finite argument).



Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

Author: RemyDegenne

Mathlib/Probability/Kernel/Composition.lean

@@ -187,15 +187,20 @@ theorem measurable_compProdFun (κ : kernel α β) [IsSFiniteKernel κ] (η : ke
   exact h_meas.lintegral_kernel_prod_right
 #align probability_theory.kernel.measurable_comp_prod_fun ProbabilityTheory.kernel.measurable_compProdFun
 
-/-- Composition-Product of kernels. It verifies
+open Classical
+
+/-- Composition-Product of kernels. For s-finite kernels, it satisfies
 `∫⁻ bc, f bc ∂(compProd κ η a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a)`
-(see `lintegral_compProd`). -/
-noncomputable def compProd (κ : kernel α β) [IsSFiniteKernel κ] (η : kernel (α × β) γ)
-    [IsSFiniteKernel η] : kernel α (β × γ) where
-  val a :=
+(see `ProbabilityTheory.kernel.lintegral_compProd`).
+If either of the kernels is not s-finite, `compProd` is given the junk value 0. -/
+noncomputable def compProd (κ : kernel α β) (η : kernel (α × β) γ) : kernel α (β × γ) :=
+if h : IsSFiniteKernel κ ∧ IsSFiniteKernel η then
+{ val := λ a ↦
     Measure.ofMeasurable (fun s _ => compProdFun κ η a s) (compProdFun_empty κ η a)
-      (compProdFun_iUnion κ η a)
+      (@compProdFun_iUnion _ _ _ _ _ _ κ η h.2 a)
   property := by
+    have : IsSFiniteKernel κ := h.1
+    have : IsSFiniteKernel η := h.2
     refine' Measure.measurable_of_measurable_coe _ fun s hs => _
     have :
       (fun a =>
@@ -204,14 +209,18 @@ noncomputable def compProd (κ : kernel α β) [IsSFiniteKernel κ] (η : kernel
         fun a => compProdFun κ η a s :=
       by ext1 a; rwa [Measure.ofMeasurable_apply]
     rw [this]
-    exact measurable_compProdFun κ η hs
+    exact measurable_compProdFun κ η hs }
+else 0
 #align probability_theory.kernel.comp_prod ProbabilityTheory.kernel.compProd
 
 scoped[ProbabilityTheory] infixl:100 " ⊗ₖ " => ProbabilityTheory.kernel.compProd
 
 theorem compProd_apply_eq_compProdFun (κ : kernel α β) [IsSFiniteKernel κ] (η : kernel (α × β) γ)
-    [IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) : (κ ⊗ₖ η) a s = compProdFun κ η a s := by
-  rw [compProd]
+    [IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) :
+    (κ ⊗ₖ η) a s = compProdFun κ η a s := by
+  rw [compProd, dif_pos]
+  swap
+  · constructor <;> infer_instance
   change
     Measure.ofMeasurable (fun s _ => compProdFun κ η a s) (compProdFun_empty κ η a)
         (compProdFun_iUnion κ η a) s =
@@ -220,6 +229,18 @@ theorem compProd_apply_eq_compProdFun (κ : kernel α β) [IsSFiniteKernel κ] (
   rfl
 #align probability_theory.kernel.comp_prod_apply_eq_comp_prod_fun ProbabilityTheory.kernel.compProd_apply_eq_compProdFun
 
+theorem compProd_of_not_isSFiniteKernel_left (κ : kernel α β) (η : kernel (α × β) γ)
+    (h : ¬ IsSFiniteKernel κ) :
+    κ ⊗ₖ η = 0 := by
+  rw [compProd, dif_neg]
+  simp [h]
+
+theorem compProd_of_not_isSFiniteKernel_right (κ : kernel α β) (η : kernel (α × β) γ)
+    (h : ¬ IsSFiniteKernel η) :
+    κ ⊗ₖ η = 0 := by
+  rw [compProd, dif_neg]
+  simp [h]
+
 theorem compProd_apply (κ : kernel α β) [IsSFiniteKernel κ] (η : kernel (α × β) γ)
     [IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) :
     (κ ⊗ₖ η) a s = ∫⁻ b, η (a, b) {c | (b, c) ∈ s} ∂κ a :=
@@ -449,16 +470,24 @@ theorem compProd_eq_sum_compProd (κ : kernel α β) [IsSFiniteKernel κ] (η :
   ext a s hs; simp_rw [kernel.sum_apply' _ a hs]; rw [compProd_eq_tsum_compProd κ η a hs]
 #align probability_theory.kernel.comp_prod_eq_sum_comp_prod ProbabilityTheory.kernel.compProd_eq_sum_compProd
 
-theorem compProd_eq_sum_compProd_left (κ : kernel α β) [IsSFiniteKernel κ] (η : kernel (α × β) γ)
-    [IsSFiniteKernel η] : κ ⊗ₖ η = kernel.sum fun n => seq κ n ⊗ₖ η := by
+theorem compProd_eq_sum_compProd_left (κ : kernel α β) [IsSFiniteKernel κ] (η : kernel (α × β) γ) :
+  κ ⊗ₖ η = kernel.sum fun n => seq κ n ⊗ₖ η := by
+  by_cases h : IsSFiniteKernel η
+  swap
+  · simp_rw [compProd_of_not_isSFiniteKernel_right _ _ h]
+    simp
   rw [compProd_eq_sum_compProd]
   congr with n a s hs
   simp_rw [kernel.sum_apply' _ _ hs, compProd_apply_eq_compProdFun _ _ _ hs,
     compProdFun_tsum_right _ η a hs]
 #align probability_theory.kernel.comp_prod_eq_sum_comp_prod_left ProbabilityTheory.kernel.compProd_eq_sum_compProd_left
 
-theorem compProd_eq_sum_compProd_right (κ : kernel α β) [IsSFiniteKernel κ] (η : kernel (α × β) γ)
+theorem compProd_eq_sum_compProd_right (κ : kernel α β) (η : kernel (α × β) γ)
     [IsSFiniteKernel η] : κ ⊗ₖ η = kernel.sum fun n => κ ⊗ₖ seq η n := by
+  by_cases hκ : IsSFiniteKernel κ
+  swap
+  · simp_rw [compProd_of_not_isSFiniteKernel_left _ _ hκ]
+    simp
   rw [compProd_eq_sum_compProd]
   simp_rw [compProd_eq_sum_compProd_left κ _]
   rw [kernel.sum_comm]
@@ -472,8 +501,12 @@ instance IsMarkovKernel.compProd (κ : kernel α β) [IsMarkovKernel κ] (η : k
       simp only [Set.mem_univ, Set.setOf_true, measure_univ, lintegral_one]⟩⟩
 #align probability_theory.kernel.is_markov_kernel.comp_prod ProbabilityTheory.kernel.IsMarkovKernel.compProd
 
-theorem compProd_apply_univ_le (κ : kernel α β) [IsSFiniteKernel κ] (η : kernel (α × β) γ)
-    [IsFiniteKernel η] (a : α) : (κ ⊗ₖ η) a Set.univ ≤ κ a Set.univ * IsFiniteKernel.bound η := by
+theorem compProd_apply_univ_le (κ : kernel α β) (η : kernel (α × β) γ) [IsFiniteKernel η] (a : α) :
+    (κ ⊗ₖ η) a Set.univ ≤ κ a Set.univ * IsFiniteKernel.bound η := by
+  by_cases hκ : IsSFiniteKernel κ
+  swap
+  · rw [compProd_of_not_isSFiniteKernel_left _ _ hκ]
+    simp
   rw [compProd_apply κ η a MeasurableSet.univ]
   simp only [Set.mem_univ, Set.setOf_true]
   let Cη := IsFiniteKernel.bound η
@@ -494,8 +527,16 @@ instance IsFiniteKernel.compProd (κ : kernel α β) [IsFiniteKernel κ] (η : k
           mul_le_mul (measure_le_bound κ a Set.univ) le_rfl (zero_le _) (zero_le _)⟩⟩
 #align probability_theory.kernel.is_finite_kernel.comp_prod ProbabilityTheory.kernel.IsFiniteKernel.compProd
 
-instance IsSFiniteKernel.compProd (κ : kernel α β) [IsSFiniteKernel κ] (η : kernel (α × β) γ)
-    [IsSFiniteKernel η] : IsSFiniteKernel (κ ⊗ₖ η) := by
+instance IsSFiniteKernel.compProd (κ : kernel α β) (η : kernel (α × β) γ) :
+    IsSFiniteKernel (κ ⊗ₖ η) := by
+  by_cases h : IsSFiniteKernel κ
+  swap
+  · rw [compProd_of_not_isSFiniteKernel_left _ _ h]
+    infer_instance
+  by_cases h : IsSFiniteKernel η
+  swap
+  · rw [compProd_of_not_isSFiniteKernel_right _ _ h]
+    infer_instance
   rw [compProd_eq_sum_compProd]
   exact kernel.isSFiniteKernel_sum fun n => kernel.isSFiniteKernel_sum inferInstance
 #align probability_theory.kernel.is_s_finite_kernel.comp_prod ProbabilityTheory.kernel.IsSFiniteKernel.compProd
@@ -774,7 +815,7 @@ section Comp
 
 variable {γ : Type _} {mγ : MeasurableSpace γ} {f : β → γ} {g : γ → α}
 
-/-- Composition of two s-finite kernels. -/
+/-- Composition of two kernels. -/
 noncomputable def comp (η : kernel β γ) (κ : kernel α β) : kernel α γ where
   val a := (κ a).bind η
   property := (Measure.measurable_bind' (kernel.measurable _)).comp (kernel.measurable _)
@@ -847,9 +888,8 @@ section Prod
 
 variable {γ : Type _} {mγ : MeasurableSpace γ}
 
-/-- Product of two s-finite kernels. -/
-noncomputable def prod (κ : kernel α β) [IsSFiniteKernel κ] (η : kernel α γ) [IsSFiniteKernel η] :
-    kernel α (β × γ) :=
+/-- Product of two kernels. This is meaningful only when the kernels are s-finite. -/
+noncomputable def prod (κ : kernel α β) (η : kernel α γ) : kernel α (β × γ) :=
   κ ⊗ₖ swapLeft (prodMkLeft β η)
 #align probability_theory.kernel.prod ProbabilityTheory.kernel.prod
 
@@ -875,8 +915,8 @@ instance IsFiniteKernel.prod (κ : kernel α β) [IsFiniteKernel κ] (η : kerne
     [IsFiniteKernel η] : IsFiniteKernel (κ ×ₖ η) := by rw [prod]; infer_instance
 #align probability_theory.kernel.is_finite_kernel.prod ProbabilityTheory.kernel.IsFiniteKernel.prod
 
-instance IsSFiniteKernel.prod (κ : kernel α β) [IsSFiniteKernel κ] (η : kernel α γ)
-    [IsSFiniteKernel η] : IsSFiniteKernel (κ ×ₖ η) := by rw [prod]; infer_instance
+instance IsSFiniteKernel.prod (κ : kernel α β) (η : kernel α γ) :
+    IsSFiniteKernel (κ ×ₖ η) := by rw [prod]; infer_instance
 #align probability_theory.kernel.is_s_finite_kernel.prod ProbabilityTheory.kernel.IsSFiniteKernel.prod
 
 end Prod

Mathlib/Probability/Kernel/Disintegration.lean

@@ -262,9 +262,8 @@ variable {Ω : Type _} [TopologicalSpace Ω] [PolishSpace Ω] [MeasurableSpace 
 
 /-- Existence of a conditional kernel. Use the definition `condKernel` to get that kernel. -/
 theorem exists_cond_kernel (γ : Type _) [MeasurableSpace γ] :
-    ∃ (η : kernel α Ω) (h : IsMarkovKernel η), kernel.const γ ρ =
-      @kernel.compProd γ α _ _ Ω _ (kernel.const γ ρ.fst) _ (kernel.prodMkLeft γ η)
-        (by haveI := h; infer_instance) := by
+    ∃ (η : kernel α Ω) (_h : IsMarkovKernel η), kernel.const γ ρ =
+      kernel.compProd (kernel.const γ ρ.fst) (kernel.prodMkLeft γ η) := by
   obtain ⟨f, hf⟩ := exists_measurableEmbedding_real Ω
   let ρ' : Measure (α × ℝ) := ρ.map (Prod.map id f)
   -- The general idea is to define `η = kernel.comapRight (condKernelReal ρ') hf`. There is