feat: integral against the composition of kernels (#22363)

Prove the formula for the integral against the composition of kernels. This is a simplified version of the proof for the composition-product which is in the same file. However we need to do all the proofs again because the results about composition-product require s-finiteness while composition do not.



Co-authored-by: EtienneC30 <66847262+EtienneC30@users.noreply.github.com>

Author: EtienneC30

Mathlib/Probability/Kernel/Composition/Basic.lean

@@ -1401,6 +1401,15 @@ lemma snd_comp (κ : Kernel α β) (η : Kernel β (γ × δ)) : (η ∘ₖ κ).
   · rfl
   · exact measurable_snd hs
 
+lemma comp_add_right (μ κ : Kernel α β) (η : Kernel β γ) :
+    η ∘ₖ (μ + κ) = η ∘ₖ μ + η ∘ₖ κ := by ext _ _ hs; simp [comp_apply' _ _ _ hs]
+
+lemma comp_add_left (μ : Kernel α β) (κ η : Kernel β γ) :
+    (κ + η) ∘ₖ μ = κ ∘ₖ μ + η ∘ₖ μ := by
+  ext a s hs
+  simp_rw [comp_apply' _ _ _ hs, add_apply, Measure.add_apply, comp_apply' _ _ _ hs,
+    lintegral_add_left (Kernel.measurable_coe κ hs)]
+
 end Comp
 
 section Prod

Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean

@@ -1,33 +1,47 @@
 /-
 Copyright (c) 2023 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Rémy Degenne
+Authors: Rémy Degenne, Etienne Marion
 -/
 import Mathlib.Probability.Kernel.Composition.Basic
 import Mathlib.Probability.Kernel.MeasurableIntegral
 
 /-!
-# Bochner integral of a function against the composition-product of two kernels
+# Bochner integral of a function against the composition and the composition-products of two kernels
 
-We prove properties of the composition-product of two kernels. If `κ` is an s-finite kernel from
-`α` to `β` and `η` is an s-finite kernel from `α × β` to `γ`, we can form their composition-product
-`κ ⊗ₖ η : Kernel α (β × γ)`. We proved in `ProbabilityTheory.Kernel.lintegral_compProd` that it
+We prove properties of the composition and the composition-product of two kernels.
+
+If `κ` is a kernel from `α` to `β` and `η` is a kernel from `β` to `γ`, we can form their
+composition `η ∘ₖ κ : Kernel α γ`. We proved in `ProbabilityTheory.Kernel.lintegral_comp` that it
+verifies `∫⁻ c, f c ∂((η ∘ₖ κ) a) = ∫⁻ b, ∫⁻ c, f c ∂(η b) ∂(κ a)`. In this file, we
+prove the same equality for the Bochner integral.
+
+If `κ` is an s-finite kernel from `α` to `β` and `η` is an s-finite kernel from `α × β` to `γ`,
+we can form their composition-product `κ ⊗ₖ η : Kernel α (β × γ)`.
+We proved in `ProbabilityTheory.Kernel.lintegral_compProd` that it
 verifies `∫⁻ bc, f bc ∂((κ ⊗ₖ η) a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a)`. In this file, we
 prove the same equality for the Bochner integral.
 
 ## Main statements
 
 * `ProbabilityTheory.integral_compProd`: the integral against the composition-product is
-  `∫ z, f z ∂((κ ⊗ₖ η) a) = ∫ x, ∫ y, f (x, y) ∂(η (a, x)) ∂(κ a)`
+  `∫ z, f z ∂((κ ⊗ₖ η) a) = ∫ x, ∫ y, f (x, y) ∂(η (a, x)) ∂(κ a)`.
+
+* `ProbabilityTheory.integral_comp`: the integral against the composition is
+  `∫⁻ z, f z ∂((η ∘ₖ κ) a) = ∫⁻ x, ∫⁻ y, f y ∂(η x) ∂(κ a)`.
 
 ## Implementation details
 
-This file is to a large extent a copy of part of
-`Mathlib/MeasureTheory/Constructions/Prod/Basic.lean`. The product of
-two measures is a particular case of composition-product of kernels and it turns out that once the
-measurablity of the Lebesgue integral of a kernel is proved, almost all proofs about integrals
-against products of measures extend with minimal modifications to the composition-product of two
-kernels.
+This file is to a large extent a copy of part of `Mathlib/MeasureTheory/Integral/Prod.lean`.
+The product of two measures is a particular case of composition-product of kernels and
+it turns out that once the measurablity of the Lebesgue integral of a kernel is proved,
+almost all proofs about integrals against products of measures extend with minimal modifications
+to the composition-product of two kernels.
+
+The composition of kernels can also be expressed easily with the composition-product and therefore
+the proofs about the composition are only simplified versions of the ones for the
+composition-product. However it is necessary to do all the proofs once again because the
+composition-product requires s-finiteness while the composition does not.
 -/
 
 
@@ -37,11 +51,14 @@ open Set Function Real ENNReal MeasureTheory Filter ProbabilityTheory Probabilit
 open scoped Topology ENNReal MeasureTheory
 
 variable {α β γ E : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
-  {mγ : MeasurableSpace γ} [NormedAddCommGroup E] {κ : Kernel α β} [IsSFiniteKernel κ]
-  {η : Kernel (α × β) γ} [IsSFiniteKernel η] {a : α}
+  {mγ : MeasurableSpace γ} [NormedAddCommGroup E] {a : α}
 
 namespace ProbabilityTheory
 
+section compProd
+
+variable {κ : Kernel α β} [IsSFiniteKernel κ] {η : Kernel (α × β) γ} [IsSFiniteKernel η]
+
 theorem hasFiniteIntegral_prod_mk_left (a : α) {s : Set (β × γ)} (h2s : (κ ⊗ₖ η) a s ≠ ∞) :
     HasFiniteIntegral (fun b => (η (a, b) (Prod.mk b ⁻¹' s)).toReal) (κ a) := by
   let t := toMeasurable ((κ ⊗ₖ η) a) s
@@ -118,10 +135,14 @@ theorem integrable_compProd_iff ⦃f : β × γ → E⦄ (hf : AEStronglyMeasura
   simp only [Integrable, hasFiniteIntegral_compProd_iff' hf, hf.norm.integral_kernel_compProd,
     hf, hf.compProd_mk_left, eventually_and, true_and]
 
-theorem _root_.MeasureTheory.Integrable.compProd_mk_left_ae ⦃f : β × γ → E⦄
+theorem _root_.MeasureTheory.Integrable.ae_of_compProd ⦃f : β × γ → E⦄
     (hf : Integrable f ((κ ⊗ₖ η) a)) : ∀ᵐ x ∂κ a, Integrable (fun y => f (x, y)) (η (a, x)) :=
   ((integrable_compProd_iff hf.aestronglyMeasurable).mp hf).1
 
+@[deprecated (since := "2025-02-28")]
+alias _root_.MeasureTheory.Integrable.compProd_mk_left_ae :=
+  _root_.MeasureTheory.Integrable.ae_of_compProd
+
 theorem _root_.MeasureTheory.Integrable.integral_norm_compProd ⦃f : β × γ → E⦄
     (hf : Integrable f ((κ ⊗ₖ η) a)) : Integrable (fun x => ∫ y, ‖f (x, y)‖ ∂η (a, x)) (κ a) :=
   ((integrable_compProd_iff hf.aestronglyMeasurable).mp hf).2
@@ -146,23 +167,23 @@ theorem Kernel.integral_fn_integral_add ⦃f g : β × γ → E⦄ (F : E → E'
     ∫ x, F (∫ y, f (x, y) + g (x, y) ∂η (a, x)) ∂κ a =
       ∫ x, F (∫ y, f (x, y) ∂η (a, x) + ∫ y, g (x, y) ∂η (a, x)) ∂κ a := by
   refine integral_congr_ae ?_
-  filter_upwards [hf.compProd_mk_left_ae, hg.compProd_mk_left_ae] with _ h2f h2g
+  filter_upwards [hf.ae_of_compProd, hg.ae_of_compProd] with _ h2f h2g
   simp [integral_add h2f h2g]
 
 theorem Kernel.integral_fn_integral_sub ⦃f g : β × γ → E⦄ (F : E → E')
     (hf : Integrable f ((κ ⊗ₖ η) a)) (hg : Integrable g ((κ ⊗ₖ η) a)) :
     ∫ x, F (∫ y, f (x, y) - g (x, y) ∂η (a, x)) ∂κ a =
       ∫ x, F (∫ y, f (x, y) ∂η (a, x) - ∫ y, g (x, y) ∂η (a, x)) ∂κ a := by
   refine integral_congr_ae ?_
-  filter_upwards [hf.compProd_mk_left_ae, hg.compProd_mk_left_ae] with _ h2f h2g
+  filter_upwards [hf.ae_of_compProd, hg.ae_of_compProd] with _ h2f h2g
   simp [integral_sub h2f h2g]
 
 theorem Kernel.lintegral_fn_integral_sub ⦃f g : β × γ → E⦄ (F : E → ℝ≥0∞)
     (hf : Integrable f ((κ ⊗ₖ η) a)) (hg : Integrable g ((κ ⊗ₖ η) a)) :
     ∫⁻ x, F (∫ y, f (x, y) - g (x, y) ∂η (a, x)) ∂κ a =
       ∫⁻ x, F (∫ y, f (x, y) ∂η (a, x) - ∫ y, g (x, y) ∂η (a, x)) ∂κ a := by
   refine lintegral_congr_ae ?_
-  filter_upwards [hf.compProd_mk_left_ae, hg.compProd_mk_left_ae] with _ h2f h2g
+  filter_upwards [hf.ae_of_compProd, hg.ae_of_compProd] with _ h2f h2g
   simp [integral_sub h2f h2g]
 
 theorem Kernel.integral_integral_add ⦃f g : β × γ → E⦄ (hf : Integrable f ((κ ⊗ₖ η) a))
@@ -261,4 +282,162 @@ theorem setIntegral_compProd_univ_left (f : β × γ → E) {t : Set γ} (ht : M
     ∫ z in univ ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫ x, ∫ y in t, f (x, y) ∂η (a, x) ∂κ a := by
   simp_rw [setIntegral_compProd MeasurableSet.univ ht hf, Measure.restrict_univ]
 
+end compProd
+
+section comp
+
+variable {κ : Kernel α β} {η : Kernel β γ}
+
+theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_kernel_comp [NormedSpace ℝ E]
+    ⦃f : γ → E⦄ (hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)) :
+    AEStronglyMeasurable (fun x ↦ ∫ y, f y ∂η x) (κ a) :=
+  ⟨fun x ↦ ∫ y, hf.mk f y ∂η x, hf.stronglyMeasurable_mk.integral_kernel, by
+    filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk] with _ hx using integral_congr_ae hx⟩
+
+theorem _root_.MeasureTheory.AEStronglyMeasurable.comp {δ : Type*} [TopologicalSpace δ]
+    {f : γ → δ} (hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)) :
+    ∀ᵐ x ∂κ a, AEStronglyMeasurable f (η x) := by
+  filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk] with x hx using
+    ⟨hf.mk f, hf.stronglyMeasurable_mk, hx⟩
+
+/-! ### Integrability with respect to composition -/
+
+theorem hasFiniteIntegral_comp_iff ⦃f : γ → E⦄ (hf : StronglyMeasurable f) :
+    HasFiniteIntegral f ((η ∘ₖ κ) a) ↔
+    (∀ᵐ x ∂κ a, HasFiniteIntegral f (η x)) ∧ HasFiniteIntegral (fun x ↦ ∫ y, ‖f y‖ ∂η x) (κ a) := by
+  simp_rw [hasFiniteIntegral_iff_enorm, lintegral_comp _ _ _ hf.enorm]
+  simp_rw [integral_eq_lintegral_of_nonneg_ae (ae_of_all _ fun y ↦ norm_nonneg _)
+      hf.norm.aestronglyMeasurable, enorm_eq_ofReal toReal_nonneg, ofReal_norm_eq_enorm]
+  have : ∀ {p q r : Prop} (_ : r → p), (r ↔ p ∧ q) ↔ p → (r ↔ q) := fun h ↦ by
+    rw [← and_congr_right_iff, and_iff_right_of_imp h]
+  rw [this]
+  · intro h
+    rw [lintegral_congr_ae]
+    filter_upwards [h] with x hx
+    rw [ofReal_toReal]
+    rwa [← lt_top_iff_ne_top]
+  · exact fun h ↦ ae_lt_top hf.enorm.lintegral_kernel h.ne
+
+theorem hasFiniteIntegral_comp_iff' ⦃f : γ → E⦄ (hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)) :
+    HasFiniteIntegral f ((η ∘ₖ κ) a) ↔
+    (∀ᵐ x ∂κ a, HasFiniteIntegral f (η x)) ∧ HasFiniteIntegral (fun x ↦ ∫ y, ‖f y‖ ∂η x) (κ a) := by
+  rw [hasFiniteIntegral_congr hf.ae_eq_mk, hasFiniteIntegral_comp_iff hf.stronglyMeasurable_mk]
+  refine and_congr (eventually_congr ?_) (hasFiniteIntegral_congr ?_)
+  · filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk.symm] with _ hx using
+      hasFiniteIntegral_congr hx
+  · filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk.symm] with _ hx using
+      integral_congr_ae (EventuallyEq.fun_comp hx _)
+
+theorem integrable_comp_iff ⦃f : γ → E⦄ (hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)) :
+    Integrable f ((η ∘ₖ κ) a) ↔
+    (∀ᵐ y ∂κ a, Integrable f (η y)) ∧ Integrable (fun y ↦ ∫ z, ‖f z‖ ∂η y) (κ a) := by
+  simp only [Integrable, hf, hasFiniteIntegral_comp_iff' hf, true_and, eventually_and, hf.comp,
+    hf.norm.integral_kernel_comp]
+
+theorem _root_.MeasureTheory.Integrable.ae_of_comp ⦃f : γ → E⦄ (hf : Integrable f ((η ∘ₖ κ) a)) :
+    ∀ᵐ x ∂κ a, Integrable f (η x) := ((integrable_comp_iff hf.1).1 hf).1
+
+theorem _root_.MeasureTheory.Integrable.integral_norm_comp ⦃f : γ → E⦄
+    (hf : Integrable f ((η ∘ₖ κ) a)) : Integrable (fun x ↦ ∫ y, ‖f y‖ ∂η x) (κ a) :=
+  ((integrable_comp_iff hf.1).1 hf).2
+
+theorem _root_.MeasureTheory.Integrable.integral_comp [NormedSpace ℝ E] ⦃f : γ → E⦄
+    (hf : Integrable f ((η ∘ₖ κ) a)) : Integrable (fun x ↦ ∫ y, f y ∂η x) (κ a) :=
+  Integrable.mono hf.integral_norm_comp hf.1.integral_kernel_comp <|
+    ae_of_all _ fun _ ↦ (norm_integral_le_integral_norm _).trans_eq
+    (norm_of_nonneg <| integral_nonneg_of_ae <| ae_of_all _ fun _ ↦ norm_nonneg _).symm
+
+/-! ### Bochner integral with respect to the composition -/
+
+variable [NormedSpace ℝ E] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E']
+
+namespace Kernel
+
+theorem integral_fn_integral_add_comp ⦃f g : γ → E⦄ (F : E → E')
+    (hf : Integrable f ((η ∘ₖ κ) a)) (hg : Integrable g ((η ∘ₖ κ) a)) :
+    ∫ x, F (∫ y, f y + g y ∂η x) ∂κ a = ∫ x, F (∫ y, f y ∂η x + ∫ y, g y ∂η x) ∂κ a := by
+  refine integral_congr_ae ?_
+  filter_upwards [hf.ae_of_comp, hg.ae_of_comp] with _ h2f h2g
+  simp [integral_add h2f h2g]
+
+theorem integral_fn_integral_sub_comp ⦃f g : γ → E⦄ (F : E → E')
+    (hf : Integrable f ((η ∘ₖ κ) a)) (hg : Integrable g ((η ∘ₖ κ) a)) :
+    ∫ x, F (∫ y, f y - g y ∂η x) ∂κ a = ∫ x, F (∫ y, f y ∂η x - ∫ y, g y ∂η x) ∂κ a := by
+  refine integral_congr_ae ?_
+  filter_upwards [hf.ae_of_comp, hg.ae_of_comp] with _ h2f h2g
+  simp [integral_sub h2f h2g]
+
+theorem lintegral_fn_integral_sub_comp ⦃f g : γ → E⦄ (F : E → ℝ≥0∞)
+    (hf : Integrable f ((η ∘ₖ κ) a)) (hg : Integrable g ((η ∘ₖ κ) a)) :
+    ∫⁻ x, F (∫ y, f y - g y ∂η x) ∂κ a = ∫⁻ x, F (∫ y, f y ∂η x - ∫ y, g y ∂η x) ∂κ a := by
+  refine lintegral_congr_ae ?_
+  filter_upwards [hf.ae_of_comp, hg.ae_of_comp] with _ h2f h2g
+  simp [integral_sub h2f h2g]
+
+theorem integral_integral_add_comp ⦃f g : γ → E⦄ (hf : Integrable f ((η ∘ₖ κ) a))
+    (hg : Integrable g ((η ∘ₖ κ) a)) :
+    ∫ x, ∫ y, f y + g y ∂η x ∂κ a = ∫ x, ∫ y, f y ∂η x ∂κ a + ∫ x, ∫ y, g y ∂η x ∂κ a :=
+  (integral_fn_integral_add_comp id hf hg).trans <| integral_add hf.integral_comp hg.integral_comp
+
+theorem integral_integral_add'_comp ⦃f g : γ → E⦄ (hf : Integrable f ((η ∘ₖ κ) a))
+    (hg : Integrable g ((η ∘ₖ κ) a)) :
+    ∫ x, ∫ y, (f + g) y ∂η x ∂κ a = ∫ x, ∫ y, f y ∂η x ∂κ a + ∫ x, ∫ y, g y ∂η x ∂κ a :=
+  integral_integral_add_comp hf hg
+
+theorem integral_integral_sub_comp ⦃f g : γ → E⦄ (hf : Integrable f ((η ∘ₖ κ) a))
+    (hg : Integrable g ((η ∘ₖ κ) a)) :
+    ∫ x, ∫ y, f y - g y ∂η x ∂κ a = ∫ x, ∫ y, f y ∂η x ∂κ a - ∫ x, ∫ y, g y ∂η x ∂κ a :=
+  (integral_fn_integral_sub_comp id hf hg).trans <| integral_sub hf.integral_comp hg.integral_comp
+
+theorem integral_integral_sub'_comp ⦃f g : γ → E⦄ (hf : Integrable f ((η ∘ₖ κ) a))
+    (hg : Integrable g ((η ∘ₖ κ) a)) :
+    ∫ x, ∫ y, (f - g) y ∂η x ∂κ a = ∫ x, ∫ y, f y ∂η x ∂κ a - ∫ x, ∫ y, g y ∂η x ∂κ a :=
+  integral_integral_sub_comp hf hg
+
+theorem continuous_integral_integral_comp :
+    Continuous fun f : γ →₁[(η ∘ₖ κ) a] E ↦ ∫ x, ∫ y, f y ∂η x ∂κ a := by
+  refine continuous_iff_continuousAt.2 fun g ↦ ?_
+  refine tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_comp
+      (Eventually.of_forall fun h ↦ (L1.integrable_coeFn h).integral_comp) ?_
+  simp_rw [← lintegral_fn_integral_sub_comp (‖·‖ₑ) (L1.integrable_coeFn _) (L1.integrable_coeFn g)]
+  refine tendsto_of_tendsto_of_tendsto_of_le_of_le
+    (h := fun i ↦ ∫⁻ x, ∫⁻ y, ‖i y - g y‖ₑ ∂η x ∂κ a)
+    tendsto_const_nhds ?_ (fun _ ↦ zero_le _) ?_
+  swap; · exact fun _ ↦ lintegral_mono fun _ ↦ enorm_integral_le_lintegral_enorm _
+  have (i : γ →₁[(η ∘ₖ κ) a] E) : Measurable fun z ↦ ‖i z - g z‖ₑ :=
+    ((Lp.stronglyMeasurable i).sub (Lp.stronglyMeasurable g)).enorm
+  simp_rw [← lintegral_comp _ _ _ (this _), ← L1.ofReal_norm_sub_eq_lintegral, ← ofReal_zero]
+  exact (continuous_ofReal.tendsto 0).comp (tendsto_iff_norm_sub_tendsto_zero.1 tendsto_id)
+
+theorem integral_comp : ∀ {f : γ → E} (_ : Integrable f ((η ∘ₖ κ) a)),
+    ∫ z, f z ∂(η ∘ₖ κ) a = ∫ x, ∫ y, f y ∂η x ∂κ a := by
+  by_cases hE : CompleteSpace E; swap
+  · simp [integral, hE]
+  apply Integrable.induction
+  · intro c s hs ms
+    simp_rw [integral_indicator hs, MeasureTheory.setIntegral_const, integral_smul_const]
+    congr
+    rw [integral_toReal, Kernel.comp_apply' _ _ _ hs]
+    · exact (Kernel.measurable_coe _ hs).aemeasurable
+    · exact ae_lt_top_of_comp_ne_top a ms.ne
+  · rintro f g - i_f i_g hf hg
+    simp_rw [integral_add' i_f i_g, integral_integral_add'_comp i_f i_g, hf, hg]
+  · exact isClosed_eq continuous_integral Kernel.continuous_integral_integral_comp
+  · rintro f g hfg - hf
+    convert hf using 1
+    · exact integral_congr_ae hfg.symm
+    · apply integral_congr_ae
+      filter_upwards [ae_ae_of_ae_comp hfg] with x hfgx using integral_congr_ae (ae_eq_symm hfgx)
+
+theorem setIntegral_comp {f : γ → E} {s : Set γ} (hs : MeasurableSet s)
+    (hf : IntegrableOn f s ((η ∘ₖ κ) a)) :
+    ∫ z in s, f z ∂(η ∘ₖ κ) a = ∫ x, ∫ y in s, f y ∂η x ∂κ a := by
+  rw [← restrict_apply (η ∘ₖ κ) hs, ← comp_restrict hs, integral_comp]
+  · simp_rw [restrict_apply]
+  · rwa [comp_restrict, restrict_apply]
+
+end Kernel
+
+end comp
+
 end ProbabilityTheory