English
Mutual singularity for signed measure s and ENNReal-typed vector measure μ is equivalent to mutual singularity of their total variation and μ.ennrealToMeasure.
Русский
Взаимная принадлежность между знаковой мерой s и векторной мерой μ ENNReal эквивалентна взаимному несовместимости их полной вариации и μ.ennrealToMeasure.
LaTeX
$$$$ s \perp_v μ \iff s.totalVariation \perp_m μ.ennrealToMeasure. $$$$
Lean4
theorem mutuallySingular_ennreal_iff (s : SignedMeasure α) (μ : VectorMeasure α ℝ≥0∞) :
s ⟂ᵥ μ ↔ s.totalVariation ⟂ₘ μ.ennrealToMeasure :=
by
constructor
· rintro ⟨u, hmeas, hu₁, hu₂⟩
obtain ⟨i, hi₁, hi₂, hi₃, hpos, hneg⟩ := s.toJordanDecomposition_spec
refine ⟨u, hmeas, ?_, ?_⟩
· rw [totalVariation, Measure.add_apply, hpos, hneg, toMeasureOfZeroLE_apply _ _ _ hmeas,
toMeasureOfLEZero_apply _ _ _ hmeas]
simp [hu₁ _ Set.inter_subset_right]
· rw [VectorMeasure.ennrealToMeasure_apply hmeas.compl]
exact hu₂ _ (Set.Subset.refl _)
· rintro ⟨u, hmeas, hu₁, hu₂⟩
refine
VectorMeasure.MutuallySingular.mk u hmeas
(fun t htu _ => null_of_totalVariation_zero _ (measure_mono_null htu hu₁)) fun t htv hmt => ?_
rw [← VectorMeasure.ennrealToMeasure_apply hmt]
exact measure_mono_null htv hu₂
