lintegral_rnDeriv_lt_top — Mathlib

English

If μ is finite, then the Radon–Nikodym derivative μ.rnDer ν is finite almost everywhere with respect to ν: ∫⁻ (μ.rnDer ν) dν < ∞ and in particular μ.rnDer ν < ∞ ν-a.e.

Русский

Если μ конечна, то радионовский производный μ по ν конечен почти всюду относительно ν: μ.rnDer ν < ∞ ν-a.e.

LaTeX

$$$\\forall \\text{finite } μ:\\quad ∀ᵐ x\\,∂ν:\\; μ\\mathrm{rnDer}\\nu(x) < \\infty$$$

Lean4

theorem lintegral_rnDeriv_lt_top (μ ν : Measure α) [IsFiniteMeasure μ] : ∫⁻ x, μ.rnDeriv ν x ∂ν < ∞ :=
  by
  rw [← setLIntegral_univ]
  exact lintegral_rnDeriv_lt_top_of_measure_ne_top _ (measure_lt_top _ _).ne

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