English
Let s be a set with μ(s) ≠ ∞. Then the integral of μ.rnDer ν over s with respect to ν is finite: ∫_s (μ.rnDer ν) dν < ∞.
Русский
Пусть s — множество с такими свойствами, что μ(s) ≠ ∞. Тогда интеграл производной радона-немера μ по отношению к ν над s по мере ν конечен: ∫_s (μ.rnDer ν) dν < ∞.
LaTeX
$$$\\text{If } μ(s) \\neq \\infty,\\quad \\int\\!_{s} (μ\\mathrm{rnDer}\\nu)(x)\\,dν(x) < \\infty$$$
Lean4
theorem lintegral_rnDeriv_lt_top_of_measure_ne_top (ν : Measure α) {s : Set α} (hs : μ s ≠ ∞) :
∫⁻ x in s, μ.rnDeriv ν x ∂ν < ∞ :=
by
by_cases hl : HaveLebesgueDecomposition μ ν
· suffices (∫⁻ x in toMeasurable μ s, μ.rnDeriv ν x ∂ν) < ∞ from
lt_of_le_of_lt (lintegral_mono_set (subset_toMeasurable _ _)) this
rw [← withDensity_apply _ (measurableSet_toMeasurable _ _)]
calc
_ ≤ (singularPart μ ν) (toMeasurable μ s) + _ := le_add_self
_ = μ s := by rw [← Measure.add_apply, ← haveLebesgueDecomposition_add, measure_toMeasurable]
_ < ⊤ := hs.lt_top
· simp only [Measure.rnDeriv, dif_neg hl, Pi.zero_apply, lintegral_zero, ENNReal.zero_lt_top]
