English
Variant: for measurable s and HaveLebesgueDecomposition, the real-valued ν-integral of μ.rnDeriv ν over s equals μ.real s.
Русский
Вариант: для измеримого множества s и HaveLebesgueDecomposition, реальный ν-интеграл μ.rnDeriv ν по s равен μ.real s.
LaTeX
$$$\\int_{s} (μ.rnDeriv ν(x))^{\\toReal} dν(x) = μ.real(s)$$$
Lean4
theorem setIntegral_toReal_rnDeriv_le [SigmaFinite μ] {s : Set α} (hμs : μ s ≠ ∞) :
∫ x in s, (μ.rnDeriv ν x).toReal ∂ν ≤ μ.real s :=
by
set t := toMeasurable μ s with ht
have ht_m : MeasurableSet t := measurableSet_toMeasurable μ s
have hμt : μ t ≠ ∞ := by rwa [ht, measure_toMeasurable s]
calc
∫ x in s, (μ.rnDeriv ν x).toReal ∂ν ≤ ∫ x in t, (μ.rnDeriv ν x).toReal ∂ν :=
by
refine setIntegral_mono_set ?_ ?_ (HasSubset.Subset.eventuallyLE (subset_toMeasurable _ _))
· exact integrableOn_toReal_rnDeriv hμt
· exact ae_of_all _ (by simp)
_ = (withDensity ν (rnDeriv μ ν)).real t := (setIntegral_toReal_rnDeriv_eq_withDensity' ht_m)
_ ≤ μ.real t := by
simp only [measureReal_def]
gcongr
· exact hμt
· apply withDensity_rnDeriv_le
_ = μ.real s := by rw [measureReal_def, measureReal_def, measure_toMeasurable s]
