feat(Probability/Kernel): add compProd_add_left/right (#11272)

Interaction of the composition-product of kernels with addition.

Mathlib/Probability/Kernel/Basic.lean

@@ -465,6 +465,9 @@ theorem const_apply (μβ : Measure β) (a : α) : const α μβ a = μβ :=
 lemma const_zero : kernel.const α (0 : Measure β) = 0 := by
   ext x s _; simp [kernel.const_apply]
 
+lemma const_add (β : Type*) [MeasurableSpace β] (μ ν : Measure α) :
+    const β (μ + ν) = const β μ + const β ν := by ext; simp
+
 lemma sum_const [Countable ι] (μ : ι → Measure β) :
     kernel.sum (fun n ↦ const α (μ n)) = const α (Measure.sum μ) := by
   ext x s hs

Mathlib/Probability/Kernel/Composition.lean

@@ -558,6 +558,19 @@ instance IsSFiniteKernel.compProd (κ : kernel α β) (η : kernel (α × β) γ
   exact kernel.isSFiniteKernel_sum fun n => kernel.isSFiniteKernel_sum inferInstance
 #align probability_theory.kernel.is_s_finite_kernel.comp_prod ProbabilityTheory.kernel.IsSFiniteKernel.compProd
 
+lemma compProd_add_left (μ κ : kernel α β) (η : kernel (α × β) γ)
+    [IsSFiniteKernel μ] [IsSFiniteKernel κ] [IsSFiniteKernel η] :
+    (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η := by ext _ _ hs; simp [compProd_apply _ _ _ hs]
+
+lemma compProd_add_right (μ : kernel α β) (κ η : kernel (α × β) γ)
+    [IsSFiniteKernel μ] [IsSFiniteKernel κ] [IsSFiniteKernel η] :
+    μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η := by
+  ext a s hs
+  simp only [compProd_apply _ _ _ hs, coeFn_add, Pi.add_apply, Measure.add_toOuterMeasure,
+    OuterMeasure.coe_add]
+  rw [lintegral_add_left]
+  exact measurable_kernel_prod_mk_left' hs a
+
 end CompositionProduct
 
 section MapComap
@@ -737,6 +750,14 @@ lemma prodMkLeft_zero : kernel.prodMkLeft α (0 : kernel β γ) = 0 := by
 lemma prodMkRight_zero : kernel.prodMkRight α (0 : kernel β γ) = 0 := by
   ext x s _; simp
 
+@[simp]
+lemma prodMkLeft_add (κ η : kernel α β) :
+    prodMkLeft γ (κ + η) = prodMkLeft γ κ + prodMkLeft γ η := by ext; simp
+
+@[simp]
+lemma prodMkRight_add (κ η : kernel α β) :
+    prodMkRight γ (κ + η) = prodMkRight γ κ + prodMkRight γ η := by ext; simp
+
 theorem lintegral_prodMkLeft (κ : kernel α β) (ca : γ × α) (g : β → ℝ≥0∞) :
     ∫⁻ b, g b ∂prodMkLeft γ κ ca = ∫⁻ b, g b ∂κ ca.snd := rfl
 #align probability_theory.kernel.lintegral_prod_mk_left ProbabilityTheory.kernel.lintegral_prodMkLeft

Mathlib/Probability/Kernel/MeasureCompProd.lean

@@ -48,13 +48,34 @@ lemma compProd_apply [SFinite μ] [IsSFiniteKernel κ] {s : Set (α × β)} (hs
   simp_rw [compProd, kernel.compProd_apply _ _ _ hs, kernel.const_apply, kernel.prodMkLeft_apply']
   rfl
 
+lemma compProd_apply_prod [SFinite μ] [IsSFiniteKernel κ]
+    {s : Set α} {t : Set β} (hs : MeasurableSet s) (ht : MeasurableSet t) :
+    (μ ⊗ₘ κ) (s ×ˢ t) = ∫⁻ a in s, κ a t ∂μ := by
+  rw [compProd_apply (hs.prod ht), ← lintegral_indicator _ hs]
+  congr with a
+  classical
+  rw [Set.indicator_apply]
+  split_ifs with ha <;> simp [ha]
+
 lemma compProd_congr [SFinite μ] [IsSFiniteKernel κ] [IsSFiniteKernel η]
     (h : κ =ᵐ[μ] η) : μ ⊗ₘ κ = μ ⊗ₘ η := by
   ext s hs
   have : (fun a ↦ κ a (Prod.mk a ⁻¹' s)) =ᵐ[μ] fun a ↦ η a (Prod.mk a ⁻¹' s) := by
     filter_upwards [h] with a ha using by rw [ha]
   rw [compProd_apply hs, lintegral_congr_ae this, compProd_apply hs]
 
+lemma compProd_add_left (μ ν : Measure α) [SFinite μ] [SFinite ν] (κ : kernel α β)
+    [IsSFiniteKernel κ] :
+    (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ := by
+  rw [Measure.compProd, kernel.const_add, kernel.compProd_add_left]; rfl
+
+lemma compProd_add_right (μ : Measure α) [SFinite μ] (κ η : kernel α β)
+    [IsSFiniteKernel κ] [IsSFiniteKernel η] :
+    μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η := by
+  rw [Measure.compProd, kernel.prodMkLeft_add, kernel.compProd_add_right]; rfl
+
+section Integral
+
 lemma lintegral_compProd [SFinite μ] [IsSFiniteKernel κ]
     {f : α × β → ℝ≥0∞} (hf : Measurable f) :
     ∫⁻ x, f x ∂(μ ⊗ₘ κ) = ∫⁻ a, ∫⁻ b, f (a, b) ∂(κ a) ∂μ := by
@@ -91,6 +112,8 @@ lemma set_integral_compProd [SFinite μ] [IsSFiniteKernel κ] {E : Type*}
   rw [compProd, ProbabilityTheory.set_integral_compProd hs ht hf]
   simp
 
+end Integral
+
 lemma dirac_compProd_apply [MeasurableSingletonClass α] {a : α} [IsSFiniteKernel κ]
     {s : Set (α × β)} (hs : MeasurableSet s) :
     (Measure.dirac a ⊗ₘ κ) s = κ a (Prod.mk a ⁻¹' s) := by