Proper kernels

We define the notion of properness for measure kernels and highlight important consequences.

theorem ProbabilityTheory.Kernel.IsProper.ae_eq_const {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : Kernel X X} (hπ : π.IsProper) (h𝓑𝓧 : 𝓑 ≤ 𝓧) {Y : Type u_2} [MeasurableSpace Y] [MeasurableSingletonClass Y] {g : X → Y} (hg : Measurable g) (x₀ : X) : ∀ᵐ (x : X) ∂π x₀, g x = g x₀

theorem ProbabilityTheory.Kernel.IsProper.integral_bdd_mul {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : Kernel X X} {f g : X → ℝ} {x₀ : X} [IsFiniteKernel π] (h𝓑𝓧 : 𝓑 ≤ 𝓧) (hπ : π.IsProper) (hf : MeasureTheory.Integrable f (π x₀)) (hg : MeasureTheory.StronglyMeasurable g) (hgbdd : ∃ C > 0, ∀ (x : X), ‖g x‖ ≤ C) : ∫ (x : X), g x * f x ∂π x₀ = g x₀ * ∫ (x : X), f x ∂π x₀