English
If κ is a finite kernel and f is bounded by B, then κ.withDensity f is finite.
Русский
Если κ является конечным ядром и f ограничен сверху константой B, то κ.withDensity f является конечным ядром.
LaTeX
$$$ \text{IsFiniteKernel}(\kappa) \Rightarrow \text{IsFiniteKernel}(\kappa^{\}\!f) \,\text{provided } f \le B < \infty $$$
Lean4
/-- If a kernel `κ` is finite and a function `f : α → β → ℝ≥0∞` is bounded, then `withDensity κ f`
is finite. -/
theorem isFiniteKernel_withDensity_of_bounded (κ : Kernel α β) [IsFiniteKernel κ] {B : ℝ≥0∞} (hB_top : B ≠ ∞)
(hf_B : ∀ a b, f a b ≤ B) : IsFiniteKernel (withDensity κ f) :=
by
by_cases hf : Measurable (Function.uncurry f)
·
exact
⟨⟨B * κ.bound, ENNReal.mul_lt_top hB_top.lt_top κ.bound_lt_top, fun a =>
by
rw [Kernel.withDensity_apply' κ hf a Set.univ]
calc
∫⁻ b in Set.univ, f a b ∂κ a ≤ ∫⁻ _ in Set.univ, B ∂κ a := lintegral_mono (hf_B a)
_ = B * κ a Set.univ := by simp only [Measure.restrict_univ, MeasureTheory.lintegral_const]
_ ≤ B * κ.bound := mul_le_mul_left' (measure_le_bound κ a Set.univ) _⟩⟩
· rw [withDensity_of_not_measurable _ hf]
infer_instance
