English
If μ = s + ν.withDensity f for some measurable f and s ⟂ ν, then ν.withDensity f = ν.withDensity(μ.rnDer ν).
Русский
Если μ = s + ν.withDensity f и s ⟂ ν, то ν.withDensity f = ν.withDensity(μ.rnDer ν).
LaTeX
$$$ μ = s + ν.withDensity f \\Rightarrow ν.withDensity f = ν.withDensity(μ.rnDer ν) $$$
Lean4
/-- Given measures `μ` and `ν`, if `s` is a measure mutually singular to `ν` and `f` is a
measurable function such that `μ = s + fν`, then `f = μ.rnDeriv ν`.
This theorem provides the uniqueness of the `rnDeriv` in the Lebesgue decomposition
theorem, while `MeasureTheory.Measure.eq_singularPart` provides the uniqueness of the
`singularPart`. Here, the uniqueness is given in terms of the measures, while the uniqueness in
terms of the functions is given in `eq_rnDeriv`. -/
theorem eq_withDensity_rnDeriv {s : Measure α} {f : α → ℝ≥0∞} (hf : Measurable f) (hs : s ⟂ₘ ν)
(hadd : μ = s + ν.withDensity f) : ν.withDensity f = ν.withDensity (μ.rnDeriv ν) :=
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 : (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) :=
by
ext1 A hA
have hs : s (A ∩ (S ∩ T)) = 0 := by
rw [← nonpos_iff_eq_zero]
exact hS₂ ▸ measure_mono (inter_subset_right.trans inter_subset_left)
have hsing : μ.singularPart ν (A ∩ (S ∩ T)) = 0 :=
by
rw [← nonpos_iff_eq_zero]
exact hT₂ ▸ measure_mono (inter_subset_right.trans inter_subset_right)
rw [restrict_apply hA, restrict_apply hA, ← add_zero (ν.withDensity f (A ∩ (S ∩ T))), ← hs, ← add_apply, add_comm, ←
hadd, add_apply, hsing, zero_add]
have heq' : ∀ A : Set α, MeasurableSet A → ν.withDensity f A = (ν.withDensity f).restrict (S ∩ T) A :=
by
intro A hA
have hνfinter : ν.withDensity f (A ∩ (S ∩ T)ᶜ) = 0 :=
by
rw [← nonpos_iff_eq_zero]
exact withDensity_absolutelyContinuous ν f hνinter ▸ measure_mono inter_subset_right
rw [restrict_apply hA, ← add_zero (ν.withDensity f (A ∩ (S ∩ T))), ← hνfinter, ← diff_eq,
measure_inter_add_diff _ (hS₁.inter hT₁)]
ext1 A hA
have hνrn : ν.withDensity (μ.rnDeriv ν) (A ∩ (S ∩ T)ᶜ) = 0 :=
by
rw [← nonpos_iff_eq_zero]
exact withDensity_absolutelyContinuous ν (μ.rnDeriv ν) hνinter ▸ measure_mono inter_subset_right
rw [heq' A hA, heq, ← add_zero ((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) A), ← hνrn, restrict_apply hA, ←
diff_eq, measure_inter_add_diff _ (hS₁.inter hT₁)]
