English
If μ is finite and μ ≪ ν with ν σ-finite, then the ν-integral of the real-valued RN-derivative of μ with respect to ν equals the total ν-mass of μ minus the ν-mass of the singular part of μ with respect to ν.
Русский
Если μ конечна и μ ≪ ν при ν σ–конечной, то интеграл по ν от вещественного RN-дериватива μ по ν равен общей массе μ минус массу сингулярной части μ по ν.
LaTeX
$$$$ \int x\, (\mu.rnDeriv ν x)^{\mathrm{toReal}} \, dν = \mu.\mathrm{real}(\mathrm{Set.univ}) - (\mu.singularPart ν).\mathrm{real}(\mathrm{Set.univ}) $$$$
Lean4
theorem integral_toReal_rnDeriv' [IsFiniteMeasure μ] [SigmaFinite ν] :
∫ x, (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ - (μ.singularPart ν).real Set.univ := by
rw [measureReal_def, measureReal_def, ← ENNReal.toReal_sub_of_le (μ.singularPart_le ν Set.univ) (measure_ne_top _ _),
← Measure.sub_apply .univ (Measure.singularPart_le μ ν), Measure.measure_sub_singularPart, ← measureReal_def, ←
Measure.setIntegral_toReal_rnDeriv_eq_withDensity, setIntegral_univ]
