English
If s ⟂ ν and μ = s + fν for some measurable f, then s = μ.singularPart ν.
Русский
Если s несобственная ν и μ = s + fν для некоторой измеримой функции f, то s = μ.singularPart ν.
LaTeX
$$$\\text{If } s ⟂_m ν \\text{ and } μ = s + ν^{\\mathrm{withDensity}}(f)\\text{ with } f\\text{ measurable}, \\text{ then } s = μ.singularPart ν$$$
Lean4
/-- Given measures `μ` and `ν`, if `s` is a measure mutually singular to `ν` and `f` is a
measurable function such that `μ = s + fν`, then `s = μ.singularPart μ`.
This theorem provides the uniqueness of the `singularPart` in the Lebesgue decomposition theorem,
while `MeasureTheory.Measure.eq_rnDeriv` provides the uniqueness of the
`rnDeriv`. -/
theorem eq_singularPart {s : Measure α} {f : α → ℝ≥0∞} (hf : Measurable f) (hs : s ⟂ₘ ν)
(hadd : μ = s + ν.withDensity f) : s = μ.singularPart ν :=
by
have : HaveLebesgueDecomposition μ ν := ⟨⟨⟨s, f⟩, hf, hs, hadd⟩⟩
obtain ⟨hmeas, hsing, hadd'⟩ := haveLebesgueDecomposition_spec μ ν
obtain ⟨⟨S, hS₁, hS₂, hS₃⟩, ⟨T, hT₁, hT₂, hT₃⟩⟩ := hs, hsing
rw [hadd'] at hadd
have hνinter : ν (S ∩ T)ᶜ = 0 := by
rw [compl_inter]
refine nonpos_iff_eq_zero.1 (le_trans (measure_union_le _ _) ?_)
rw [hT₃, hS₃, add_zero]
have heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ :=
by
ext1 A hA
have hf : ν.withDensity f (A ∩ (S ∩ T)ᶜ) = 0 :=
by
refine withDensity_absolutelyContinuous ν _ ?_
rw [← nonpos_iff_eq_zero]
exact hνinter ▸ measure_mono inter_subset_right
have hrn : ν.withDensity (μ.rnDeriv ν) (A ∩ (S ∩ T)ᶜ) = 0 :=
by
refine withDensity_absolutelyContinuous ν _ ?_
rw [← nonpos_iff_eq_zero]
exact hνinter ▸ measure_mono inter_subset_right
rw [restrict_apply hA, restrict_apply hA, ← add_zero (s (A ∩ (S ∩ T)ᶜ)), ← hf, ← add_apply, ← hadd, add_apply, hrn,
add_zero]
have heq' : ∀ A : Set α, MeasurableSet A → s A = s.restrict (S ∩ T)ᶜ A :=
by
intro A hA
have hsinter : s (A ∩ (S ∩ T)) = 0 := by
rw [← nonpos_iff_eq_zero]
exact hS₂ ▸ measure_mono (inter_subset_right.trans inter_subset_left)
rw [restrict_apply hA, ← diff_eq, AEDisjoint.measure_diff_left hsinter]
ext1 A hA
have hμinter : μ.singularPart ν (A ∩ (S ∩ T)) = 0 :=
by
rw [← nonpos_iff_eq_zero]
exact hT₂ ▸ measure_mono (inter_subset_right.trans inter_subset_right)
rw [heq' A hA, heq, restrict_apply hA, ← diff_eq, AEDisjoint.measure_diff_left hμinter]
