feat(measure_theory): absolute continuity of the integral (#5743)

### API changes:

#### `ennreal`s and `nnreal`s:

* `ennreal.mul_le_mul` and `ennreal.mul_lt_mul` are now `mono` lemmas;
* rename `ennreal.sub_lt_sub_self` to `ennreal.sub_lt_self`: there is no `-` in the RHS;
* new lemmas `enrneal.mul_div_le`, `nnreal.sub_add_eq_max`, and `nnreal.add_sub_eq_max`;
* add new lemma `ennreal.bsupr_add`, use in in the proof of `ennreal.Sup_add`;

#### Complete lattice

* new lemma `supr_lt_iff`;

#### Simple functions

* new lemmas `simple_func.exists_forall_le`, `simple_func.map_add`,
  `simple_func.sub_apply`;
* weaker typeclass assumptions in `simple_func.coe_sub`;
* `monotone_eapprox` is now a `mono` lemma;

#### Integration

* new lemmas `exists_simple_func_forall_lintegral_sub_lt_of_pos`,
  `exists_pos_set_lintegral_lt_of_measure_lt`,
  `tendsto_set_lintegral_zero`, and
  `has_finite_integral.tendsto_set_integral_nhds_zero`.

src/data/real/ennreal.lean

@@ -525,10 +525,10 @@ end complete_lattice
 
 section mul
 
-lemma mul_le_mul : a ≤ b → c ≤ d → a * c ≤ b * d :=
+@[mono] lemma mul_le_mul : a ≤ b → c ≤ d → a * c ≤ b * d :=
 canonically_ordered_semiring.mul_le_mul
 
-lemma mul_lt_mul (ac : a < c) (bd : b < d) : a * b < c * d :=
+@[mono] lemma mul_lt_mul (ac : a < c) (bd : b < d) : a * b < c * d :=
 begin
   rcases lt_iff_exists_nnreal_btwn.1 ac with ⟨a', aa', a'c⟩,
   lift a to ℝ≥0 using ne_top_of_lt aa',
@@ -648,9 +648,7 @@ iff.intro
   (assume h : a - b ≤ c,
     calc a ≤ (a - b) + b : le_sub_add_self
       ... ≤ c + b : add_le_add_right h _)
-  (assume h : a ≤ c + b,
-    calc a - b ≤ (c + b) - b : sub_le_sub h (le_refl _)
-      ... ≤ c : Inf_le (le_refl (c + b)))
+  (assume h : a ≤ c + b, Inf_le h)
 
 protected lemma sub_le_iff_le_add' : a - b ≤ c ↔ a ≤ b + c :=
 add_comm c b ▸ ennreal.sub_le_iff_le_add
@@ -661,7 +659,7 @@ lemma sub_eq_of_add_eq : b ≠ ∞ → a + b = c → c - b = a :=
 protected lemma sub_le_of_sub_le (h : a - b ≤ c) : a - c ≤ b :=
 ennreal.sub_le_iff_le_add.2 $ by { rw add_comm, exact ennreal.sub_le_iff_le_add.1 h }
 
-protected lemma sub_lt_sub_self : a ≠ ∞ → a ≠ 0 → 0 < b → a - b < a :=
+protected lemma sub_lt_self : a ≠ ∞ → a ≠ 0 → 0 < b → a - b < a :=
 match a, b with
 | none, _ := by { have := none_eq_top, assume h, contradiction }
 | (some a), none := by {intros, simp only [none_eq_top, sub_infty, pos_iff_ne_zero], assumption}
@@ -803,7 +801,7 @@ assume x0, by simp [x0]
 
 lemma mem_Ioo_self_sub_add : x ≠ ∞ → x ≠ 0 → 0 < ε₁ → 0 < ε₂ → x ∈ Ioo (x - ε₁) (x + ε₂) :=
 assume xt x0 ε0 ε0',
-  ⟨ennreal.sub_lt_sub_self xt x0 ε0, lt_add_right (by rwa [lt_top_iff_ne_top]) ε0'⟩
+  ⟨ennreal.sub_lt_self xt x0 ε0, lt_add_right (by rwa [lt_top_iff_ne_top]) ε0'⟩
 
 end interval
 
@@ -1068,6 +1066,13 @@ by rw [div_def, mul_assoc, inv_mul_cancel h0 hI, mul_one]
 lemma mul_div_cancel' (h0 : a ≠ 0) (hI : a ≠ ∞) : a * (b / a) = b :=
 by rw [mul_comm, mul_div_cancel h0 hI]
 
+lemma mul_div_le : a * (b / a) ≤ b :=
+begin
+  by_cases h0 : a = 0, { simp [h0] },
+  by_cases hI : a = ∞, { simp [hI] },
+  rw mul_div_cancel' h0 hI, exact le_refl b
+end
+
 lemma inv_two_add_inv_two : (2:ennreal)⁻¹ + 2⁻¹ = 1 :=
 by rw [← two_mul, ← div_def, div_self two_ne_zero two_ne_top]
 

src/data/real/nnreal.lean

@@ -481,8 +481,15 @@ nnreal.eq $ by rw [nnreal.coe_sub, nnreal.coe_add, add_sub_cancel]; exact le_add
 lemma add_sub_cancel' {r p : ℝ≥0} : (r + p) - r = p :=
 by rw [add_comm, add_sub_cancel]
 
+lemma sub_add_eq_max {r p : ℝ≥0} : (r - p) + p = max r p :=
+nnreal.eq $ by rw [sub_def, nnreal.coe_add, coe_max, nnreal.of_real, coe_mk,
+  ← max_add_add_right, zero_add, sub_add_cancel]
+
+lemma add_sub_eq_max {r p : ℝ≥0} : p + (r - p) = max p r :=
+by rw [add_comm, sub_add_eq_max, max_comm]
+
 @[simp] lemma sub_add_cancel_of_le {a b : ℝ≥0} (h : b ≤ a) : (a - b) + b = a :=
-nnreal.eq $ by rw [nnreal.coe_add, nnreal.coe_sub h, sub_add_cancel]
+by rw [sub_add_eq_max, max_eq_left h]
 
 lemma sub_sub_cancel_of_le {r p : ℝ≥0} (h : r ≤ p) : p - (p - r) = r :=
 by rw [nnreal.sub_def, nnreal.sub_def, nnreal.coe_of_real _ $ sub_nonneg.2 h,

src/measure_theory/bochner_integration.lean

@@ -1079,6 +1079,28 @@ lemma integral_eq_zero_of_ae {f : α → E} (hf : f =ᵐ[μ] 0) : ∫ a, f a ∂
 if hfm : ae_measurable f μ then by simp [integral_congr_ae hf, integral_zero]
 else integral_non_ae_measurable hfm
 
+/-- If `f` has finite integral, then `∫ x in s, f x ∂μ` is absolutely continuous in `s`: it tends
+to zero as `μ s` tends to zero. -/
+lemma has_finite_integral.tendsto_set_integral_nhds_zero {ι} {f : α → E}
+  (hf : has_finite_integral f μ) {l : filter ι} {s : ι → set α}
+  (hs : tendsto (μ ∘ s) l (𝓝 0)) :
+  tendsto (λ i, ∫ x in s i, f x ∂μ) l (𝓝 0) :=
+begin
+  rw [tendsto_zero_iff_norm_tendsto_zero],
+  simp_rw [← coe_nnnorm, ← nnreal.coe_zero, nnreal.tendsto_coe, ← ennreal.tendsto_coe,
+    ennreal.coe_zero],
+  exact tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
+    (tendsto_set_lintegral_zero hf hs) (λ i, zero_le _)
+    (λ i, ennnorm_integral_le_lintegral_ennnorm _)
+end
+
+/-- If `f` is integrable, then `∫ x in s, f x ∂μ` is absolutely continuous in `s`: it tends
+to zero as `μ s` tends to zero. -/
+lemma integrable.tendsto_set_integral_nhds_zero {ι} {f : α → E}
+  (hf : integrable f μ) {l : filter ι} {s : ι → set α} (hs : tendsto (μ ∘ s) l (𝓝 0)) :
+  tendsto (λ i, ∫ x in s i, f x ∂μ) l (𝓝 0) :=
+hf.2.tendsto_set_integral_nhds_zero hs
+
 /-- If `F i → f` in `L1`, then `∫ x, F i x ∂μ → ∫ x, f x∂μ`. -/
 lemma tendsto_integral_of_l1 {ι} (f : α → E) (hfi : integrable f μ)
   {F : ι → α → E} {l : filter ι} (hFi : ∀ᶠ i in l, integrable (F i) μ)

src/measure_theory/content.lean

@@ -90,7 +90,7 @@ begin
   have h'ε := ennreal.zero_lt_coe_iff.2 hε,
   cases le_or_lt (inner_content μ U) ε,
   { exact ⟨⊥, empty_subset _, le_trans h (le_add_of_nonneg_left (zero_le _))⟩ },
-  have := ennreal.sub_lt_sub_self (ne_of_lt hU) (ne_of_gt $ lt_trans h'ε h) h'ε,
+  have := ennreal.sub_lt_self (ne_of_lt hU) (ne_of_gt $ lt_trans h'ε h) h'ε,
   conv at this {to_rhs, rw inner_content }, simp only [lt_supr_iff] at this,
   rcases this with ⟨U, h1U, h2U⟩, refine ⟨U, h1U, _⟩,
   rw [← ennreal.sub_le_iff_le_add], exact le_of_lt h2U

src/measure_theory/integration.lean

@@ -95,6 +95,10 @@ by simpa only [mem_range, exists_prop] using set.exists_range_iff
 lemma preimage_eq_empty_iff (f : α →ₛ β) (b : β) : f ⁻¹' {b} = ∅ ↔ b ∉ f.range :=
 preimage_singleton_eq_empty.trans $ not_congr mem_range.symm
 
+lemma exists_forall_le [nonempty β] [directed_order β] (f : α →ₛ β) :
+  ∃ C, ∀ x, f x ≤ C :=
+f.range.exists_le.imp $ λ C, forall_range_iff.1
+
 /-- Constant function as a `simple_func`. -/
 def const (α) {β} [measurable_space α] (b : β) : α →ₛ β :=
 ⟨λ a, b, λ x, is_measurable.const _, finite_range_const⟩
@@ -275,6 +279,10 @@ rfl
 
 lemma const_mul_eq_map [has_mul β] (f : α →ₛ β) (b : β) : const α b * f = f.map (λa, b * a) := rfl
 
+theorem map_add [has_add β] [has_add γ] {g : β → γ}
+  (hg : ∀ x y, g (x + y) = g x + g y) (f₁ f₂ : α →ₛ β) : (f₁ + f₂).map g = f₁.map g + f₂.map g :=
+ext $ λ x, hg _ _
+
 instance [add_monoid β] : add_monoid (α →ₛ β) :=
 function.injective.add_monoid (λ f, show α → β, from f) coe_injective coe_zero coe_add
 
@@ -287,9 +295,11 @@ instance [has_neg β] : has_neg (α →ₛ β) := ⟨λf, f.map (has_neg.neg)⟩
 
 instance [has_sub β] : has_sub (α →ₛ β) := ⟨λf g, (f.map (has_sub.sub)).seq g⟩
 
-@[simp, norm_cast] lemma coe_sub [add_group β] (f g : α →ₛ β) : ⇑(f - g) = f - g :=
+@[simp, norm_cast] lemma coe_sub [has_sub β] (f g : α →ₛ β) : ⇑(f - g) = f - g :=
 rfl
 
+lemma sub_apply [has_sub β] (f g : α →ₛ β) (x : α) : (f - g) x = f x - g x := rfl
+
 instance [add_group β] : add_group (α →ₛ β) :=
 function.injective.add_group_sub (λ f, show α → β, from f) coe_injective
   coe_zero coe_add coe_neg coe_sub
@@ -496,7 +506,7 @@ by rw [ennreal_rat_embed, encodable.encodek]; refl
 def eapprox : (α → ennreal) → ℕ → α →ₛ ennreal :=
 approx ennreal_rat_embed
 
-lemma monotone_eapprox (f : α → ennreal) : monotone (eapprox f) :=
+@[mono] lemma monotone_eapprox (f : α → ennreal) : monotone (eapprox f) :=
 monotone_approx _ f
 
 lemma supr_eapprox_apply (f : α → ennreal) (hf : measurable f) (a : α) :
@@ -916,6 +926,24 @@ begin
     simp only [hx, le_top] }
 end
 
+lemma exists_simple_func_forall_lintegral_sub_lt_of_pos {f : α → ennreal} (h : ∫⁻ x, f x ∂μ < ⊤)
+  {ε : ennreal} (hε : 0 < ε) :
+  ∃ φ : α →ₛ ℝ≥0, (∀ x, ↑(φ x) ≤ f x) ∧ ∀ ψ : α →ₛ ℝ≥0, (∀ x, ↑(ψ x) ≤ f x) →
+    (map coe (ψ - φ)).lintegral μ < ε :=
+begin
+  rw lintegral_eq_nnreal at h,
+  have := ennreal.lt_add_right h hε,
+  erw ennreal.bsupr_add at this; [skip, exact ⟨0, λ x, by simp⟩],
+  simp_rw [lt_supr_iff, supr_lt_iff, supr_le_iff] at this,
+  rcases this with ⟨φ, hle : ∀ x, ↑(φ x) ≤ f x, b, hbφ, hb⟩,
+  refine ⟨φ, hle, λ ψ hψ, _⟩,
+  have : (map coe φ).lintegral μ < ⊤, from (le_bsupr φ hle).trans_lt h,
+  rw [← add_lt_add_iff_left this, ← add_lintegral, ← map_add @ennreal.coe_add],
+  refine (hb _ (λ x, le_trans _ (max_le (hle x) (hψ x)))).trans_lt hbφ,
+  norm_cast,
+  simp only [add_apply, sub_apply, nnreal.add_sub_eq_max]
+end
+
 theorem supr_lintegral_le {ι : Sort*} (f : ι → α → ennreal) :
   (⨆i, ∫⁻ a, f i a ∂μ) ≤ (∫⁻ a, ⨆i, f i a ∂μ) :=
 begin
@@ -1054,11 +1082,57 @@ lemma set_lintegral_congr {f : α → ennreal} {s t : set α} (h : s =ᵐ[μ] t)
   ∫⁻ x in s, f x ∂μ = ∫⁻ x in t, f x ∂μ :=
 by rw [restrict_congr_set h]
 
+/-- If `f` has finite integral, then `∫⁻ x in s, f x ∂μ` is absolutely continuous in `s`: it tends
+to zero as `μ s` tends to zero. This lemma states states this fact in terms of `ε` and `δ`. -/
+lemma exists_pos_set_lintegral_lt_of_measure_lt {f : α → ennreal} (h : ∫⁻ x, f x ∂μ < ⊤)
+  {ε : ennreal} (hε : 0 < ε) :
+  ∃ δ > 0, ∀ s, μ s < δ → ∫⁻ x in s, f x ∂μ < ε :=
+begin
+  rcases exists_between hε with ⟨ε₂, hε₂0, hε₂ε⟩, rcases exists_between hε₂0 with ⟨ε₁, hε₁0, hε₁₂⟩,
+  rcases exists_simple_func_forall_lintegral_sub_lt_of_pos h hε₁0 with ⟨φ, hle, hφ⟩,
+  rcases φ.exists_forall_le with ⟨C, hC⟩,
+  use [(ε₂ - ε₁) / C, ennreal.div_pos_iff.2 ⟨(zero_lt_sub_iff_lt.2 hε₁₂).ne', ennreal.coe_ne_top⟩],
+  intros s hs,
+  simp only [lintegral_eq_nnreal, supr_lt_iff, supr_le_iff],
+  refine ⟨ε₂, hε₂ε, λ ψ hψ, _⟩,
+  calc (map coe ψ).lintegral (μ.restrict s)
+      ≤ (map coe φ).lintegral (μ.restrict s) + (map coe (ψ - φ)).lintegral (μ.restrict s) :
+    begin
+      rw [← simple_func.add_lintegral, ← simple_func.map_add @ennreal.coe_add],
+      refine simple_func.lintegral_mono (λ x, _) le_rfl,
+      simp [-ennreal.coe_add, nnreal.add_sub_eq_max, le_max_right]
+    end
+  ... ≤ (map coe φ).lintegral (μ.restrict s) + ε₁ :
+    begin
+      refine add_le_add le_rfl (le_trans _ (hφ _ hψ).le),
+      exact simple_func.lintegral_mono le_rfl measure.restrict_le_self
+    end
+  ... ≤ (simple_func.const α (C : ennreal)).lintegral (μ.restrict s) + ε₁ :
+    by { mono*, exacts [λ x, coe_le_coe.2 (hC x), le_rfl, le_rfl] }
+  ... = C * μ s + ε₁ : by simp [← simple_func.lintegral_eq_lintegral]
+  ... ≤ C * ((ε₂ - ε₁) / C) + ε₁ : by { mono*, exacts [le_rfl, hs.le, le_rfl] }
+  ... ≤ (ε₂ - ε₁) + ε₁ : add_le_add mul_div_le le_rfl
+  ... = ε₂ : sub_add_cancel_of_le hε₁₂.le,
+end
+
+/-- If `f` has finite integral, then `∫⁻ x in s, f x ∂μ` is absolutely continuous in `s`: it tends
+to zero as `μ s` tends to zero. -/
+lemma tendsto_set_lintegral_zero {ι} {f : α → ennreal} (h : ∫⁻ x, f x ∂μ < ⊤)
+  {l : filter ι} {s : ι → set α} (hl : tendsto (μ ∘ s) l (𝓝 0)) :
+  tendsto (λ i, ∫⁻ x in s i, f x ∂μ) l (𝓝 0) :=
+begin
+  simp only [ennreal.nhds_zero, tendsto_infi, tendsto_principal, mem_Iio, ← pos_iff_ne_zero]
+    at hl ⊢,
+  intros ε ε0,
+  rcases exists_pos_set_lintegral_lt_of_measure_lt h ε0 with ⟨δ, δ0, hδ⟩,
+  exact (hl δ δ0).mono (λ i, hδ _)
+end
+
 @[simp] lemma lintegral_add {f g : α → ennreal} (hf : measurable f) (hg : measurable g) :
   (∫⁻ a, f a + g a ∂μ) = (∫⁻ a, f a ∂μ) + (∫⁻ a, g a ∂μ) :=
 calc (∫⁻ a, f a + g a ∂μ) =
     (∫⁻ a, (⨆n, (eapprox f n : α → ennreal) a) + (⨆n, (eapprox g n : α → ennreal) a) ∂μ) :
-    by congr; funext a; rw [supr_eapprox_apply f hf, supr_eapprox_apply g hg]
+    by simp only [supr_eapprox_apply, hf, hg]
   ... = (∫⁻ a, (⨆n, (eapprox f n + eapprox g n : α → ennreal) a) ∂μ) :
   begin
     congr, funext a,

src/order/complete_lattice.lean

@@ -372,6 +372,9 @@ supr_le $ le_supr _ ∘ h
 @[simp] theorem supr_le_iff : supr s ≤ a ↔ (∀i, s i ≤ a) :=
 (is_lub_le_iff is_lub_supr).trans forall_range_iff
 
+theorem supr_lt_iff : supr s < a ↔ ∃ b < a, ∀ i, s i ≤ b :=
+⟨λ h, ⟨supr s, h, λ i, le_supr s i⟩, λ ⟨b, hba, hsb⟩, (supr_le hsb).trans_lt hba⟩
+
 theorem Sup_eq_supr {s : set α} : Sup s = (⨆a ∈ s, a) :=
 le_antisymm
   (Sup_le $ assume b h, le_supr_of_le b $ le_supr _ h)

src/topology/instances/ennreal.lean

@@ -339,18 +339,22 @@ by { apply tendsto.mul_const hm, simp [ha] }
 protected lemma tendsto_inv_nat_nhds_zero : tendsto (λ n : ℕ, (n : ennreal)⁻¹) at_top (𝓝 0) :=
 ennreal.inv_top ▸ ennreal.tendsto_inv_iff.2 tendsto_nat_nhds_top
 
+lemma bsupr_add {ι} {s : set ι} (hs : s.nonempty) {f : ι → ennreal} :
+  (⨆ i ∈ s, f i) + a = ⨆ i ∈ s, f i + a :=
+begin
+  simp only [← Sup_image], symmetry,
+  rw [image_comp (+ a)],
+  refine is_lub.Sup_eq (is_lub_of_is_lub_of_tendsto _ (is_lub_Sup _) (hs.image _) _),
+  exacts [λ x _ y _ hxy, add_le_add hxy le_rfl,
+    tendsto.add (tendsto_id' inf_le_left) tendsto_const_nhds]
+end
+
 lemma Sup_add {s : set ennreal} (hs : s.nonempty) : Sup s + a = ⨆b∈s, b + a :=
-have Sup ((λb, b + a) '' s) = Sup s + a,
-  from is_lub.Sup_eq (is_lub_of_is_lub_of_tendsto
-    (assume x _ y _ h, add_le_add h (le_refl _))
-    (is_lub_Sup s)
-    hs
-    (tendsto.add (tendsto_id' inf_le_left) tendsto_const_nhds)),
-by simp [Sup_image, -add_comm] at this; exact this.symm
+by rw [Sup_eq_supr, bsupr_add hs]
 
 lemma supr_add {ι : Sort*} {s : ι → ennreal} [h : nonempty ι] : supr s + a = ⨆b, s b + a :=
 let ⟨x⟩ := h in
-calc supr s + a = Sup (range s) + a : by simp [Sup_range]
+calc supr s + a = Sup (range s) + a : by rw Sup_range
   ... = (⨆b∈range s, b + a) : Sup_add ⟨s x, x, rfl⟩
   ... = _ : supr_range
 
@@ -459,15 +463,7 @@ protected lemma coe_tsum {f : α → ℝ≥0} : summable f → ↑(tsum f) = ∑
 | ⟨r, hr⟩ := by rw [hr.tsum_eq, ennreal.tsum_coe_eq hr]
 
 protected lemma has_sum : has_sum f (⨆s:finset α, ∑ a in s, f a) :=
-tendsto_order.2
-  ⟨assume a' ha',
-    let ⟨s, hs⟩ := lt_supr_iff.mp ha' in
-    mem_at_top_sets.mpr ⟨s, assume t ht, lt_of_lt_of_le hs $ finset.sum_le_sum_of_subset ht⟩,
-  assume a' ha',
-    univ_mem_sets' $ assume s,
-    have ∑ a in s, f a ≤ ⨆(s : finset α), ∑ a in s, f a,
-      from le_supr (λ(s : finset α), ∑ a in s, f a) s,
-    lt_of_le_of_lt this ha'⟩
+tendsto_at_top_supr $ λ s t, finset.sum_le_sum_of_subset
 
 @[simp] protected lemma summable : summable f := ⟨_, ennreal.has_sum⟩