English
Two signed measures s and μ are mutually singular if and only if their total variation is mutually singular with μ.ennrealToMeasure, in the ENNReal setting.
Русский
Две подписанные меры s и μ взаимно-с tvрежны тогда и только тогда, когда их полная вариация взаимоодинакова по отношению к μ.ennrealToMeasure, в обстановке ENNReal.
LaTeX
$$$$ s \perp^\!_v μ \iff s.totalVariation \perp^\!_m μ.ennrealToMeasure. $$$$
Lean4
theorem absolutelyContinuous_ennreal_iff (s : SignedMeasure α) (μ : VectorMeasure α ℝ≥0∞) :
s ≪ᵥ μ ↔ s.totalVariation ≪ μ.ennrealToMeasure :=
by
constructor <;> intro h
· refine Measure.AbsolutelyContinuous.mk fun S hS₁ hS₂ => ?_
obtain ⟨i, hi₁, hi₂, hi₃, hpos, hneg⟩ := s.toJordanDecomposition_spec
rw [totalVariation, Measure.add_apply, hpos, hneg, toMeasureOfZeroLE_apply _ _ _ hS₁,
toMeasureOfLEZero_apply _ _ _ hS₁]
rw [← VectorMeasure.AbsolutelyContinuous.ennrealToMeasure] at h
simp [h (measure_mono_null (i.inter_subset_right) hS₂), h (measure_mono_null (iᶜ.inter_subset_right) hS₂)]
· refine VectorMeasure.AbsolutelyContinuous.mk fun S hS₁ hS₂ => ?_
rw [← VectorMeasure.ennrealToMeasure_apply hS₁] at hS₂
exact null_of_totalVariation_zero s (h hS₂)
