English
A signed measure s has total variation absolutely continuous with respect to μ if and only if its Jordan decomposition’s posPart and negPart are absolutely continuous with respect to μ.
Русский
Полная вариация знаковой меры s относительно μ абсолютизируется тогда и только тогда, когда её часть posPart и negPart абсолютизируемы относительно μ.
LaTeX
$$$$ s.totalVariation \ll \!\!\!\! \mu \;\iff\; (s.toJordanDecomposition.posPart \ll \!\!\!\! \mu) \land (s.toJordanDecomposition.negPart \ll \!\!\!\! \mu). $$$$
Lean4
theorem totalVariation_absolutelyContinuous_iff (s : SignedMeasure α) (μ : Measure α) :
s.totalVariation ≪ μ ↔ s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ :=
by
constructor <;> intro h
· constructor
all_goals
refine Measure.AbsolutelyContinuous.mk fun S _ hS₂ => ?_
have := h hS₂
rw [totalVariation, Measure.add_apply, add_eq_zero] at this
exacts [this.1, this.2]
· refine Measure.AbsolutelyContinuous.mk fun S _ hS₂ => ?_
rw [totalVariation, Measure.add_apply, h.1 hS₂, h.2 hS₂, add_zero]
-- TODO: Generalize to vector measures once total variation on vector measures is defined
