feat(measure_theory/integral/interval_integral): integrability of non…

…negative derivatives on open intervals (#14147)

Shows that derivatives of continuous functions are integrable when nonnegative.



Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
Co-authored-by: loefflerd <d.loeffler.01@cantab.net>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/analysis/special_functions/integrals.lean

@@ -5,6 +5,7 @@ Authors: Benjamin Davidson
 -/
 import measure_theory.integral.interval_integral
 import analysis.special_functions.trigonometric.arctan_deriv
+import measure_theory.integral.integral_eq_improper
 
 /-!
 # Integration of specific interval integrals
@@ -52,6 +53,32 @@ lemma interval_integrable_rpow {r : ℝ} (h : 0 ≤ r ∨ (0 : ℝ) ∉ [a, b])
   interval_integrable (λ x, x ^ r) μ a b :=
 (continuous_on_id.rpow_const $ λ x hx, h.symm.imp (ne_of_mem_of_not_mem hx) id).interval_integrable
 
+/-- Alternative version with a weaker hypothesis on `r`, but assuming the measure is volume. -/
+lemma interval_integrable_rpow' {r : ℝ} (h : -1 < r) :
+  interval_integrable (λ x, x ^ r) volume a b :=
+begin
+  suffices : ∀ (c : ℝ), interval_integrable (λ x, x ^ r) volume 0 c,
+  { exact interval_integrable.trans (this a).symm (this b) },
+  have : ∀ (c : ℝ), (0 ≤ c) → interval_integrable (λ x, x ^ r) volume 0 c,
+  { intros c hc,
+    rw [interval_integrable_iff, interval_oc_of_le hc],
+    have hderiv : ∀ x ∈ Ioo 0 c, has_deriv_at (λ x : ℝ, x ^ (r + 1) / (r + 1)) (x ^ r) x,
+    { intros x hx, convert (real.has_deriv_at_rpow_const (or.inl hx.1.ne')).div_const (r + 1),
+      field_simp [(by linarith : r + 1 ≠ 0)], ring, },
+    apply integrable_on_deriv_of_nonneg hc _ hderiv,
+    { intros x hx, apply rpow_nonneg_of_nonneg hx.1.le, },
+    { refine (continuous_on_id.rpow_const _).div_const, intros x hx, right, linarith } },
+  intro c, rcases le_total 0 c with hc|hc,
+  { exact this c hc },
+  { rw [interval_integrable.iff_comp_neg, neg_zero],
+    have m := (this (-c) (by linarith)).smul (cos (r * π)),
+    rw interval_integrable_iff at m ⊢,
+    refine m.congr_fun _ measurable_set_Ioc, intros x hx,
+    rw interval_oc_of_le (by linarith : 0 ≤ -c) at hx,
+    simp only [pi.smul_apply, algebra.id.smul_eq_mul, log_neg_eq_log, mul_comm,
+      rpow_def_of_pos hx.1, rpow_def_of_neg (by linarith [hx.1] : -x < 0)], }
+end
+
 @[simp]
 lemma interval_integrable_id : interval_integrable (λ x, x) μ a b :=
 continuous_id.interval_integrable a b
@@ -172,28 +199,43 @@ open interval_integral
 
 /-! ### Integrals of simple functions -/
 
-lemma integral_rpow {r : ℝ} (h : 0 ≤ r ∨ r ≠ -1 ∧ (0 : ℝ) ∉ [a, b]) :
+lemma integral_rpow {r : ℝ} (h : -1 < r ∨ (r ≠ -1 ∧ (0 : ℝ) ∉ [a, b])) :
   ∫ x in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1) :=
 begin
-  suffices : ∀ x ∈ [a, b], has_deriv_at (λ x : ℝ, x ^ (r + 1) / (r + 1)) (x ^ r) x,
-  { rw sub_div,
-    exact integral_eq_sub_of_has_deriv_at this (interval_integrable_rpow (h.imp_right and.right)) },
-  intros x hx,
-  have hx' : x ≠ 0 ∨ 1 ≤ r + 1,
-    from h.symm.imp (λ h, ne_of_mem_of_not_mem hx h.2) (le_add_iff_nonneg_left _).2,
-  convert (real.has_deriv_at_rpow_const hx').div_const (r + 1),
-  rw [add_sub_cancel, mul_div_cancel_left],
-  rw [ne.def, ← eq_neg_iff_add_eq_zero],
-  rintro rfl,
-  apply (@zero_lt_one ℝ _ _).not_le,
-  simpa using h
+  rw sub_div,
+  have hderiv : ∀ (x : ℝ), x ≠ 0 → has_deriv_at (λ x : ℝ, x ^ (r + 1) / (r + 1)) (x ^ r) x,
+  { intros x hx,
+    convert (real.has_deriv_at_rpow_const (or.inl hx)).div_const (r + 1),
+    rw [add_sub_cancel, mul_div_cancel_left],
+    contrapose! h, rw ←eq_neg_iff_add_eq_zero at h, rw h, tauto, },
+  cases h,
+  { suffices : ∀ (c : ℝ), ∫ x in 0..c, x ^ r = c ^ (r + 1) / (r + 1),
+    { rw [←integral_add_adjacent_intervals
+        (interval_integrable_rpow' h) (interval_integrable_rpow' h), this b],
+      have t := this a, rw integral_symm at t, apply_fun (λ x, -x) at t, rw neg_neg at t,
+      rw t, ring },
+    intro c, rcases le_total 0 c with hc|hc,
+    { convert integral_eq_sub_of_has_deriv_at_of_le hc _ (λ x hx, hderiv x hx.1.ne') _,
+      { rw zero_rpow, ring, linarith,},
+      { apply continuous_at.continuous_on, intros x hx,
+        refine (continuous_at_id.rpow_const _).div_const, right, linarith,},
+      apply interval_integrable_rpow' h },
+    { rw integral_symm, symmetry, rw eq_neg_iff_eq_neg,
+      convert integral_eq_sub_of_has_deriv_at_of_le hc _ (λ x hx, hderiv x hx.2.ne) _,
+      { rw zero_rpow, ring, linarith },
+      { apply continuous_at.continuous_on, intros x hx,
+        refine (continuous_at_id.rpow_const _).div_const, right, linarith },
+      apply interval_integrable_rpow' h, } },
+  { have hderiv' : ∀ (x : ℝ), x ∈ [a, b] → has_deriv_at (λ x : ℝ, x ^ (r + 1) / (r + 1)) (x ^ r) x,
+    { intros x hx, apply hderiv x, exact ne_of_mem_of_not_mem hx h.2 },
+    exact integral_eq_sub_of_has_deriv_at hderiv' (interval_integrable_rpow (or.inr h.2)) },
 end
 
 lemma integral_zpow {n : ℤ} (h : 0 ≤ n ∨ n ≠ -1 ∧ (0 : ℝ) ∉ [a, b]) :
   ∫ x in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (n + 1) :=
 begin
-  replace h : 0 ≤ (n : ℝ) ∨ (n : ℝ) ≠ -1 ∧ (0 : ℝ) ∉ [a, b], by exact_mod_cast h,
-  exact_mod_cast integral_rpow h
+  replace h : -1 < (n : ℝ) ∨ (n : ℝ) ≠ -1 ∧ (0 : ℝ) ∉ [a, b], by exact_mod_cast h,
+  exact_mod_cast integral_rpow h,
 end
 
 @[simp] lemma integral_pow : ∫ x in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (n + 1) :=

src/measure_theory/integral/integral_eq_improper.lean

@@ -576,6 +576,29 @@ lemma integrable_on_Ioi_of_interval_integral_norm_tendsto (I a : ℝ)
 let ⟨I', hI'⟩ := h.is_bounded_under_le in
   integrable_on_Ioi_of_interval_integral_norm_bounded I' a hfi hb hI'
 
+lemma integrable_on_Ioc_of_interval_integral_norm_bounded {I a₀ b₀ : ℝ}
+  (hfi : ∀ i, integrable_on f $ Ioc (a i) (b i))
+  (ha : tendsto a l $ 𝓝 a₀) (hb : tendsto b l $ 𝓝 b₀)
+  (h : ∀ᶠ i in l, (∫ x in Ioc (a i) (b i), ∥f x∥) ≤ I) : integrable_on f (Ioc a₀ b₀) :=
+begin
+  refine (ae_cover_Ioc_of_Ioc ha hb).integrable_of_integral_norm_bounded I
+    (λ i, (hfi i).restrict measurable_set_Ioc) (eventually.mono h _),
+  intros i hi, simp only [measure.restrict_restrict measurable_set_Ioc],
+  refine le_trans (set_integral_mono_set (hfi i).norm _ _) hi,
+  { apply ae_of_all, simp only [pi.zero_apply, norm_nonneg, forall_const] },
+  { apply ae_of_all, intros c hc, exact hc.1 },
+end
+
+lemma integrable_on_Ioc_of_interval_integral_norm_bounded_left {I a₀ b : ℝ}
+  (hfi : ∀ i, integrable_on f $ Ioc (a i) b) (ha : tendsto a l $ 𝓝 a₀)
+  (h : ∀ᶠ i in l, (∫ x in Ioc (a i) b, ∥f x∥ ) ≤ I) : integrable_on f (Ioc a₀ b) :=
+integrable_on_Ioc_of_interval_integral_norm_bounded hfi ha tendsto_const_nhds h
+
+lemma integrable_on_Ioc_of_interval_integral_norm_bounded_right {I a b₀ : ℝ}
+  (hfi : ∀ i, integrable_on f $ Ioc a (b i)) (hb : tendsto b l $ 𝓝 b₀)
+  (h : ∀ᶠ i in l, (∫ x in Ioc a (b i), ∥f x∥ ) ≤ I) : integrable_on f (Ioc a b₀) :=
+integrable_on_Ioc_of_interval_integral_norm_bounded hfi tendsto_const_nhds hb h
+
 end integrable_of_interval_integral
 
 section integral_of_interval_integral