English
A signed measure s is absolutely continuous with respect to a vector measure μ (ENNReal setting) if and only if its total variation is absolutely continuous with respect to μ.ennrealToMeasure, which is equivalent to the joint absolute continuity of posPart and negPart with μ.
Русский
Подписанная мера s относительно векторной меры μ (величины ENNReal) абсолютно непрерывна тогда и только тогда, когда её полная вариация абсолютно непрерывна относительно μ.ennrealToMeasure, что эквивалентно абсолютной непрерывности положительной и отрицательной частей по отношению к μ.
LaTeX
$$$$ \forall s:\, SignedMeasure(\alpha),\; \mu:\, VectorMeasure(\alpha, ENNReal),\; s \ll\!\!\!\!_v \mu \iff s.totalVariation \ll\!\!\!\!\mu.ennrealToMeasure. $$$$
Lean4
theorem null_of_totalVariation_zero (s : SignedMeasure α) {i : Set α} (hs : s.totalVariation i = 0) : s i = 0 :=
by
rw [totalVariation, Measure.coe_add, Pi.add_apply, add_eq_zero] at hs
rw [← toSignedMeasure_toJordanDecomposition s, toSignedMeasure, VectorMeasure.coe_sub, Pi.sub_apply,
Measure.toSignedMeasure_apply, Measure.toSignedMeasure_apply]
by_cases hi : MeasurableSet i
· simp [hs.1, hs.2, measureReal_def]
· simp [if_neg hi]
