feat(measure_theory/integral/integral_eq_improper): fundamental theor…

…em of calculus on (a, +\infty) (#18844)

It became apparent in several applications that we are missing API here. As an illustration, two existing proofs in the library are shortened with the new API.

src/analysis/special_functions/gaussian.lean

@@ -158,25 +158,20 @@ lemma integral_mul_cexp_neg_mul_sq {b : ℂ} (hb : 0 < b.re) :
   ∫ r:ℝ in Ioi 0, (r : ℂ) * cexp (-b * r ^ 2) = (2 * b)⁻¹ :=
 begin
   have hb' : b ≠ 0 := by { contrapose! hb, rw [hb, zero_re], },
-  refine tendsto_nhds_unique (interval_integral_tendsto_integral_Ioi _
-    (integrable_mul_cexp_neg_mul_sq hb).integrable_on filter.tendsto_id) _,
   have A : ∀ x:ℂ, has_deriv_at (λ x, - (2 * b)⁻¹ * cexp (-b * x^2)) (x * cexp (- b * x^2)) x,
   { intro x,
     convert (((has_deriv_at_pow 2 x)).const_mul (-b)).cexp.const_mul (- (2 * b)⁻¹) using 1,
     field_simp [hb'],
     ring },
-  have : ∀ (y : ℝ), ∫ x in 0..(id y), ↑x * cexp (-b * x^2)
-      = (- (2 * b)⁻¹ * cexp (-b * y^2)) - (- (2 * b)⁻¹ * cexp (-b * 0^2)) :=
-    λ y, interval_integral.integral_eq_sub_of_has_deriv_at
-      (λ x hx, (A x).comp_of_real) (integrable_mul_cexp_neg_mul_sq hb).interval_integrable,
-  simp_rw this,
-  have L : tendsto (λ (x : ℝ), (2 * b)⁻¹ - (2 * b)⁻¹ * cexp (-b * x ^ 2)) at_top
-    (𝓝 ((2 * b)⁻¹ - (2 * b)⁻¹ * 0)),
-  { refine tendsto_const_nhds.sub (tendsto.const_mul _ $ tendsto_zero_iff_norm_tendsto_zero.mpr _),
+  have B : tendsto (λ (y : ℝ), -(2 * b)⁻¹ * cexp (-b * ↑y ^ 2)) at_top (𝓝 (-(2 * b)⁻¹ * 0)),
+  { refine (tendsto.const_mul _ (tendsto_zero_iff_norm_tendsto_zero.mpr _)),
     simp_rw norm_cexp_neg_mul_sq b,
     exact tendsto_exp_at_bot.comp
       (tendsto.neg_const_mul_at_top (neg_lt_zero.2 hb) (tendsto_pow_at_top two_ne_zero)) },
-  simpa using L,
+  convert integral_Ioi_of_has_deriv_at_of_tendsto' (λ x hx, (A ↑x).comp_of_real)
+    (integrable_mul_cexp_neg_mul_sq hb).integrable_on B,
+  simp only [mul_zero, of_real_zero, zero_pow', ne.def, bit0_eq_zero, nat.one_ne_zero,
+    not_false_iff, complex.exp_zero, mul_one, sub_neg_eq_add, zero_add],
 end
 
 /-- The *square* of the Gaussian integral `∫ x:ℝ, exp (-b * x^2)` is equal to `π / b`. -/

src/analysis/special_functions/integrals.lean

@@ -67,7 +67,7 @@ begin
     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,
+    apply integrable_on_deriv_of_nonneg _ 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,

src/measure_theory/integral/exp_decay.lean

@@ -18,33 +18,17 @@ for integrability:
 
 noncomputable theory
 open real interval_integral measure_theory set filter
-
-/-- Integral of `exp (-b * x)` over `(a, X)` is bounded as `X → ∞`. -/
-lemma integral_exp_neg_le {b : ℝ} (a X : ℝ) (h2 : 0 < b) :
-  (∫ x in a .. X, exp (-b * x)) ≤ exp (-b * a) / b :=
-begin
-  rw integral_deriv_eq_sub' (λ x, -exp (-b * x) / b),
-  -- goal 1/4: F(X) - F(a) is bounded
-  { simp only [tsub_le_iff_right],
-    rw [neg_div b (exp (-b * a)), neg_div b (exp (-b * X)), add_neg_self, neg_le, neg_zero],
-    exact (div_pos (exp_pos _) h2).le, },
-  -- goal 2/4: the derivative of F is exp(-b x)
-  { ext1, simp [h2.ne'] },
-  -- goal 3/4: F is differentiable
-  { intros x hx, simp [h2.ne'], },
-  -- goal 4/4: exp(-b x) is continuous
-  { apply continuous.continuous_on, continuity }
-end
+open_locale topology
 
 /-- `exp (-b * x)` is integrable on `(a, ∞)`. -/
 lemma exp_neg_integrable_on_Ioi (a : ℝ) {b : ℝ} (h : 0 < b) :
   integrable_on (λ x : ℝ, exp (-b * x)) (Ioi a) :=
 begin
-  have : ∀ (X : ℝ), integrable_on (λ x : ℝ, exp (-b * x) ) (Ioc a X),
-  { intro X, exact (continuous_const.mul continuous_id).exp.integrable_on_Ioc },
-  apply (integrable_on_Ioi_of_interval_integral_norm_bounded (exp (-b * a) / b) a this tendsto_id),
-  simp only [eventually_at_top, norm_of_nonneg (exp_pos _).le],
-  exact ⟨a, λ b2 hb2, integral_exp_neg_le a b2 h⟩,
+  have : tendsto (λ x, -exp (-b * x) / b) at_top (𝓝 (-0/b)),
+  { refine tendsto.div_const (tendsto.neg _) _,
+    exact tendsto_exp_at_bot.comp (tendsto_id.neg_const_mul_at_top (right.neg_neg_iff.2 h)) },
+  refine integrable_on_Ioi_deriv_of_nonneg' (λ x hx, _) (λ x hx, (exp_pos _).le) this,
+  simpa [h.ne'] using ((has_deriv_at_id x).const_mul b).neg.exp.neg.div_const b,
 end
 
 /-- If `f` is continuous on `[a, ∞)`, and is `O (exp (-b * x))` at `∞` for some `b > 0`, then

src/measure_theory/integral/integral_eq_improper.lean

@@ -50,7 +50,15 @@ as an `ae_cover` w.r.t. `μ.restrict (Iic b)`, instead of using `(λ x, Ioc x b)
   then `∫ x in φ n, f x ∂μ` tends to `∫ x, f x ∂μ` as `n` tends to `+∞`.
 
 We then specialize these lemmas to various use cases involving intervals, which are frequent
-in analysis.
+in analysis. In particular,
+- `measure_theory.integral_Ioi_of_has_deriv_at_of_tendsto` is a version of FTC-2 on the interval
+  `(a, +∞)`, giving the formula `∫ x in (a, +∞), g' x = l - g a` if `g'` is integrable and
+  `g` tends to `l` at `+∞`.
+- `measure_theory.integral_Ioi_of_has_deriv_at_of_nonneg` gives the same result assuming that
+  `g'` is nonnegative instead of integrable. Its automatic integrability in this context is proved
+  in `measure_theory.integrable_on_Ioi_deriv_of_nonneg`.
+- `measure_theory.integral_comp_smul_deriv_Ioi` is a version of the change of variables formula
+  on semi-infinite intervals.
 -/
 
 open measure_theory filter set topological_space
@@ -604,7 +612,7 @@ 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) :=
+  (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₀ : ℝ}
@@ -660,12 +668,170 @@ end
 
 end integral_of_interval_integral
 
+open real
+open_locale interval
+
+section Ioi_FTC
+
+variables {E : Type*} {f f' : ℝ → E} {g g' : ℝ → ℝ} {a b l : ℝ} {m : E}
+  [normed_add_comm_group E] [normed_space ℝ E] [complete_space E]
+
+/-- **Fundamental theorem of calculus-2**, on semi-infinite intervals `(a, +∞)`.
+When a function has a limit at infinity `m`, and its derivative is integrable, then the
+integral of the derivative on `(a, +∞)` is `m - f a`. Version assuming differentiability
+on `(a, +∞)` and continuity on `[a, +∞)`.-/
+lemma integral_Ioi_of_has_deriv_at_of_tendsto (hcont : continuous_on f (Ici a))
+  (hderiv : ∀ x ∈ Ioi a, has_deriv_at f (f' x) x)
+  (f'int : integrable_on f' (Ioi a)) (hf : tendsto f at_top (𝓝 m)) :
+  ∫ x in Ioi a, f' x = m - f a :=
+begin
+  refine tendsto_nhds_unique (interval_integral_tendsto_integral_Ioi a f'int tendsto_id) _,
+  apply tendsto.congr' _ (hf.sub_const _),
+  filter_upwards [Ioi_mem_at_top a] with x hx,
+  have h'x : a ≤ id x := le_of_lt hx,
+  symmetry,
+  apply interval_integral.integral_eq_sub_of_has_deriv_at_of_le h'x
+    (hcont.mono Icc_subset_Ici_self) (λ y hy, hderiv y hy.1),
+  rw interval_integrable_iff_integrable_Ioc_of_le h'x,
+  exact f'int.mono (λ y hy, hy.1) le_rfl,
+end
+
+/-- **Fundamental theorem of calculus-2**, on semi-infinite intervals `(a, +∞)`.
+When a function has a limit at infinity `m`, and its derivative is integrable, then the
+integral of the derivative on `(a, +∞)` is `m - f a`. Version assuming differentiability
+on `[a, +∞)`. -/
+lemma integral_Ioi_of_has_deriv_at_of_tendsto'
+  (hderiv : ∀ x ∈ Ici a, has_deriv_at f (f' x) x)
+  (f'int : integrable_on f' (Ioi a)) (hf : tendsto f at_top (𝓝 m)) :
+  ∫ x in Ioi a, f' x = m - f a :=
+begin
+  apply integral_Ioi_of_has_deriv_at_of_tendsto _ (λ x hx, hderiv x (le_of_lt hx)) f'int hf,
+  assume x hx,
+  exact (hderiv x hx).continuous_at.continuous_within_at,
+end
+
+/-- When a function has a limit at infinity, and its derivative is nonnegative, then the derivative
+is automatically integrable on `(a, +∞)`. Version assuming differentiability
+on `(a, +∞)` and continuity on `[a, +∞)`. -/
+lemma integrable_on_Ioi_deriv_of_nonneg (hcont : continuous_on g (Ici a))
+  (hderiv : ∀ x ∈ Ioi a, has_deriv_at g (g' x) x)
+  (g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x) (hg : tendsto g at_top (𝓝 l)) :
+  integrable_on g' (Ioi a) :=
+begin
+  apply integrable_on_Ioi_of_interval_integral_norm_tendsto (l - g a) a (λ x, _) tendsto_id, swap,
+  { exact interval_integral.integrable_on_deriv_of_nonneg (hcont.mono Icc_subset_Ici_self)
+      (λ y hy, hderiv y hy.1) (λ y hy, g'pos y hy.1) },
+  apply tendsto.congr' _ (hg.sub_const _),
+  filter_upwards [Ioi_mem_at_top a] with x hx,
+  have h'x : a ≤ id x := le_of_lt hx,
+  calc g x - g a = ∫ y in a..id x, g' y :
+    begin
+      symmetry,
+      apply interval_integral.integral_eq_sub_of_has_deriv_at_of_le h'x
+        (hcont.mono Icc_subset_Ici_self) (λ y hy, hderiv y hy.1),
+      rw interval_integrable_iff_integrable_Ioc_of_le h'x,
+      exact interval_integral.integrable_on_deriv_of_nonneg (hcont.mono Icc_subset_Ici_self)
+        (λ y hy, hderiv y hy.1) (λ y hy, g'pos y hy.1)
+    end
+  ... = ∫ y in a..id x, ‖g' y‖ :
+    begin
+      simp_rw interval_integral.integral_of_le h'x,
+      refine set_integral_congr (measurable_set_Ioc) (λ y hy, _),
+      dsimp,
+      rw abs_of_nonneg,
+      exact g'pos _ hy.1,
+    end
+end
+
+/-- When a function has a limit at infinity, and its derivative is nonnegative, then the derivative
+is automatically integrable on `(a, +∞)`. Version assuming differentiability
+on `[a, +∞)`. -/
+lemma integrable_on_Ioi_deriv_of_nonneg'
+  (hderiv : ∀ x ∈ Ici a, has_deriv_at g (g' x) x)
+  (g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x) (hg : tendsto g at_top (𝓝 l)) :
+  integrable_on g' (Ioi a) :=
+begin
+  apply integrable_on_Ioi_deriv_of_nonneg _ (λ x hx, hderiv x (le_of_lt hx)) g'pos hg,
+  assume x hx,
+  exact (hderiv x hx).continuous_at.continuous_within_at,
+end
+
+/-- When a function has a limit at infinity `l`, and its derivative is nonnegative, then the
+integral of the derivative on `(a, +∞)` is `l - g a` (and the derivative is integrable, see
+`integrable_on_Ioi_deriv_of_nonneg`). Version assuming differentiability on `(a, +∞)` and
+continuity on `[a, +∞)`. -/
+lemma integral_Ioi_of_has_deriv_at_of_nonneg (hcont : continuous_on g (Ici a))
+  (hderiv : ∀ x ∈ Ioi a, has_deriv_at g (g' x) x)
+  (g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x) (hg : tendsto g at_top (𝓝 l)) :
+  ∫ x in Ioi a, g' x = l - g a :=
+integral_Ioi_of_has_deriv_at_of_tendsto hcont hderiv
+  (integrable_on_Ioi_deriv_of_nonneg hcont hderiv g'pos hg) hg
+
+/-- When a function has a limit at infinity `l`, and its derivative is nonnegative, then the
+integral of the derivative on `(a, +∞)` is `l - g a` (and the derivative is integrable, see
+`integrable_on_Ioi_deriv_of_nonneg'`). Version assuming differentiability on `[a, +∞)`. -/
+lemma integral_Ioi_of_has_deriv_at_of_nonneg'
+  (hderiv : ∀ x ∈ Ici a, has_deriv_at g (g' x) x)
+  (g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x) (hg : tendsto g at_top (𝓝 l)) :
+  ∫ x in Ioi a, g' x = l - g a :=
+integral_Ioi_of_has_deriv_at_of_tendsto' hderiv
+  (integrable_on_Ioi_deriv_of_nonneg' hderiv g'pos hg) hg
+
+/-- When a function has a limit at infinity, and its derivative is nonpositive, then the derivative
+is automatically integrable on `(a, +∞)`. Version assuming differentiability
+on `(a, +∞)` and continuity on `[a, +∞)`. -/
+lemma integrable_on_Ioi_deriv_of_nonpos (hcont : continuous_on g (Ici a))
+  (hderiv : ∀ x ∈ Ioi a, has_deriv_at g (g' x) x)
+  (g'neg : ∀ x ∈ Ioi a, g' x ≤ 0) (hg : tendsto g at_top (𝓝 l)) :
+  integrable_on g' (Ioi a) :=
+begin
+  apply integrable_neg_iff.1,
+  exact integrable_on_Ioi_deriv_of_nonneg hcont.neg (λ x hx, (hderiv x hx).neg)
+    (λ x hx, neg_nonneg_of_nonpos (g'neg x hx)) hg.neg,
+end
+
+/-- When a function has a limit at infinity, and its derivative is nonpositive, then the derivative
+is automatically integrable on `(a, +∞)`. Version assuming differentiability
+on `[a, +∞)`. -/
+lemma integrable_on_Ioi_deriv_of_nonpos'
+  (hderiv : ∀ x ∈ Ici a, has_deriv_at g (g' x) x)
+  (g'neg : ∀ x ∈ Ioi a, g' x ≤ 0) (hg : tendsto g at_top (𝓝 l)) :
+  integrable_on g' (Ioi a) :=
+begin
+  apply integrable_on_Ioi_deriv_of_nonpos _ (λ x hx, hderiv x (le_of_lt hx)) g'neg hg,
+  assume x hx,
+  exact (hderiv x hx).continuous_at.continuous_within_at,
+end
+
+/-- When a function has a limit at infinity `l`, and its derivative is nonpositive, then the
+integral of the derivative on `(a, +∞)` is `l - g a` (and the derivative is integrable, see
+`integrable_on_Ioi_deriv_of_nonneg`). Version assuming differentiability on `(a, +∞)` and
+continuity on `[a, +∞)`. -/
+lemma integral_Ioi_of_has_deriv_at_of_nonpos (hcont : continuous_on g (Ici a))
+  (hderiv : ∀ x ∈ Ioi a, has_deriv_at g (g' x) x)
+  (g'neg : ∀ x ∈ Ioi a, g' x ≤ 0) (hg : tendsto g at_top (𝓝 l)) :
+  ∫ x in Ioi a, g' x = l - g a :=
+integral_Ioi_of_has_deriv_at_of_tendsto hcont hderiv
+  (integrable_on_Ioi_deriv_of_nonpos hcont hderiv g'neg hg) hg
+
+/-- When a function has a limit at infinity `l`, and its derivative is nonpositive, then the
+integral of the derivative on `(a, +∞)` is `l - g a` (and the derivative is integrable, see
+`integrable_on_Ioi_deriv_of_nonneg'`). Version assuming differentiability on `[a, +∞)`. -/
+lemma integral_Ioi_of_has_deriv_at_of_nonpos'
+  (hderiv : ∀ x ∈ Ici a, has_deriv_at g (g' x) x)
+  (g'neg : ∀ x ∈ Ioi a, g' x ≤ 0) (hg : tendsto g at_top (𝓝 l)) :
+  ∫ x in Ioi a, g' x = l - g a :=
+integral_Ioi_of_has_deriv_at_of_tendsto' hderiv
+  (integrable_on_Ioi_deriv_of_nonpos' hderiv g'neg hg) hg
+
+end Ioi_FTC
+
 section Ioi_change_variables
 
 open real
 open_locale interval
 
-variables {E : Type*} {μ : measure ℝ} {f : ℝ → E}
+variables {E : Type*} {f : ℝ → E}
   [normed_add_comm_group E] [normed_space ℝ E] [complete_space E]
 
 /-- Change-of-variables formula for `Ioi` integrals of vector-valued functions, proved by taking

src/measure_theory/integral/interval_integral.lean

@@ -2524,11 +2524,13 @@ end
 -/
 
 /-- When the right derivative of a function is nonnegative, then it is automatically integrable. -/
-lemma integrable_on_deriv_right_of_nonneg (hab : a ≤ b) (hcont : continuous_on g (Icc a b))
+lemma integrable_on_deriv_right_of_nonneg  (hcont : continuous_on g (Icc a b))
   (hderiv : ∀ x ∈ Ioo a b, has_deriv_within_at g (g' x) (Ioi x) x)
   (g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x) :
   integrable_on g' (Ioc a b) :=
 begin
+  by_cases hab : a < b, swap,
+  { simp [Ioc_eq_empty hab] },
   rw integrable_on_Ioc_iff_integrable_on_Ioo,
   have meas_g' : ae_measurable g' (volume.restrict (Ioo a b)),
   { apply (ae_measurable_deriv_within_Ioi g _).congr,
@@ -2549,8 +2551,8 @@ begin
     lintegral_coe_eq_integral _ intF,
   rw A at hf,
   have B : ∫ (x : ℝ) in Ioo a b, F x ≤ g b - g a,
-  { rw [← integral_Ioc_eq_integral_Ioo, ← interval_integral.integral_of_le hab],
-    apply integral_le_sub_of_has_deriv_right_of_le hab hcont hderiv _ (λ x hx, _),
+  { rw [← integral_Ioc_eq_integral_Ioo, ← interval_integral.integral_of_le hab.le],
+    apply integral_le_sub_of_has_deriv_right_of_le hab.le hcont hderiv _ (λ x hx, _),
     { rwa integrable_on_Icc_iff_integrable_on_Ioo },
     { convert nnreal.coe_le_coe.2 (fle x),
       simp only [real.norm_of_nonneg (g'pos x hx), coe_nnnorm] } },
@@ -2559,11 +2561,11 @@ end
 
 /-- When the derivative of a function is nonnegative, then it is automatically integrable,
 Ioc version. -/
-lemma integrable_on_deriv_of_nonneg (hab : a ≤ b) (hcont : continuous_on g (Icc a b))
+lemma integrable_on_deriv_of_nonneg (hcont : continuous_on g (Icc a b))
   (hderiv : ∀ x ∈ Ioo a b, has_deriv_at g (g' x) x)
   (g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x) :
   integrable_on g' (Ioc a b) :=
-integrable_on_deriv_right_of_nonneg hab hcont (λ x hx, (hderiv x hx).has_deriv_within_at) g'pos
+integrable_on_deriv_right_of_nonneg hcont (λ x hx, (hderiv x hx).has_deriv_within_at) g'pos
 
 /-- When the derivative of a function is nonnegative, then it is automatically integrable,
 interval version. -/
@@ -2575,10 +2577,10 @@ begin
   cases le_total a b with hab hab,
   { simp only [uIcc_of_le, min_eq_left, max_eq_right, hab, interval_integrable,
       hab, Ioc_eq_empty_of_le, integrable_on_empty, and_true] at hcont hderiv hpos ⊢,
-    exact integrable_on_deriv_of_nonneg hab hcont hderiv hpos, },
+    exact integrable_on_deriv_of_nonneg hcont hderiv hpos, },
   { simp only [uIcc_of_ge, min_eq_right, max_eq_left, hab, interval_integrable,
       Ioc_eq_empty_of_le, integrable_on_empty, true_and] at hcont hderiv hpos ⊢,
-    exact integrable_on_deriv_of_nonneg hab hcont hderiv hpos }
+    exact integrable_on_deriv_of_nonneg hcont hderiv hpos }
 end
 
 /-!