feat(measure_theory/decomposition/lebesgue): Lebesgue decomposition for sigma-finite measures (#8875)

This PR shows sigma-finite measures `have_lebesgue_decomposition`. With this instance, `absolutely_continuous_iff_with_density_radon_nikodym_deriv_eq` will provide the Radon-Nikodym theorem for sigma-finite measures.

Author: kex-y

src/measure_theory/constructions/borel_space.lean

@@ -1279,6 +1279,15 @@ lemma measurable.ennreal_tsum {ι} [encodable ι] {f : ι → α → ℝ≥0∞}
 by { simp_rw [ennreal.tsum_eq_supr_sum], apply measurable_supr,
   exact λ s, s.measurable_sum (λ i _, h i) }
 
+@[measurability]
+lemma measurable.ennreal_tsum' {ι} [encodable ι] {f : ι → α → ℝ≥0∞} (h : ∀ i, measurable (f i)) :
+  measurable (∑' i, f i) :=
+begin
+  convert measurable.ennreal_tsum h,
+  ext1 x,
+  exact tsum_apply (pi.summable.2 (λ _, ennreal.summable)),
+end
+
 @[measurability]
 lemma measurable.nnreal_tsum {ι} [encodable ι] {f : ι → α → ℝ≥0} (h : ∀ i, measurable (f i)) :
   measurable (λ x, ∑' i, f i x) :=

src/measure_theory/decomposition/lebesgue.lean

@@ -9,7 +9,7 @@ import measure_theory.decomposition.jordan
 # Lebesgue decomposition
 
 This file proves the Lebesgue decomposition theorem. The Lebesgue decomposition theorem states that,
-given two finite measures `μ` and `ν`, there exists a finite measure `ξ` and a measurable function
+given two σ-finite measures `μ` and `ν`, there exists a finite measure `ξ` and a measurable function
 `f` such that `μ = ξ + fν` and `ξ` is mutually singular with respect to `ν`.
 
 The Lebesgue decomposition provides the Radon-Nikodym theorem readily.
@@ -22,13 +22,13 @@ The Lebesgue decomposition provides the Radon-Nikodym theorem readily.
 * `measure_theory.measure.singular_part` : If a pair of measures `have_lebesgue_decomposition`,
   then `singular_part` chooses the measure from `have_lebesgue_decomposition`, otherwise it
   returns the zero measure.
-* ``measure_theory.measure.radon_nikodym_deriv` : If a pair of measures
+* `measure_theory.measure.radon_nikodym_deriv` : If a pair of measures
   `have_lebesgue_decomposition`, then `radon_nikodym_deriv` chooses the measurable function from
   `have_lebesgue_decomposition`, otherwise it returns the zero function.
 
 ## Main results
 
-* `measure_theory.measure.have_lebesgue_decomposition_of_finite_measure` :
+* `measure_theory.measure.have_lebesgue_decomposition_of_sigma_finite` :
   the Lebesgue decomposition theorem.
 * `measure_theory.measure.eq_singular_part` : Given measures `μ` and `ν`, if `s` is a measure
   mutually singular to `ν` and `f` is a measurable function such that `μ = s + fν`, then
@@ -37,10 +37,6 @@ The Lebesgue decomposition provides the Radon-Nikodym theorem readily.
   measure mutually singular to `ν` and `f` is a measurable function such that `μ = s + fν`,
   then `f = radon_nikodym_deriv μ ν`.
 
-## To do
-
-The Lebesgue decomposition theorem can be generalized to σ-finite measures from the finite version.
-
 # Tags
 
 Lebesgue decomposition theorem
@@ -458,11 +454,13 @@ end lebesgue_decomposition
 
 open lebesgue_decomposition
 
-/-- **The Lebesgue decomposition theorem**: Any pair of finite measures `μ` and `ν`
-`have_lebesgue_decomposition`. That is to say, there exists a measure `ξ` and a measurable function
-`f`, such that `ξ` is mutually singular with respect to `ν` and `μ = ξ + ν.with_density f` -/
-@[priority 100] -- see Note [lower instance priority]
-instance have_lebesgue_decomposition_of_finite_measure
+/-- Any pair of finite measures `μ` and `ν`, `have_lebesgue_decomposition`. That is to say,
+there exist a measure `ξ` and a measurable function `f`, such that `ξ` is mutually singular
+with respect to `ν` and `μ = ξ + ν.with_density f`.
+
+This is not an instance since this is also shown for the more general σ-finite measures with
+`measure_theory.measure.have_lebesgue_decomposition_of_sigma_finite`. -/
+theorem have_lebesgue_decomposition_of_finite_measure
   {μ ν : measure α} [finite_measure μ] [finite_measure ν] :
   have_lebesgue_decomposition μ ν :=
 ⟨begin
@@ -574,6 +572,118 @@ instance have_lebesgue_decomposition_of_finite_measure
         add_comm, ennreal.add_sub_cancel_of_le (hle A hA)] },
 end⟩
 
+local attribute [instance] have_lebesgue_decomposition_of_finite_measure
+
+instance {μ : measure α} {S : μ.finite_spanning_sets_in {s : set α | measurable_set s}} (n : ℕ) :
+  finite_measure (μ.restrict $ S.set n) :=
+⟨by { rw [restrict_apply measurable_set.univ, set.univ_inter], exact S.finite _ }⟩
+
+/-- **The Lebesgue decomposition theorem**: Any pair of σ-finite measures `μ` and `ν`
+`have_lebesgue_decomposition`. That is to say, there exist a measure `ξ` and a measurable function
+`f`, such that `ξ` is mutually singular with respect to `ν` and `μ = ξ + ν.with_density f` -/
+@[priority 100] -- see Note [lower instance priority]
+instance have_lebesgue_decomposition_of_sigma_finite
+  (μ ν : measure α) [sigma_finite μ] [sigma_finite ν] :
+  have_lebesgue_decomposition μ ν :=
+⟨begin
+  -- Since `μ` and `ν` are both σ-finite, there exists a sequence of pairwise disjoint spanning
+  -- sets which are finite with respect to both `μ` and `ν`
+  obtain ⟨S, T, h₁, h₂⟩ := exists_eq_disjoint_finite_spanning_sets_in μ ν,
+  have h₃ : pairwise (disjoint on T.set) := h₁ ▸ h₂,
+  -- We define `μn` and `νn` as sequences of measures such that `μn n = μ ∩ S n` and
+  -- `νn n = ν ∩ S n` where `S` is the aforementioned finite spanning set sequence.
+  -- Since `S` is spanning, it is clear that `sum μn = μ` and `sum νn = ν`
+  set μn : ℕ → measure α := λ n, μ.restrict (S.set n) with hμn,
+  have hμ : μ = sum μn,
+    { rw [hμn, ← restrict_Union h₂ S.set_mem, S.spanning, restrict_univ] },
+  set νn : ℕ → measure α := λ n, ν.restrict (T.set n) with hνn,
+  have hν : ν = sum νn,
+    { rw [hνn, ← restrict_Union h₃ T.set_mem, T.spanning, restrict_univ] },
+  -- As `S` is finite with respect to both `μ` and `ν`, it is clear that `μn n` and `νn n` are
+  -- finite measures for all `n : ℕ`. Thus, we may apply the finite Lebesgue decomposition theorem
+  -- to `μn n` and `νn n`. We define `ξ` as the sum of the singular part of the Lebesgue
+  -- decompositions of `μn n` and `νn n`, and `f` as the sum of the Radon-Nikodym derviatives of
+  -- `μn n` and `νn n` restricted on `S n`
+  set ξ := sum (λ n, singular_part (μn n) (νn n)) with hξ,
+  set f := ∑' n, (S.set n).indicator (radon_nikodym_deriv (μn n) (νn n)) with hf,
+  -- I claim `ξ` and `f` form a Lebesgue decomposition of `μ` and `ν`
+  refine ⟨⟨ξ, f⟩, _, _, _⟩,
+  { exact measurable.ennreal_tsum' (λ n, measurable.indicator
+      (measurable_radon_nikodym_deriv (μn n) (νn n)) (S.set_mem n)) },
+  -- We show that `ξ` is mutually singular with respect to `ν`
+  { choose A hA₁ hA₂ hA₃ using λ n, mutually_singular_singular_part (μn n) (νn n),
+    simp only [hξ],
+  -- We use the set `B := ⋃ j, (S.set j) ∩ A j` where `A n` is the set provided as
+  -- `singular_part (μn n) (νn n) ⊥ₘ νn n`
+    refine ⟨⋃ j, (S.set j) ∩ A j,
+      measurable_set.Union (λ n, (S.set_mem n).inter (hA₁ n)), _, _⟩,
+  -- `ξ B = 0` since `ξ B = ∑ i j, singular_part (μn j) (νn j) (S.set i ∩ A i)`
+  --                     `= ∑ i, singular_part (μn i) (νn i) (S.set i ∩ A i)`
+  --                     `≤ ∑ i, singular_part (μn i) (νn i) (A i) = 0`
+  -- where the second equality follows as `singular_part (μn j) (νn j) (S.set i ∩ A i)` vanishes
+  -- for all `i ≠ j`
+    { rw [measure_Union],
+      { have : ∀ i, (sum (λ n, (μn n).singular_part (νn n))) (S.set i ∩ A i) =
+          (μn i).singular_part (νn i) (S.set i ∩ A i),
+        { intro i, rw [sum_apply _ ((S.set_mem i).inter (hA₁ i)), tsum_eq_single i],
+          { intros j hij,
+            rw [hμn, ← nonpos_iff_eq_zero],
+            refine le_trans ((singular_part_le _ _) _ ((S.set_mem i).inter (hA₁ i))) (le_of_eq _),
+            rw [restrict_apply ((S.set_mem i).inter (hA₁ i)), set.inter_comm, ← set.inter_assoc],
+            have : disjoint (S.set j) (S.set i) := h₂ j i hij,
+            rw set.disjoint_iff_inter_eq_empty at this,
+            rw [this, set.empty_inter, measure_empty] },
+          { apply_instance } },
+        simp_rw [this, tsum_eq_zero_iff ennreal.summable],
+        intro n, exact measure_mono_null (set.inter_subset_right _ _) (hA₂ n) },
+      { exact h₂.mono (λ i j, disjoint.mono inf_le_left inf_le_left) },
+      { exact λ n, (S.set_mem n).inter (hA₁ n) } },
+  -- We will now show `ν Bᶜ = 0`. This follows since `Bᶜ = ⋃ n, S.set n ∩ (A n)ᶜ` and thus,
+  -- `ν Bᶜ = ∑ i, ν (S.set i ∩ (A i)ᶜ) = ∑ i, (νn i) (A i)ᶜ = 0`
+    { have hcompl : is_compl (⋃ n, (S.set n ∩ A n)) (⋃ n, S.set n ∩ (A n)ᶜ),
+      { split,
+        { rintro x ⟨hx₁, hx₂⟩, rw set.mem_Union at hx₁ hx₂,
+          obtain ⟨⟨i, hi₁, hi₂⟩, ⟨j, hj₁, hj₂⟩⟩ := ⟨hx₁, hx₂⟩,
+          have : i = j,
+          { by_contra hij, exact h₂ i j hij ⟨hi₁, hj₁⟩ },
+          exact hj₂ (this ▸ hi₂) },
+        { intros x hx,
+          simp only [set.mem_Union, set.sup_eq_union, set.mem_inter_eq,
+                    set.mem_union_eq, set.mem_compl_eq, or_iff_not_imp_left],
+          intro h, push_neg at h,
+          rw [set.top_eq_univ, ← S.spanning, set.mem_Union] at hx,
+          obtain ⟨i, hi⟩ := hx,
+          exact ⟨i, hi, h i hi⟩ } },
+      rw [hcompl.compl_eq, measure_Union, tsum_eq_zero_iff ennreal.summable],
+      { intro n, rw [set.inter_comm, ← restrict_apply (hA₁ n).compl, ← hA₃ n, hνn, h₁] },
+      { exact h₂.mono (λ i j, disjoint.mono inf_le_left inf_le_left) },
+      { exact λ n, (S.set_mem n).inter (hA₁ n).compl } } },
+  -- Finally, it remains to show `μ = ξ + ν.with_density f`. Since `μ = sum μn`, and
+  -- `ξ + ν.with_density f = ∑ n, singular_part (μn n) (νn n)`
+  --                        `+ ν.with_density (radon_nikodym_deriv (μn n) (νn n)) ∩ (S.set n)`,
+  -- it suffices to show that the individual summands are equal. This follows by the
+  -- Lebesgue decomposition properties on the individual `μn n` and `νn n`
+  { simp only [hξ, hf, hμ],
+    rw [with_density_tsum _, sum_add_sum],
+    { refine sum_congr (λ n, _),
+      conv_lhs { rw have_lebesgue_decomposition_add (μn n) (νn n) },
+      suffices heq : (νn n).with_density ((μn n).radon_nikodym_deriv (νn n)) =
+        ν.with_density ((S.set n).indicator ((μn n).radon_nikodym_deriv (νn n))),
+      { rw heq },
+      rw [hν, with_density_indicator (S.set_mem n), restrict_sum _ (S.set_mem n)],
+      suffices hsumeq : sum (λ (i : ℕ), (νn i).restrict (S.set n)) = νn n,
+      { rw hsumeq },
+      ext1 s hs,
+      rw [sum_apply _ hs, tsum_eq_single n, hνn, h₁,
+          restrict_restrict (T.set_mem n), set.inter_self],
+      { intros m hm,
+        rw [hνn, h₁, restrict_restrict (T.set_mem n), set.inter_comm,
+            set.disjoint_iff_inter_eq_empty.1 (h₃ m n hm), restrict_empty,
+            coe_zero, pi.zero_apply] },
+      { apply_instance } },
+    { exact λ n, measurable.indicator (measurable_radon_nikodym_deriv _ _) (S.set_mem n) } },
+end⟩
+
 end measure
 
 end measure_theory

src/measure_theory/decomposition/radon_nikodym.lean

@@ -18,7 +18,7 @@ most notably conditional expectations and probability cumulative functions.
 
 ## Main results
 
-* `measure_theory.measureabsolutely_continuous_iff_with_density_radon_nikodym_derive_eq` :
+* `measure_theory.measure.absolutely_continuous_iff_with_density_radon_nikodym_deriv_eq` :
   the Radon-Nikodym theorem
 
 ## Tags
@@ -60,7 +60,7 @@ end
 /-- **The Radon-Nikodym theorem**: Given two measures `μ` and `ν`, if
 `have_lebesgue_decomposition μ ν`, then `μ` is absolutely continuous to `ν` if and only if
 `ν.with_density (radon_nikodym_deriv μ ν) = μ`. -/
-theorem absolutely_continuous_iff_with_density_radon_nikodym_derive_eq
+theorem absolutely_continuous_iff_with_density_radon_nikodym_deriv_eq
   {μ ν : measure α} [have_lebesgue_decomposition μ ν] :
   μ ≪ ν ↔ ν.with_density (radon_nikodym_deriv μ ν) = μ :=
 ⟨with_density_radon_nikodym_deriv_eq μ ν, λ h, h ▸ with_density_absolutely_continuous _ _⟩

src/measure_theory/integral/lebesgue.lean

@@ -1894,6 +1894,24 @@ begin
   simp [with_density_apply _ hs],
 end
 
+lemma with_density_tsum {f : ℕ → α → ℝ≥0∞} (h : ∀ i, measurable (f i)) :
+  μ.with_density (∑' n, f n) = sum (λ n, μ.with_density (f n)) :=
+begin
+  ext1 s hs,
+  simp_rw [sum_apply _ hs, with_density_apply _ hs],
+  change ∫⁻ x in s, (∑' n, f n) x ∂μ = ∑' (i : ℕ), ∫⁻ x, f i x ∂(μ.restrict s),
+  rw ← lintegral_tsum h,
+  refine lintegral_congr (λ x, tsum_apply (pi.summable.2 (λ _, ennreal.summable))),
+end
+
+lemma with_density_indicator {s : set α} (hs : measurable_set s) (f : α → ℝ≥0∞) :
+  μ.with_density (s.indicator f) = (μ.restrict s).with_density f :=
+begin
+  ext1 t ht,
+  rw [with_density_apply _ ht, lintegral_indicator _ hs,
+      restrict_comm hs ht, ← with_density_apply _ ht]
+end
+
 end lintegral
 
 end measure_theory

src/measure_theory/measure/measure_space.lean

@@ -1089,6 +1089,16 @@ ext $ λ s hs, by simp [hs, tsum_fintype]
   (sum μ).restrict s = sum (λ i, (μ i).restrict s) :=
 ext $ λ t ht, by simp only [sum_apply, restrict_apply, ht, ht.inter hs]
 
+lemma sum_congr {μ ν : ℕ → measure α} (h : ∀ n, μ n = ν n) : sum μ = sum ν :=
+by { congr, ext1 n, exact h n }
+
+lemma sum_add_sum (μ ν : ℕ → measure α) : sum μ + sum ν = sum (λ n, μ n + ν n) :=
+begin
+  ext1 s hs,
+  simp only [add_apply, sum_apply _ hs, pi.add_apply, coe_add,
+             tsum_add ennreal.summable ennreal.summable],
+end
+
 omit m0
 end sum