feat(Probability/Kernel/Basic): Evaluation function of a finite kerne…

…l is integrable (#6111)

Co-authored-by: JasonKYi <kexing.ying19@imperial.ac.uk>

Mathlib/Probability/Kernel/Basic.lean

@@ -210,6 +210,21 @@ protected theorem measurable_coe (κ : kernel α β) {s : Set β} (hs : Measurab
   (Measure.measurable_coe hs).comp (kernel.measurable κ)
 #align probability_theory.kernel.measurable_coe ProbabilityTheory.kernel.measurable_coe
 
+lemma IsFiniteKernel.integrable (μ : Measure α) [IsFiniteMeasure μ]
+    (κ : kernel α β) [IsFiniteKernel κ] {s : Set β} (hs : MeasurableSet s) :
+    Integrable (fun x => (κ x s).toReal) μ := by
+  refine' Integrable.mono' (integrable_const (IsFiniteKernel.bound κ).toReal)
+    ((kernel.measurable_coe κ hs).ennreal_toReal.aestronglyMeasurable)
+    (ae_of_all μ <| fun x => _)
+  rw [Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg,
+    ENNReal.toReal_le_toReal (measure_ne_top _ _) (IsFiniteKernel.bound_ne_top _)]
+  exact kernel.measure_le_bound _ _ _
+
+lemma IsMarkovKernel.integrable (μ : Measure α) [IsFiniteMeasure μ]
+    (κ : kernel α β) [IsMarkovKernel κ] {s : Set β} (hs : MeasurableSet s) :
+    Integrable (fun x => (κ x s).toReal) μ :=
+  IsFiniteKernel.integrable μ κ hs
+
 section Sum
 
 /-- Sum of an indexed family of kernels. -/