English
Any s-finite measure μ has a Lebesgue decomposition w.r.t. any σ-finite ν.
Русский
Любая s-финитная мера μ имеет разложение Лебеса по любой σ-финитной мере ν.
LaTeX
$$$$ \\text{HaveLebesgueDecomposition}(μ, ν) \\text{ for all } μ\\;[SFinite], ν\\;[SigmaFinite]. $$$$
Lean4
/-- **The Lebesgue decomposition theorem**:
Any s-finite measure `μ` has Lebesgue decomposition with respect to any σ-finite measure `ν`.
That is to say, there exist a measure `ξ` and a measurable function `f`,
such that `ξ` is mutually singular with respect to `ν` and `μ = ξ + ν.withDensity f` -/
nonrec instance (priority := 100) haveLebesgueDecomposition_of_sigmaFinite [SFinite μ] [SigmaFinite ν] :
HaveLebesgueDecomposition μ ν := by
wlog hμ : IsFiniteMeasure μ generalizing μ
·
exact
.sfinite_of_isFiniteMeasure fun μ _ ↦
this μ
‹_›
-- Take a disjoint cover that consists of sets of finite measure `ν`.
set s : ℕ → Set α := disjointed (spanningSets ν)
have hsm : ∀ n, MeasurableSet (s n) := .disjointed <| measurableSet_spanningSets _
have hs : ∀ n, Fact (ν (s n) < ⊤) := fun n ↦
⟨lt_of_le_of_lt (measure_mono <| disjointed_le ..) (measure_spanningSets_lt_top ν n)⟩
-- Note that the restrictions of `μ` and `ν` to `s n` are finite measures.
-- Therefore, as we proved above, these restrictions have a Lebesgue decomposition.
-- Let `ξ n` and `f n` be the singular part and the Radon-Nikodym derivative
-- of these restrictions.
set ξ : ℕ → Measure α := fun n : ℕ ↦ singularPart (.restrict μ (s n)) (.restrict ν (s n))
set f : ℕ → α → ℝ≥0∞ := fun n ↦ (s n).indicator (rnDeriv (.restrict μ (s n)) (.restrict ν (s n)))
have hfm (n : ℕ) : Measurable (f n) := by
measurability
-- Each `ξ n` is supported on `s n` and is mutually singular with the restriction of `ν` to `s n`.
-- Therefore, `ξ n` is mutually singular with `ν`, hence their sum is mutually singular with `ν`.
have hξ : .sum ξ ⟂ₘ ν := by
refine MutuallySingular.sum_left.2 fun n ↦ ?_
rw [← ν.restrict_add_restrict_compl (hsm n)]
refine (mutuallySingular_singularPart ..).add_right (.singularPart ?_ _)
refine ⟨(s n)ᶜ, (hsm n).compl, ?_⟩
simp [hsm]
-- Finally, the sum of all `ξ n` and measure `ν` with the density `∑' n, f n`
-- is equal to `μ`, thus `(Measure.sum ξ, ∑' n, f n)` is a Lebesgue decomposition for `μ` and `ν`.
have hadd : .sum ξ + ν.withDensity (∑' n, f n) = μ :=
calc
.sum ξ + ν.withDensity (∑' n, f n) = .sum fun n ↦ ξ n + ν.withDensity (f n) := by
rw [withDensity_tsum hfm, Measure.sum_add_sum]
_ = .sum fun n ↦ .restrict μ (s n) := by simp_rw [ξ, f, withDensity_indicator (hsm _), singularPart_add_rnDeriv]
_ = μ := sum_restrict_disjointed_spanningSets ..
exact ⟨⟨(.sum ξ, ∑' n, f n), by fun_prop, hξ, hadd.symm⟩⟩
