refactor(measure_theory/integral/lebesgue): golf a proof (#9206)

* add `exists_pos_tsum_mul_lt_of_encodable`;
* add `measure.spanning_sets_index` and lemmas about this definition;
* replace the proof of `exists_integrable_pos_of_sigma_finite` with a simpler one.

src/analysis/specific_limits.lean

@@ -950,6 +950,20 @@ theorem exists_pos_sum_of_encodable' {ε : ℝ≥0∞} (hε : 0 < ε) (ι) [enco
 let ⟨δ, δpos, hδ⟩ := exists_pos_sum_of_encodable hε ι in
   ⟨λ i, δ i, λ i, ennreal.coe_pos.2 (δpos i), hδ⟩
 
+theorem exists_pos_tsum_mul_lt_of_encodable {ε : ℝ≥0∞} (hε : 0 < ε) {ι} [encodable ι]
+  (w : ι → ℝ≥0∞) (hw : ∀ i, w i ≠ ∞) :
+  ∃ δ : ι → ℝ≥0, (∀ i, 0 < δ i) ∧ ∑' i, (w i * δ i : ℝ≥0∞) < ε :=
+begin
+  lift w to ι → ℝ≥0 using hw,
+  rcases exists_pos_sum_of_encodable hε ι with ⟨δ', Hpos, Hsum⟩,
+  have : ∀ i, 0 < max 1 (w i), from λ i, zero_lt_one.trans_le (le_max_left _ _),
+  refine ⟨λ i, δ' i / max 1 (w i), λ i, nnreal.div_pos (Hpos _) (this i), _⟩,
+  refine lt_of_le_of_lt (ennreal.tsum_le_tsum $ λ i, _) Hsum,
+  rw [coe_div (this i).ne'],
+  refine mul_le_of_le_div' (ennreal.mul_le_mul le_rfl $ ennreal.inv_le_inv.2 _),
+  exact coe_le_coe.2 (le_max_right _ _)
+end
+
 end ennreal
 
 /-!

src/measure_theory/integral/lebesgue.lean

@@ -2022,54 +2022,20 @@ lemma exists_integrable_pos_of_sigma_finite
   {α} [measurable_space α] (μ : measure α) [sigma_finite μ] {ε : ℝ≥0} (εpos : 0 < ε) :
   ∃ g : α → ℝ≥0, (∀ x, 0 < g x) ∧ measurable g ∧ (∫⁻ x, g x ∂μ < ε) :=
 begin
-  /- The desired function is almost `∑' n, indicator (s n) * δ n / μ (s n)` where `s n` is any
-    sequence of finite measure sets covering the whole space, which exists by sigma-finiteness,
-    and `δ n` is any summable sequence with sum at most `ε`.
-    The only problem with this definition is that `μ (s n)` might be small, so it is not guaranteed
-    that this series converges everywhere (although it does almost everywhere, as its integral is
-    `∑ n, δ n`). We solve this by using instead `∑' n, indicator (s n) * δ n / max (1, μ (s n))` -/
-  obtain ⟨δ, δpos, ⟨cδ, δsum, c_lt⟩⟩ :
-    ∃ δ : ℕ → ℝ≥0, (∀ i, 0 < δ i) ∧ ∃ (c : ℝ≥0), has_sum δ c ∧ c < ε :=
-    nnreal.exists_pos_sum_of_encodable εpos ℕ,
-  set s := spanning_sets μ with hs,
-  have I : ∀ n, 0 < max 1 (μ (s n)).to_nnreal := λ n, zero_lt_one.trans_le (le_max_left _ _),
-  let ρ := λ n, δ n / max 1 (μ (s n)).to_nnreal,
-  let g := λ x, ∑' n, ((s n).indicator (λ x, ρ n) x),
-  have A : summable ρ,
-  { apply nnreal.summable_of_le (λ n, _) δsum.summable,
-    rw nnreal.div_le_iff (I n).ne',
-    conv_lhs { rw ← mul_one (δ n) },
-    exact mul_le_mul (le_refl _) (le_max_left _ _) bot_le bot_le },
-  have B : ∀ x, summable (λ n, (s n).indicator (λ x, ρ n) x),
-  { assume x,
-    apply nnreal.summable_of_le (λ n, _) A,
-    simp only [set.indicator],
-    split_ifs,
-    { exact le_refl _ },
-    { exact bot_le } },
-  have M : ∀ n, measurable ((s n).indicator (λ x, ρ n)) :=
-    λ n, measurable_const.indicator (measurable_spanning_sets μ n),
-  refine ⟨g, λ x, _, measurable.nnreal_tsum M, _⟩,
-  { have : x ∈ (⋃ n, s n), by { rw [hs, Union_spanning_sets], exact set.mem_univ _ },
-    rcases set.mem_Union.1 this with ⟨n, hn⟩,
-    simp only [nnreal.tsum_pos (B x) n, hn, set.indicator_of_mem, nnreal.div_pos (δpos n) (I n)] },
-  { calc ∫⁻ (x : α), (g x) ∂μ
-        = ∫⁻ x, ∑' n, (((s n).indicator (λ x, ρ n) x : ℝ≥0) : ℝ≥0∞) ∂μ :
-      by { apply lintegral_congr (λ x, _), simp_rw [g, ennreal.coe_tsum (B x)] }
-    ... = ∑' n, ∫⁻ x, (((s n).indicator (λ x, ρ n) x : ℝ≥0) : ℝ≥0∞) ∂μ :
-      lintegral_tsum (λ n, (M n).coe_nnreal_ennreal)
-    ... = ∑' n, μ (s n) * ρ n :
-      by simp only [measurable_spanning_sets μ, lintegral_const, measurable_set.univ, mul_comm,
-                    lintegral_indicator, univ_inter, coe_indicator, measure.restrict_apply]
-    ... ≤ ∑' n, δ n :
-      begin
-        apply ennreal.tsum_le_tsum (λ n, _),
-        rw [ennreal.coe_div (I n).ne', ← mul_div_assoc, mul_comm, ennreal.coe_max],
-        apply ennreal.div_le_of_le_mul (ennreal.mul_le_mul (le_refl _) _),
-        convert le_max_right _ _,
-        exact ennreal.coe_to_nnreal (measure_spanning_sets_lt_top μ n).ne
-      end
-    ... < ε : by rwa [← ennreal.coe_tsum δsum.summable, ennreal.coe_lt_coe, δsum.tsum_eq] }
+  /- Let `s` be a covering of `α` by pairwise disjoint measurable sets of finite measure. Let
+  `δ : ℕ → ℝ≥0` be a positive function such that `∑' i, μ (s i) * δ i < ε`. Then the function that
+   is equal to `δ n` on `s n` is a positive function with integral less than `ε`. -/
+  set s : ℕ → set α := disjointed (spanning_sets μ),
+  have : ∀ n, μ (s n) < ∞,
+    from λ n, (measure_mono $ disjointed_subset _ _).trans_lt (measure_spanning_sets_lt_top μ n),
+  obtain ⟨δ, δpos, δsum⟩ : ∃ δ : ℕ → ℝ≥0, (∀ i, 0 < δ i) ∧ ∑' i, μ (s i) * δ i < ε,
+    from ennreal.exists_pos_tsum_mul_lt_of_encodable (ennreal.coe_pos.2 εpos) _ (λ n, (this n).ne),
+  set N : α → ℕ := spanning_sets_index μ,
+  have hN_meas : measurable N := measurable_spanning_sets_index μ,
+  have hNs : ∀ n, N ⁻¹' {n} = s n := preimage_spanning_sets_index_singleton μ,
+  refine ⟨δ ∘ N, λ x, δpos _, measurable_from_nat.comp hN_meas, _⟩,
+  simpa [lintegral_comp measurable_from_nat.coe_nnreal_ennreal hN_meas, hNs,
+    lintegral_encodable, measurable_spanning_sets_index, mul_comm] using δsum,
 end
 
 lemma lintegral_trim {α : Type*} {m m0 : measurable_space α} {μ : measure α} (hm : m ≤ m0)

src/measure_theory/measure/measure_space.lean

@@ -1826,6 +1826,30 @@ lemma is_countably_spanning_spanning_sets (μ : measure α) [sigma_finite μ] :
   is_countably_spanning (range (spanning_sets μ)) :=
 ⟨spanning_sets μ, mem_range_self, Union_spanning_sets μ⟩
 
+/-- `spanning_sets_index μ x` is the least `n : ℕ` such that `x ∈ spanning_sets μ n`. -/
+def spanning_sets_index (μ : measure α) [sigma_finite μ] (x : α) : ℕ :=
+nat.find $ Union_eq_univ_iff.1 (Union_spanning_sets μ) x
+
+lemma measurable_spanning_sets_index (μ : measure α) [sigma_finite μ] :
+  measurable (spanning_sets_index μ) :=
+measurable_find _ $ measurable_spanning_sets μ
+
+lemma preimage_spanning_sets_index_singleton (μ : measure α) [sigma_finite μ] (n : ℕ) :
+  spanning_sets_index μ ⁻¹' {n} = disjointed (spanning_sets μ) n :=
+preimage_find_eq_disjointed _ _ _
+
+lemma spanning_sets_index_eq_iff (μ : measure α) [sigma_finite μ] {x : α} {n : ℕ} :
+  spanning_sets_index μ x = n ↔ x ∈ disjointed (spanning_sets μ) n :=
+by convert set.ext_iff.1 (preimage_spanning_sets_index_singleton μ n) x
+
+lemma mem_disjointed_spanning_sets_index (μ : measure α) [sigma_finite μ] (x : α) :
+  x ∈ disjointed (spanning_sets μ) (spanning_sets_index μ x) :=
+(spanning_sets_index_eq_iff μ).1 rfl
+
+lemma mem_spanning_sets_index (μ : measure α) [sigma_finite μ] (x : α) :
+  x ∈ spanning_sets μ (spanning_sets_index μ x) :=
+disjointed_subset _ _ (mem_disjointed_spanning_sets_index μ x)
+
 omit m0
 
 namespace measure

src/order/disjointed.lean

@@ -160,3 +160,8 @@ supr_disjointed f
 lemma disjointed_eq_inter_compl (f : ℕ → set α) (n : ℕ) :
   disjointed f n = f n ∩ (⋂ i < n, (f i)ᶜ) :=
 disjointed_eq_inf_compl f n
+
+lemma preimage_find_eq_disjointed (s : ℕ → set α) (H : ∀ x, ∃ n, x ∈ s n)
+  [∀ x n, decidable (x ∈ s n)] (n : ℕ) :
+  (λ x, nat.find (H x)) ⁻¹' {n} = disjointed s n :=
+by { ext x, simp [nat.find_eq_iff, disjointed_eq_inter_compl] }