English
A signed measure s is absolutely continuous with respect to μ if and only if μ.withDensityᵥ (s.rnDeriv μ) = s.
Русский
Знаковая мера s абсолютно непрерывна по отношению к μ если и только если μ.withDensityᵥ (s.rnDeriv μ) = s.
LaTeX
$$$ s ≪ᵥ μ.toENNRealVectorMeasure \\iff μ.withDensityᵥ (s.rnDeriv μ) = s $$$
Lean4
@[simp]
theorem withDensityᵥ_neg : μ.withDensityᵥ (-f) = -μ.withDensityᵥ f :=
by
by_cases hf : Integrable f μ
· ext1 i hi
rw [VectorMeasure.neg_apply, withDensityᵥ_apply hf hi, ← integral_neg, withDensityᵥ_apply hf.neg hi]
simp only [Pi.neg_apply]
· rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg, neg_zero]
rwa [integrable_neg_iff]