English
For any finite measures μ, ν there exists a Lebesgue decomposition: μ = ξ + ν withDensity f and ξ ⟂ₘ ν.
Русский
Для любых конечных мер μ, ν существует разложение Лебеса: μ = ξ + ν.withDensity f, причём ξ ⟂ₘ ν.
LaTeX
$$$$ \\exists \\xi, f \\text{ with } \\xi \\perp_m \\nu \\text{ and } \\mu = \\xi + \\nu.withDensity(f). $$$$
Lean4
/-- Any pair of finite measures `μ` and `ν`, `HaveLebesgueDecomposition`. That is to say,
there exist a measure `ξ` and a measurable function `f`, such that `ξ` is mutually singular
with respect to `ν` and `μ = ξ + ν.withDensity f`.
This is not an instance since this is also shown for the more general σ-finite measures with
`MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite`. -/
theorem haveLebesgueDecomposition_of_finiteMeasure [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
HaveLebesgueDecomposition μ ν where
lebesgue_decomposition :=
by
have h :=
@exists_seq_tendsto_sSup _ _ _ _ _ (measurableLEEval ν μ) ⟨0, 0, zero_mem_measurableLE, by simp⟩
(OrderTop.bddAbove _)
choose g _ hg₂ f hf₁ hf₂ using h
set ξ := ⨆ (n) (k) (_ : k ≤ n), f k with hξ
have hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ a, ξ a ∂ν :=
by
have :=
@lintegral_tendsto_of_tendsto_of_monotone _ _ ν (fun n ↦ ⨆ (k) (_ : k ≤ n), f k) (⨆ (n) (k) (_ : k ≤ n), f k) ?_
?_ ?_
· refine tendsto_nhds_unique ?_ this
refine tendsto_of_tendsto_of_tendsto_of_le_of_le hg₂ tendsto_const_nhds (fun n ↦ ?_) fun n ↦ ?_
· rw [← hf₂ n]
apply lintegral_mono
convert iSup_le_le f n n le_rfl
simp only [iSup_apply]
· exact le_sSup ⟨⨆ (k : ℕ) (_ : k ≤ n), f k, iSup_mem_measurableLE' _ hf₁ _, rfl⟩
· intro n
refine Measurable.aemeasurable ?_
convert (iSup_mem_measurableLE _ hf₁ n).1
simp
· refine Filter.Eventually.of_forall fun a ↦ ?_
simp [iSup_monotone' f _]
· refine Filter.Eventually.of_forall fun a ↦ ?_
simp [tendsto_atTop_iSup (iSup_monotone' f a)]
have hξm : Measurable ξ :=
by
convert Measurable.iSup fun n ↦ (iSup_mem_measurableLE _ hf₁ n).1
simp [hξ]
-- we see that `ξ` has the largest integral among all functions in `measurableLE`
have hξle A (hA : MeasurableSet A) : ∫⁻ a in A, ξ a ∂ν ≤ μ A :=
by
rw [hξ]
simp_rw [iSup_apply]
rw [lintegral_iSup (fun n ↦ (iSup_mem_measurableLE _ hf₁ n).1) (iSup_monotone _)]
exact iSup_le fun n ↦ (iSup_mem_measurableLE _ hf₁ n).2 A hA
have hle : ν.withDensity ξ ≤ μ := by
refine le_intro fun B hB _ ↦ ?_
rw [withDensity_apply _ hB]
exact hξle B hB
have : IsFiniteMeasure (ν.withDensity ξ) :=
by
refine isFiniteMeasure_withDensity ?_
have hle' := hle univ
rw [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ] at hle'
exact ne_top_of_le_ne_top (measure_ne_top _ _) hle'
set μ₁ := μ - ν.withDensity ξ with hμ₁
refine ⟨⟨μ₁, ξ⟩, hξm, ?_, ?_⟩
· by_contra h
obtain ⟨ε, hε₁, E, hE₁, hE₂, hE₃⟩ := exists_positive_of_not_mutuallySingular μ₁ ν h
simp_rw [hμ₁] at hE₃
have hε₂ (A : Set α) (hA : MeasurableSet A) : ∫⁻ a in A ∩ E, ε + ξ a ∂ν ≤ μ (A ∩ E) :=
by
specialize hE₃ A hA
rw [lintegral_add_left measurable_const, lintegral_const, restrict_apply_univ]
rw [Measure.sub_apply (hA.inter hE₁) hle, withDensity_apply _ (hA.inter hE₁)] at hE₃
refine add_le_of_le_tsub_right_of_le (hξle _ (hA.inter hE₁)) hE₃
have hξε : (ξ + E.indicator fun _ ↦ (ε : ℝ≥0∞)) ∈ measurableLE ν μ :=
by
refine ⟨hξm.add (measurable_const.indicator hE₁), fun A hA ↦ ?_⟩
have :
∫⁻ a in A, (ξ + E.indicator fun _ ↦ (ε : ℝ≥0∞)) a ∂ν = ∫⁻ a in A ∩ E, ε + ξ a ∂ν + ∫⁻ a in A \ E, ξ a ∂ν :=
by
simp only [lintegral_add_left measurable_const, lintegral_add_left hξm, setLIntegral_const, add_assoc,
lintegral_inter_add_diff _ _ hE₁, Pi.add_apply, lintegral_indicator hE₁, restrict_apply hE₁]
rw [inter_comm, add_comm]
rw [this, ← measure_inter_add_diff A hE₁]
exact add_le_add (hε₂ A hA) (hξle (A \ E) (hA.diff hE₁))
have : (∫⁻ a, ξ a + E.indicator (fun _ ↦ (ε : ℝ≥0∞)) a ∂ν) ≤ sSup (measurableLEEval ν μ) :=
le_sSup
⟨ξ + E.indicator fun _ ↦ (ε : ℝ≥0∞), hξε, rfl⟩
-- but this contradicts the maximality of `∫⁻ x, ξ x ∂ν`
refine not_lt.2 this ?_
rw [hξ₁, lintegral_add_left hξm, lintegral_indicator hE₁, setLIntegral_const]
refine ENNReal.lt_add_right ?_ (ENNReal.mul_pos_iff.2 ⟨ENNReal.coe_pos.2 hε₁, hE₂⟩).ne'
have := measure_ne_top (ν.withDensity ξ) univ
rwa [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ] at this
· rw [hμ₁]
ext1 A hA
rw [Measure.coe_add, Pi.add_apply, Measure.sub_apply hA hle, add_comm, add_tsub_cancel_of_le (hle A)]
