Proper kernels #
We define the notion of properness for measure kernels and highlight important consequences.
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)
: