English
For a finite μ, restricting to the complement of the sigma-finite set scales by ∞: μ.restrict μ.sigmaFiniteSetᶜ = ∞ · μ.toFinite.restrict μ.sigmaFiniteSetᶜ.
Русский
Для μ, ограничивая по дополнению множества σ-плотного, имеем μ.restrict μ.sigmaFiniteSetᶜ = ∞ · μ.toFinite.restrict μ.sigmaFiniteSetᶜ.
LaTeX
$$$ μ \restrict μ.sigmaFiniteSet^c = \infty \cdot (μ^{toFinite} \restrict μ.sigmaFiniteSet^c) $$$
Lean4
theorem restrict_compl_sigmaFiniteSet [SFinite μ] :
μ.restrict μ.sigmaFiniteSetᶜ = ∞ • μ.toFinite.restrict μ.sigmaFiniteSetᶜ :=
by
rw [Measure.sigmaFiniteSet, restrict_compl_sigmaFiniteSetWRT (Measure.AbsolutelyContinuous.refl μ)]
ext t ht
simp only [Measure.smul_apply, smul_eq_mul]
rw [Measure.restrict_apply ht, Measure.restrict_apply ht]
by_cases hμt : μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = 0
· rw [hμt, toFinite_absolutelyContinuous μ hμt]
· rw [ENNReal.top_mul hμt, ENNReal.top_mul]
exact fun h ↦ hμt (absolutelyContinuous_toFinite μ h)
