English
If μ is absolutely continuous with respect to ν and ν is sigma-finite and ν finite, then the complement of μ.sigmaFiniteSetWRT ν has ν-measure zero.
Русский
Если μ абсолютно непрерывна относительно ν и ν сигма-финитна и ν конечна, то мера ν на дополнение к μ.sigmaFiniteSetWRT ν равна нулю.
LaTeX
$$$$ ν (μ.sigmaFiniteSetWRT ν)^{c} = 0.$$$$
Lean4
@[simp]
theorem measure_compl_sigmaFiniteSetWRT (hμν : μ ≪ ν) [SigmaFinite μ] [SFinite ν] : ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0 :=
by
have h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞ :=
measure_eq_top_of_subset_compl_sigmaFiniteSetWRT subset_rfl
by_contra h0
refine ENNReal.top_ne_zero ?_
rw [← h h0, ← Measure.iSup_restrict_spanningSets]
simp_rw [Measure.restrict_apply' (measurableSet_spanningSets μ _), ENNReal.iSup_eq_zero]
intro i
by_contra h_ne_zero
have h_zero_top :=
measure_eq_top_of_subset_compl_sigmaFiniteSetWRT
(Set.inter_subset_left : (μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i ⊆ _) ?_
swap; · exact fun h ↦ h_ne_zero (hμν h)
refine absurd h_zero_top (ne_of_lt ?_)
exact (measure_mono Set.inter_subset_right).trans_lt (measure_spanningSets_lt_top μ i)
