feat(measure_theory/interval_integral): strong version of FTC-2 (#7978)

The equality `∫ y in a..b, f' y = f b - f a` is currently proved in mathlib assuming that `f'` is continuous. We weaken the assumption, assuming only that `f'` is integrable.

Author: sgouezel

archive/100-theorems-list/9_area_of_a_circle.lean

@@ -79,7 +79,7 @@ begin
   have hf : continuous f := by continuity,
   suffices : ∫ x in -r..r, 2 * f x = nnreal.pi * r ^ 2,
   { have h : integrable_on f (Ioc (-r) r) :=
-      (hf.integrable_on_compact is_compact_Icc).mono_set Ioc_subset_Icc_self,
+      hf.integrable_on_Icc.mono_set Ioc_subset_Icc_self,
     calc  volume (disc r)
         = volume (region_between (λ x, -f x) f (Ioc (-r) r)) : by rw disc_eq_region_between
     ... = ennreal.of_real (∫ x in Ioc (-r:ℝ) r, (f - has_neg.neg ∘ f) x) :
@@ -108,8 +108,8 @@ begin
                    ... = 1 : inv_mul_cancel hlt.ne' },
     { nlinarith } },
   have hcont := (by continuity : continuous F).continuous_on,
-  have hcont' := (continuous_const.mul hf).continuous_on,
   calc  ∫ x in -r..r, 2 * f x
-      = F r - F (-r) : integral_eq_sub_of_has_deriv_at'_of_le (neg_le_self r.2) hcont hderiv hcont'
+      = F r - F (-r) : integral_eq_sub_of_has_deriv_at_of_le (neg_le_self r.2)
+                         hcont hderiv (continuous_const.mul hf).continuous_on.interval_integrable
   ... = nnreal.pi * r ^ 2 : by norm_num [F, inv_mul_cancel hlt.ne', ← mul_div_assoc, mul_comm π],
 end

src/analysis/special_functions/integrals.lean

@@ -232,8 +232,10 @@ lemma integral_log (h : (0:ℝ) ∉ interval a b) :
 begin
   obtain ⟨h', heq⟩ := ⟨λ x hx, ne_of_mem_of_not_mem hx h, λ x hx, mul_inv_cancel (h' x hx)⟩,
   convert integral_mul_deriv_eq_deriv_mul (λ x hx, has_deriv_at_log (h' x hx))
-    (λ x hx, has_deriv_at_id x) (continuous_on_inv'.mono $ subset_compl_singleton_iff.mpr h)
-      continuous_on_const using 1; simp [integral_congr heq, mul_comm, ← sub_add],
+      (λ x hx, has_deriv_at_id x)
+      (continuous_on_inv'.mono $ subset_compl_singleton_iff.mpr h).interval_integrable
+      continuous_on_const.interval_integrable using 1;
+    simp [integral_congr heq, mul_comm, ← sub_add],
 end
 
 @[simp]
@@ -257,7 +259,8 @@ by rw integral_deriv_eq_sub'; norm_num [continuous_on_cos]
 lemma integral_cos_sq_sub_sin_sq :
   ∫ x in a..b, cos x ^ 2 - sin x ^ 2 = sin b * cos b - sin a * cos a :=
 by simpa only [sq, sub_eq_add_neg, neg_mul_eq_mul_neg] using integral_deriv_mul_eq_sub
-  (λ x hx, has_deriv_at_sin x) (λ x hx, has_deriv_at_cos x) continuous_on_cos continuous_on_sin.neg
+  (λ x hx, has_deriv_at_sin x) (λ x hx, has_deriv_at_cos x) continuous_on_cos.interval_integrable
+  continuous_on_sin.neg.interval_integrable
 
 @[simp]
 lemma integral_inv_one_add_sq : ∫ x : ℝ in a..b, (1 + x^2)⁻¹ = arctan b - arctan a :=
@@ -293,7 +296,7 @@ begin
                                                                           ← pow_add, add_comm]
   ... = C + (n + 1) * (∫ x in a..b, sin x ^ n) - (n + 1) * ∫ x in a..b, sin x ^ (n + 2) :
     by rw [integral_sub, mul_sub, add_sub_assoc]; apply continuous.interval_integrable; continuity,
-  all_goals { apply continuous.continuous_on, continuity },
+  all_goals { apply continuous.interval_integrable, continuity },
 end
 
 /-- The reduction formula for the integral of `sin x ^ n` for any natural `n ≥ 2`. -/
@@ -361,7 +364,7 @@ begin
                                                                           ← pow_add, add_comm]
   ... = C + (n + 1) * (∫ x in a..b, cos x ^ n) - (n + 1) * ∫ x in a..b, cos x ^ (n + 2) :
     by rw [integral_sub, mul_sub, add_sub_assoc]; apply continuous.interval_integrable; continuity,
-  all_goals { apply continuous.continuous_on, continuity },
+  all_goals { apply continuous.interval_integrable, continuity },
 end
 
 /-- The reduction formula for the integral of `cos x ^ n` for any natural `n ≥ 2`. -/

src/measure_theory/integral/integrable_on.lean

@@ -384,28 +384,42 @@ begin
   { apply_instance }
 end
 
-lemma measure_theory.integrable_on.mul_continuous_on
-  [topological_space α] [opens_measurable_space α] [t2_space α]
-  {μ : measure α} {s : set α} {f g : α → ℝ}
-  (hf : integrable_on f s μ) (hg : continuous_on g s) (hs : is_compact s) :
+section
+variables [topological_space α] [opens_measurable_space α]
+  {μ : measure α} {s t : set α} {f g : α → ℝ}
+
+lemma measure_theory.integrable_on.mul_continuous_on_of_subset
+  (hf : integrable_on f s μ) (hg : continuous_on g t)
+  (hs : measurable_set s) (ht : is_compact t) (hst : s ⊆ t) :
   integrable_on (λ x, f x * g x) s μ :=
 begin
-  rcases is_compact.exists_bound_of_continuous_on hs hg with ⟨C, hC⟩,
+  rcases is_compact.exists_bound_of_continuous_on ht hg with ⟨C, hC⟩,
   rw [integrable_on, ← mem_ℒp_one_iff_integrable] at hf ⊢,
   have : ∀ᵐ x ∂(μ.restrict s), ∥f x * g x∥ ≤ C * ∥f x∥,
-  { filter_upwards [ae_restrict_mem hs.measurable_set],
+  { filter_upwards [ae_restrict_mem hs],
     assume x hx,
     rw [real.norm_eq_abs, abs_mul, mul_comm, real.norm_eq_abs],
-    apply mul_le_mul_of_nonneg_right (hC x hx) (abs_nonneg _) },
-  exact mem_ℒp.of_le_mul hf (hf.ae_measurable.mul (hg.ae_measurable hs.measurable_set)) this
+    apply mul_le_mul_of_nonneg_right (hC x (hst hx)) (abs_nonneg _) },
+  exact mem_ℒp.of_le_mul hf (hf.ae_measurable.mul ((hg.mono hst).ae_measurable hs)) this,
 end
 
-lemma measure_theory.integrable_on.continuous_on_mul
-  [topological_space α] [opens_measurable_space α] [t2_space α]
-  {μ : measure α} {s : set α} {f g : α → ℝ}
+lemma measure_theory.integrable_on.mul_continuous_on [t2_space α]
+  (hf : integrable_on f s μ) (hg : continuous_on g s) (hs : is_compact s) :
+  integrable_on (λ x, f x * g x) s μ :=
+hf.mul_continuous_on_of_subset hg hs.measurable_set hs (subset.refl _)
+
+lemma measure_theory.integrable_on.continuous_on_mul_of_subset
+  (hf : integrable_on f s μ) (hg : continuous_on g t)
+  (hs : measurable_set s) (ht : is_compact t) (hst : s ⊆ t) :
+  integrable_on (λ x, g x * f x) s μ :=
+by simpa [mul_comm] using hf.mul_continuous_on_of_subset hg hs ht hst
+
+lemma measure_theory.integrable_on.continuous_on_mul [t2_space α]
   (hf : integrable_on f s μ) (hg : continuous_on g s) (hs : is_compact s) :
   integrable_on (λ x, g x * f x) s μ :=
-by simpa [mul_comm] using hf.mul_continuous_on hg hs
+hf.continuous_on_mul_of_subset hg hs.measurable_set hs (subset.refl _)
+
+end
 
 section monotone