Theorems · Theorem · probability

ProbabilityTheory.Kernel.isFiniteKernel_withDensity_of_bounded

∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal}
  (κ : ProbabilityTheory.Kernel α β) [inst : ProbabilityTheory.IsFiniteKernel κ] {B : ENNReal},
  B ≠ ⊤ → (∀ (a : α) (b : β), f a b ≤ B) → ProbabilityTheory.IsFiniteKernel (κ.withDensity f)

If a kernel κ is finite and a function f : α → β → ℝ≥0∞ is bounded, then withDensity κ f is finite.

Defined in

Mathlib.Probability.Kernel.WithDensity

Cited by

0 results in Mathlib

Foundations

Depth 212 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

ProbabilityTheory.IsFiniteKernel