English
For finite kernels κ and η and any a, rnDeriv κ η a x is finite almost everywhere with respect to η a; more precisely rnDeriv κ η a x < ∞ almost everywhere.
Русский
Для конечных ядер κ и η и любого a, rnDeriv κ η a x ограничена сверху почти всюду по η a; то есть rnDeriv κ η a x < ∞ почти всюду.
LaTeX
$$∀ᵐ x ∂(η a), rnDeriv κ η a x < ∞$$
Lean4
theorem rnDeriv_lt_top (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} :
∀ᵐ x ∂(η a), rnDeriv κ η a x < ∞ := by
filter_upwards [κ.rnDeriv_eq_rnDeriv_measure, (κ a).rnDeriv_ne_top _] with x heq htop using heq ▸ htop.lt_top