feat(measure_theory/integration): in a sigma finite space, there exis…

…ts an integrable positive function (#7721)

src/measure_theory/borel_space.lean

@@ -1115,6 +1115,13 @@ 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) }
 
+lemma measurable.nnreal_tsum {ι} [encodable ι] {f : ι → α → ℝ≥0} (h : ∀ i, measurable (f i)) :
+  measurable (λ x, ∑' i, f i x) :=
+begin
+  simp_rw [nnreal.tsum_eq_to_nnreal_tsum],
+  exact (measurable.ennreal_tsum (λ i, (h i).ennreal_coe)).to_nnreal,
+end
+
 lemma ae_measurable.ennreal_tsum {ι} [encodable ι] {f : ι → α → ℝ≥0∞} {μ : measure α}
   (h : ∀ i, ae_measurable (f i) μ) :
   ae_measurable (λ x, ∑' i, f i x) μ :=

src/measure_theory/integration.lean

@@ -1804,4 +1804,60 @@ begin
     simp [lintegral_supr, ennreal.mul_supr, h_mf.mul (h_mea_g _), *] }
 end
 
+/-- In a sigma-finite measure space, there exists an integrable function which is
+positive everywhere (and with an arbitrarily small integral). -/
+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).ennreal_coe)
+    ... = ∑' 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] }
+end
+
 end measure_theory

src/topology/algebra/infinite_sum.lean

@@ -864,6 +864,10 @@ has_sum_lt h hi hf.has_sum hg.has_sum
   ∑' n, f n < ∑' n, g n :=
 let ⟨hle, i, hi⟩ := pi.lt_def.mp h in tsum_lt_tsum hle hi hf hg
 
+lemma tsum_pos (hsum : summable g) (hg : ∀ b, 0 ≤ g b) (i : β) (hi : 0 < g i) :
+  0 < ∑' b, g b :=
+by { rw ← tsum_zero, exact tsum_lt_tsum hg hi summable_zero hsum }
+
 end ordered_topological_group
 
 section canonically_ordered

src/topology/instances/ennreal.lean

@@ -650,6 +650,16 @@ namespace nnreal
 
 open_locale nnreal
 
+lemma tsum_eq_to_nnreal_tsum {f : β → ℝ≥0} :
+  (∑' b, f b) = (∑' b, (f b : ℝ≥0∞)).to_nnreal :=
+begin
+  by_cases h : summable f,
+  { rw [← ennreal.coe_tsum h, ennreal.to_nnreal_coe] },
+  { have A := tsum_eq_zero_of_not_summable h,
+    simp only [← ennreal.tsum_coe_ne_top_iff_summable, not_not] at h,
+    simp only [h, ennreal.top_to_nnreal, A] }
+end
+
 /-- Comparison test of convergence of `ℝ≥0`-valued series. -/
 lemma exists_le_has_sum_of_le {f g : β → ℝ≥0} {r : ℝ≥0}
   (hgf : ∀b, g b ≤ f b) (hfr : has_sum f r) : ∃p≤r, has_sum g p :=
@@ -743,6 +753,31 @@ begin
   norm_cast,
 end
 
+lemma has_sum_lt {f g : α → ℝ≥0} {sf sg : ℝ≥0} {i : α} (h : ∀ (a : α), f a ≤ g a) (hi : f i < g i)
+  (hf : has_sum f sf) (hg : has_sum g sg) : sf < sg :=
+begin
+  have A : ∀ (a : α), (f a : ℝ) ≤ g a := λ a, nnreal.coe_le_coe.2 (h a),
+  have : (sf : ℝ) < sg :=
+    has_sum_lt A (nnreal.coe_lt_coe.2 hi) (has_sum_coe.2 hf) (has_sum_coe.2 hg),
+  exact nnreal.coe_lt_coe.1 this
+end
+
+@[mono] lemma has_sum_strict_mono
+  {f g : α → ℝ≥0} {sf sg : ℝ≥0} (hf : has_sum f sf) (hg : has_sum g sg) (h : f < g) : sf < sg :=
+let ⟨hle, i, hi⟩ := pi.lt_def.mp h in has_sum_lt hle hi hf hg
+
+lemma tsum_lt_tsum {f g : α → ℝ≥0} {i : α} (h : ∀ (a : α), f a ≤ g a) (hi : f i < g i)
+  (hg : summable g) : ∑' n, f n < ∑' n, g n :=
+has_sum_lt h hi (summable_of_le h hg).has_sum hg.has_sum
+
+@[mono] lemma tsum_strict_mono {f g : α → ℝ≥0} (hg : summable g) (h : f < g) :
+  ∑' n, f n < ∑' n, g n :=
+let ⟨hle, i, hi⟩ := pi.lt_def.mp h in tsum_lt_tsum hle hi hg
+
+lemma tsum_pos {g : α → ℝ≥0} (hg : summable g) (i : α) (hi : 0 < g i) :
+  0 < ∑' b, g b :=
+by { rw ← tsum_zero, exact tsum_lt_tsum (λ a, zero_le _) hi hg }
+
 end nnreal
 
 namespace ennreal