rnDeriv_lt_top — Mathlib

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

Похожие утверждения