English
For f: α → ENNReal that is almost everywhere measurable, the real-valued density μ.withDensityᵥ f corresponds to the signed measure of μ.withDensity f via the real-part extraction.
Русский
Для f: α → ENNReal, измеримой almost everywhere, плотность μ.withDensityᵥ f соответствует знаковой мере μ.withDensity f через извлечение вещественной части.
LaTeX
$$$(\mu.withDensityᵥ (f)).toReal = (\mu.withDensity f).toSignedMeasure$$
Lean4
theorem withDensityᵥ_toReal {f : α → ℝ≥0∞} (hfm : AEMeasurable f μ) (hf : (∫⁻ x, f x ∂μ) ≠ ∞) :
(μ.withDensityᵥ fun x => (f x).toReal) = @toSignedMeasure α _ (μ.withDensity f) (isFiniteMeasure_withDensity hf) :=
by
have hfi := integrable_toReal_of_lintegral_ne_top hfm hf
haveI := isFiniteMeasure_withDensity hf
ext i hi
rw [withDensityᵥ_apply hfi hi, toSignedMeasure_apply_measurable hi, measureReal_def, withDensity_apply _ hi,
integral_toReal hfm.restrict]
refine ae_lt_top' hfm.restrict (ne_top_of_le_ne_top hf ?_)
conv_rhs => rw [← setLIntegral_univ]
exact lintegral_mono_set (Set.subset_univ _)
