English
If s is a signed measure and μ a measure with Lebesgue decomposition μ, and s ≪ᵥ μ, then μ.withDensityᵥ (s.rnDeriv μ) = s.
Русский
Если s — знаковая мера и μ — мера с разложением Лебега, и s абсолютно непрерывна относительно μ, то density-вес μ с rnDeriv μ совпадает с s.
LaTeX
$$$ μ.withDensityᵥ (s.rnDeriv μ) = s $$$
Lean4
theorem withDensityᵥ_rnDeriv_eq (s : SignedMeasure α) (μ : Measure α) [SigmaFinite μ]
(h : s ≪ᵥ μ.toENNRealVectorMeasure) : μ.withDensityᵥ (s.rnDeriv μ) = s :=
by
rw [absolutelyContinuous_ennreal_iff, (_ : μ.toENNRealVectorMeasure.ennrealToMeasure = μ),
totalVariation_absolutelyContinuous_iff] at h
· ext1 i hi
rw [withDensityᵥ_apply (integrable_rnDeriv _ _) hi, rnDeriv_def, integral_sub, setIntegral_toReal_rnDeriv h.1 i,
setIntegral_toReal_rnDeriv h.2 i]
· conv_rhs => rw [← s.toSignedMeasure_toJordanDecomposition]
erw [VectorMeasure.sub_apply]
rw [toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi, measureReal_def, measureReal_def]
all_goals
refine Integrable.integrableOn ?_
refine ⟨?_, hasFiniteIntegral_toReal_of_lintegral_ne_top ?_⟩
· apply Measurable.aestronglyMeasurable (by fun_prop)
· exact (lintegral_rnDeriv_lt_top _ _).ne
· exact equivMeasure.right_inv μ
