feat(special_functions/gamma): better convergence bounds (#14496)

Use the stronger form of FTC-2 added #14147 to strengthen some results about the gamma function.



Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
Co-authored-by: loefflerd <d.loeffler.01@cantab.net>

src/analysis/special_functions/gamma.lean

@@ -10,14 +10,13 @@ import analysis.calculus.parametric_integral
 # The Gamma function
 
 This file defines the `Γ` function (of a real or complex variable `s`). We define this by Euler's
-integral `Γ(s) = ∫ x in Ioi 0, exp (-x) * x ^ (s - 1)` in a range where we can prove this is
-convergent: presently `1 ≤ s` in the real case, and `1 ≤ re s` in the complex case (which is
-non-optimal, but the optimal bound of `0 < s`, resp `0 < re s`, is harder to prove using the
-methods in the library).
+integral `Γ(s) = ∫ x in Ioi 0, exp (-x) * x ^ (s - 1)` in the range where this integral converges
+(i.e., for `0 < s` in the real case, and `0 < re s` in the complex case).
 
 We show that this integral satisfies `Γ(1) = 1` and `Γ(s + 1) = s * Γ(s)`; hence we can define
 `Γ(s)` for all `s` as the unique function satisfying this recurrence and agreeing with Euler's
-integral in the convergence range.
+integral in the convergence range. In the complex case we also prove that the resulting function is
+holomorphic on `ℂ` away from the points `{-n : n ∈ ℤ}`.
 
 ## Tags
 
@@ -55,19 +54,23 @@ end
 /-- Euler's integral for the `Γ` function (of a real variable `s`), defined as
 `∫ x in Ioi 0, exp (-x) * x ^ (s - 1)`.
 
-See `Gamma_integral_convergent` for a proof of the convergence of the integral for `1 ≤ s`. -/
+See `Gamma_integral_convergent` for a proof of the convergence of the integral for `0 < s`. -/
 def Gamma_integral (s : ℝ) : ℝ := ∫ x in Ioi (0:ℝ), exp (-x) * x ^ (s - 1)
 
-/-- The integral defining the `Γ` function converges for real `s` with `1 ≤ s`.
-
-This is not optimal, but the optimal bound (convergence for `0 < s`) is hard to establish with the
-results currently in the library. -/
-lemma Gamma_integral_convergent {s : ℝ} (h : 1 ≤ s) :
+/-- The integral defining the `Γ` function converges for positive real `s`. -/
+lemma Gamma_integral_convergent {s : ℝ} (h : 0 < s) :
   integrable_on (λ x:ℝ, exp (-x) * x ^ (s - 1)) (Ioi 0) :=
 begin
-  refine integrable_of_is_O_exp_neg one_half_pos _ (Gamma_integrand_is_o _ ).is_O,
-  refine continuous_on_id.neg.exp.mul (continuous_on_id.rpow_const _),
-  intros x hx, right, simpa only [sub_nonneg] using h,
+  rw [←Ioc_union_Ioi_eq_Ioi (@zero_le_one ℝ _ _ _ _), integrable_on_union],
+  split,
+  { rw ←integrable_on_Icc_iff_integrable_on_Ioc,
+    refine integrable_on.continuous_on_mul continuous_on_id.neg.exp _ is_compact_Icc,
+    refine (interval_integrable_iff_integrable_Icc_of_le zero_le_one).mp _,
+    exact interval_integrable_rpow' (by linarith), },
+  { refine integrable_of_is_O_exp_neg one_half_pos _ (Gamma_integrand_is_o _ ).is_O,
+    refine continuous_on_id.neg.exp.mul (continuous_on_id.rpow_const _),
+    intros x hx,
+    exact or.inl ((zero_lt_one : (0 : ℝ) < 1).trans_le hx).ne' }
 end
 
 lemma Gamma_integral_one : Gamma_integral 1 = 1 :=
@@ -81,16 +84,12 @@ make a choice between ↑(real.exp (-x)), complex.exp (↑(-x)), and complex.exp
 equal but not definitionally so. We use the first of these throughout. -/
 
 
-/-- The integral defining the `Γ` function converges for complex `s` with `1 ≤ re s`.
+/-- The integral defining the `Γ` function converges for complex `s` with `0 < re s`.
 
-This is proved by reduction to the real case. The bound is not optimal, but the optimal bound
-(convergence for `0 < re s`) is hard to establish with the results currently in the library. -/
-lemma Gamma_integral_convergent {s : ℂ} (hs : 1 ≤ s.re) :
+This is proved by reduction to the real case. -/
+lemma Gamma_integral_convergent {s : ℂ} (hs : 0 < s.re) :
   integrable_on (λ x, (-x).exp * x ^ (s - 1) : ℝ → ℂ) (Ioi 0) :=
 begin
-  -- This is slightly subtle if `s` is non-real but `s.re = 1`, as the integrand is not continuous
-  -- at the lower endpoint. However, it is continuous on the interior, and its norm is continuous
-  -- at the endpoint, which is good enough.
   split,
   { refine continuous_on.ae_strongly_measurable _ measurable_set_Ioi,
     apply (continuous_of_real.comp continuous_neg.exp).continuous_on.mul,
@@ -112,7 +111,7 @@ end
 `∫ x in Ioi 0, exp (-x) * x ^ (s - 1)`.
 
 See `complex.Gamma_integral_convergent` for a proof of the convergence of the integral for
-`1 ≤ re s`. -/
+`0 < re s`. -/
 def Gamma_integral (s : ℂ) : ℂ := ∫ x in Ioi (0:ℝ), ↑(-x).exp * ↑x ^ (s - 1)
 
 lemma Gamma_integral_of_real (s : ℝ) :
@@ -142,26 +141,26 @@ section Gamma_recurrence
 /-- The indefinite version of the `Γ` function, `Γ(s, X) = ∫ x ∈ 0..X, exp(-x) x ^ (s - 1)`. -/
 def partial_Gamma (s : ℂ) (X : ℝ) : ℂ := ∫ x in 0..X, (-x).exp * x ^ (s - 1)
 
-lemma tendsto_partial_Gamma {s : ℂ} (hs: 1 ≤ s.re) :
+lemma tendsto_partial_Gamma {s : ℂ} (hs: 0 < s.re) :
   tendsto (λ X:ℝ, partial_Gamma s X) at_top (𝓝 $ Gamma_integral s) :=
 interval_integral_tendsto_integral_Ioi 0 (Gamma_integral_convergent hs) tendsto_id
 
-private lemma Gamma_integrand_interval_integrable (s : ℂ) {X : ℝ} (hs : 1 ≤ s.re) (hX : 0 ≤ X):
+private lemma Gamma_integrand_interval_integrable (s : ℂ) {X : ℝ} (hs : 0 < s.re) (hX : 0 ≤ X):
   interval_integrable (λ x, (-x).exp * x ^ (s - 1) : ℝ → ℂ) volume 0 X :=
 begin
   rw interval_integrable_iff_integrable_Ioc_of_le hX,
   exact integrable_on.mono_set (Gamma_integral_convergent hs) Ioc_subset_Ioi_self
 end
 
-private lemma Gamma_integrand_deriv_integrable_A {s : ℂ} (hs: 1 ≤ s.re) {X : ℝ} (hX : 0 ≤ X):
+private lemma Gamma_integrand_deriv_integrable_A {s : ℂ} (hs : 0 < s.re) {X : ℝ} (hX : 0 ≤ X):
  interval_integrable (λ x, -((-x).exp * x ^ s) : ℝ → ℂ) volume 0 X :=
 begin
-  have t := (Gamma_integrand_interval_integrable (s+1) _ hX).neg,
-  { simpa using t },
+  convert (Gamma_integrand_interval_integrable (s+1) _ hX).neg,
+  { ext1, simp only [add_sub_cancel, pi.neg_apply] },
   { simp only [add_re, one_re], linarith,},
 end
 
-private lemma Gamma_integrand_deriv_integrable_B {s : ℂ} (hs: 1 ≤ s.re) {Y : ℝ} (hY : 0 ≤ Y) :
+private lemma Gamma_integrand_deriv_integrable_B {s : ℂ} (hs : 0 < s.re) {Y : ℝ} (hY : 0 ≤ Y) :
   interval_integrable (λ (x : ℝ), (-x).exp * (s * x ^ (s - 1)) : ℝ → ℂ) volume 0 Y :=
 begin
   have: (λ x, (-x).exp * (s * x ^ (s - 1)) : ℝ → ℂ) =
@@ -174,19 +173,19 @@ begin
     intros x hx,
     refine (_ : continuous_at (λ x:ℂ, x ^ (s - 1)) _).comp continuous_of_real.continuous_at,
     apply continuous_at_cpow_const, rw of_real_re, exact or.inl hx.1, },
-  apply has_finite_integral_of_bounded, swap, exact s.abs * Y ^ (s.re - 1),
-  refine (ae_restrict_iff' measurable_set_Ioc).mpr (ae_of_all _ (λ x hx, _)),
-  rw [norm_eq_abs, abs_mul,abs_mul, abs_of_nonneg (exp_pos(-x)).le],
-  refine mul_le_mul_of_nonneg_left _ (abs_nonneg s),
-  have i1: (-x).exp ≤ 1 := by { simpa using hx.1.le, },
-  have i2: abs (↑x ^ (s - 1)) ≤ Y ^ (s.re - 1),
-  { rw [abs_cpow_eq_rpow_re_of_pos hx.1 _, sub_re, one_re],
-    apply rpow_le_rpow hx.1.le hx.2, linarith, },
-  simpa using mul_le_mul i1 i2 (abs_nonneg (↑x ^ (s - 1))) zero_le_one,
+  rw ←has_finite_integral_norm_iff,
+  simp_rw [norm_eq_abs, complex.abs_mul],
+  refine (((real.Gamma_integral_convergent hs).mono_set
+    Ioc_subset_Ioi_self).has_finite_integral.congr _).const_mul _,
+  rw [eventually_eq, ae_restrict_iff'],
+  { apply ae_of_all, intros x hx,
+    rw [abs_of_nonneg (exp_pos _).le,abs_cpow_eq_rpow_re_of_pos hx.1],
+    simp },
+  { exact measurable_set_Ioc},
 end
 
 /-- The recurrence relation for the indefinite version of the `Γ` function. -/
-lemma partial_Gamma_add_one {s : ℂ} (hs: 1 ≤ s.re) {X : ℝ} (hX : 0 ≤ X) :
+lemma partial_Gamma_add_one {s : ℂ} (hs: 0 < s.re) {X : ℝ} (hX : 0 ≤ X) :
   partial_Gamma (s + 1) X = s * partial_Gamma s X - (-X).exp * X ^ s :=
 begin
   rw [partial_Gamma, partial_Gamma, add_sub_cancel],
@@ -204,7 +203,7 @@ begin
       simpa using has_deriv_at.comp x (t hx.left) of_real_clm.has_deriv_at, },
     simpa only [of_real_neg, neg_mul] using d1b.mul d2 },
   have cont := (continuous_of_real.comp continuous_neg.exp).mul
-    (continuous_of_real_cpow_const $ lt_of_lt_of_le zero_lt_one hs),
+    (continuous_of_real_cpow_const hs),
   have der_ible := (Gamma_integrand_deriv_integrable_A hs hX).add
     (Gamma_integrand_deriv_integrable_B hs hX),
   have int_eval := integral_eq_sub_of_has_deriv_at_of_le hX cont.continuous_on F_der_I der_ible,
@@ -222,11 +221,11 @@ begin
   have t := @integral_const_mul (0:ℝ) X volume _ _ s (λ x:ℝ, (-x).exp * x ^ (s - 1)),
   dsimp at t, rw [←t, of_real_zero, zero_cpow],
   { rw [mul_zero, add_zero], congr', ext1, ring },
-  { contrapose! hs, rw [hs, zero_re], exact zero_lt_one,}
+  { contrapose! hs, rw [hs, zero_re] }
 end
 
 /-- The recurrence relation for the `Γ` integral. -/
-theorem Gamma_integral_add_one {s : ℂ} (hs: 1 ≤ s.re) :
+theorem Gamma_integral_add_one {s : ℂ} (hs: 0 < s.re) :
   Gamma_integral (s + 1) = s * Gamma_integral s :=
 begin
   suffices : tendsto (s+1).partial_Gamma at_top (𝓝 $ s * Gamma_integral s),
@@ -255,73 +254,81 @@ end Gamma_recurrence
 
 section Gamma_def
 
-/-- Th `n`th function in this family is `Γ(s)` if `1-n ≤ s.re`, and junk otherwise. -/
+/-- The `n`th function in this family is `Γ(s)` if `-n < s.re`, and junk otherwise. -/
 noncomputable def Gamma_aux : ℕ → (ℂ → ℂ)
 | 0      := Gamma_integral
 | (n+1)  := λ s:ℂ, (Gamma_aux n (s+1)) / s
 
-lemma Gamma_aux_recurrence1 (s : ℂ) (n : ℕ) (h1 : 1 - s.re ≤ ↑n) :
+lemma Gamma_aux_recurrence1 (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) :
   Gamma_aux n s = Gamma_aux n (s+1) / s :=
 begin
   induction n with n hn generalizing s,
-  { simp only [nat.cast_zero, sub_nonpos] at h1,
+  { simp only [nat.cast_zero, neg_lt_zero] at h1,
     dsimp only [Gamma_aux], rw Gamma_integral_add_one h1,
     rw [mul_comm, mul_div_cancel], contrapose! h1, rw h1,
     simp },
   { dsimp only [Gamma_aux],
-    have hh1 : 1 - (s+1).re ≤ n,
+    have hh1 : -(s+1).re < n,
     { rw [nat.succ_eq_add_one, nat.cast_add, nat.cast_one] at h1,
       rw [add_re, one_re], linarith, },
     rw ←(hn (s+1) hh1) }
 end
 
-lemma Gamma_aux_recurrence2 (s : ℂ) (n : ℕ) (h1 : 1 - s.re ≤ ↑n) :
+lemma Gamma_aux_recurrence2 (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) :
   Gamma_aux n s = Gamma_aux (n+1) s :=
 begin
   cases n,
-  { simp only [nat.cast_zero, sub_nonpos] at h1,
+  { simp only [nat.cast_zero, neg_lt_zero] at h1,
     dsimp only [Gamma_aux], rw Gamma_integral_add_one h1,
     have : s ≠ 0 := by { contrapose! h1, rw h1, simp, },
     field_simp, ring },
   { dsimp only [Gamma_aux],
     have : (Gamma_aux n (s + 1 + 1)) / (s+1) = Gamma_aux n (s + 1),
-    { have hh1 : 1 - (s+1).re ≤ n,
+    { have hh1 : -(s+1).re < n,
       { rw [nat.succ_eq_add_one, nat.cast_add, nat.cast_one] at h1,
         rw [add_re, one_re], linarith, },
       rw Gamma_aux_recurrence1 (s+1) n hh1, },
     rw this },
 end
 
+
 /-- The `Γ` function (of a complex variable `s`). -/
-def Gamma (s : ℂ) : ℂ := Gamma_aux ⌈ 1 - s.re ⌉₊ s
+def Gamma (s : ℂ) : ℂ := Gamma_aux ⌊1 - s.re⌋₊ s
 
-lemma Gamma_eq_Gamma_aux (s : ℂ) (n : ℕ) (h1 : 1 - s.re ≤ ↑n) : Gamma s = Gamma_aux n s :=
+lemma Gamma_eq_Gamma_aux (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) : Gamma s = Gamma_aux n s :=
 begin
-  have u : ∀ (k : ℕ), Gamma_aux (⌈ 1 - s.re ⌉₊ + k) s = Gamma s,
+  have u : ∀ (k : ℕ), Gamma_aux (⌊1 - s.re⌋₊ + k) s = Gamma s,
   { intro k, induction k with k hk,
     { simp [Gamma],},
     { rw [←hk, nat.succ_eq_add_one, ←add_assoc],
-      refine (Gamma_aux_recurrence2 s (⌈ 1 - s.re ⌉₊ + k) _).symm,
+      refine (Gamma_aux_recurrence2 s (⌊1 - s.re⌋₊ + k) _).symm,
       rw nat.cast_add,
-      have i1 := nat.le_ceil (1 - s.re),
-      refine le_add_of_le_of_nonneg i1 _,
+      have i0 := nat.sub_one_lt_floor (1 - s.re),
+      simp only [sub_sub_cancel_left] at i0,
+      refine lt_add_of_lt_of_nonneg i0 _,
       rw [←nat.cast_zero, nat.cast_le], exact nat.zero_le k, } },
-  rw [←nat.add_sub_of_le (nat.ceil_le.mpr h1), u (n - ⌈ 1 - s.re ⌉₊)],
+  convert (u $ n - ⌊1 - s.re⌋₊).symm, rw nat.add_sub_of_le,
+  by_cases (0 ≤ 1 - s.re),
+  { apply nat.le_of_lt_succ,
+    exact_mod_cast lt_of_le_of_lt (nat.floor_le h) (by linarith : 1 - s.re < n + 1) },
+  { rw nat.floor_of_nonpos, linarith, linarith },
 end
 
 /-- The recurrence relation for the `Γ` function. -/
 theorem Gamma_add_one (s : ℂ) (h2 : s ≠ 0) : Gamma (s+1) = s * Gamma s :=
 begin
-  let n := ⌈ 1 - s.re ⌉₊,
-  have t1 : 1 - s.re ≤ n := nat.le_ceil (1 - s.re),
-  have t2 : 1 - (s+1).re ≤ n := by { rw [add_re, one_re], linarith, },
+  let n := ⌊1 - s.re⌋₊,
+  have t1 : -s.re < n,
+  { simpa only [sub_sub_cancel_left] using nat.sub_one_lt_floor (1 - s.re) },
+  -- := nat.le_ceil (1 - s.re),
+  have t2 : -(s+1).re < n := by { rw [add_re, one_re], linarith, },
   rw [Gamma_eq_Gamma_aux s n t1, Gamma_eq_Gamma_aux (s+1) n t2, Gamma_aux_recurrence1 s n t1],
-  field_simp, ring
+  field_simp, ring,
 end
 
-theorem Gamma_eq_integral (s : ℂ) (hs : 1 ≤ s.re) : Gamma s = Gamma_integral s :=
+theorem Gamma_eq_integral (s : ℂ) (hs : 0 < s.re) : Gamma s = Gamma_integral s :=
 begin
-  refine Gamma_eq_Gamma_aux s 0 (_ : _ ≤ 0), linarith
+  refine Gamma_eq_Gamma_aux s 0 (_ : _ < 0), linarith,
 end
 
 theorem Gamma_nat_eq_factorial (n : ℕ) : Gamma (n+1) = nat.factorial n :=
@@ -372,8 +379,7 @@ end
 lemma dGamma_integral_abs_convergent (s : ℝ) (hs : 1 < s) :
   integrable_on (λ x:ℝ, ∥exp (-x) * log x * x ^ (s-1)∥) (Ioi 0) :=
 begin
-  have : Ioi (0:ℝ) = Ioc 0 1 ∪ Ioi 1 := by simp,
-  rw [this, integrable_on_union],
+  rw [←Ioc_union_Ioi_eq_Ioi (@zero_le_one ℝ _ _ _ _), integrable_on_union],
   refine ⟨⟨_, _⟩, _⟩,
   { refine continuous_on.ae_strongly_measurable (continuous_on.mul _ _).norm measurable_set_Ioc,
     { refine (continuous_exp.comp continuous_neg).continuous_on.mul (continuous_on_log.mono _),
@@ -383,7 +389,7 @@ begin
     swap, { exact 1 / (s - 1), },
     refine (ae_restrict_iff' measurable_set_Ioc).mpr (ae_of_all _ (λ x hx, _)),
     rw [norm_norm, norm_eq_abs, mul_assoc, abs_mul],
-    have : 1/(s-1) = 1 * (1 / (s-1)) := by ring, rw this,
+    have : 1 / (s - 1) = 1 * (1 / (s - 1)) := by ring, rw this,
     refine mul_le_mul _ _ (by apply abs_nonneg) zero_le_one,
     { rw [abs_of_pos (exp_pos(-x)), exp_le_one_iff, neg_le, neg_zero], exact hx.1.le },
     { apply le_of_lt, refine abs_log_mul_self_rpow_lt x (s-1) hx.1 hx.2 (by linarith), }, },
@@ -475,7 +481,7 @@ begin
     have := ((has_deriv_at_id t).sub_const 1).const_cpow (or.inl (of_real_ne_zero.mpr hx.ne')),
     rwa mul_one at this },
   exact (has_deriv_at_integral_of_dominated_loc_of_deriv_le eps_pos hF_meas
-    (Gamma_integral_convergent hs.le) hF'_meas h_bound bound_integrable h_diff),
+    (Gamma_integral_convergent (zero_lt_one.trans hs)) hF'_meas h_bound bound_integrable h_diff),
 end
 
 lemma differentiable_at_Gamma_aux (s : ℂ) (n : ℕ) (h1 : (1 - s.re) < n ) (h2 : ∀ m:ℕ, s + m ≠ 0) :
@@ -509,7 +515,7 @@ begin
     refine continuous.is_open_preimage continuous_re _ is_open_Ioi, },
   apply eventually_eq_of_mem this,
   intros t ht, rw mem_set_of_eq at ht,
-  apply Gamma_eq_Gamma_aux, exact ht.le,
+  apply Gamma_eq_Gamma_aux, linarith,
 end
 
 end complex