English
Two signed measures s and t are mutually singular if and only if their total variations are mutually singular as vector measures.
Русский
Две подписанные меры s и t взаимно-собственны тогда и только тогда, когда их полные вариации взаимно-сословны как векторные меры.
LaTeX
$$$$ s \perp_v t \iff s.totalVariation \perp_m t.totalVariation. $$$$
Lean4
theorem mutuallySingular_iff (s t : SignedMeasure α) : s ⟂ᵥ t ↔ s.totalVariation ⟂ₘ t.totalVariation :=
by
constructor
· rintro ⟨u, hmeas, hu₁, hu₂⟩
obtain ⟨i, hi₁, hi₂, hi₃, hipos, hineg⟩ := s.toJordanDecomposition_spec
obtain ⟨j, hj₁, hj₂, hj₃, hjpos, hjneg⟩ := t.toJordanDecomposition_spec
refine ⟨u, hmeas, ?_, ?_⟩
· rw [totalVariation, Measure.add_apply, hipos, hineg, toMeasureOfZeroLE_apply _ _ _ hmeas,
toMeasureOfLEZero_apply _ _ _ hmeas]
simp [hu₁ _ Set.inter_subset_right]
· rw [totalVariation, Measure.add_apply, hjpos, hjneg, toMeasureOfZeroLE_apply _ _ _ hmeas.compl,
toMeasureOfLEZero_apply _ _ _ hmeas.compl]
simp [hu₂ _ Set.inter_subset_right]
· rintro ⟨u, hmeas, hu₁, hu₂⟩
exact
⟨u, hmeas, fun t htu => null_of_totalVariation_zero _ (measure_mono_null htu hu₁), fun t htv =>
null_of_totalVariation_zero _ (measure_mono_null htv hu₂)⟩
