Integral against a kernel over a set

This file contains lemmas about the integral against a kernel and over a set.

theorem ProbabilityTheory.Kernel.integral_integral_indicator {X : Type u_1} {Y : Type u_2} {E : Type u_3} {mX : MeasurableSpace X} {mY : MeasurableSpace Y} [NormedAddCommGroup E] [NormedSpace ℝ E] (κ : Kernel X Y) (μ : MeasureTheory.Measure X) (f : X → Y → E) {s : Set X} (hs : MeasurableSet s) : ∫ (x : X), ∫ (y : Y), s.indicator (fun (x : X) => f x y) x ∂κ x ∂μ = ∫ (x : X) in s, ∫ (y : Y), f x y ∂κ x ∂μ