feat(Analysis/SpecialFunctions): hide Gamma func implementation details (leanprover-community#38447)

The definition of the gamma function relies on an auxiliary declaration `gammaAux`, which is of no interest once the actual gamma function is built. This PR makes `gammaAux` and its cousins private, and un-`expose`'s the definition of the gamma function (which is fine because there are plenty of API lemmas about it, so we do not need to unfold its actual definition downstream).

Author: loefflerd

Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

@@ -38,7 +38,7 @@ set it to be `0` by convention.)
 Gamma
 -/
 
-@[expose] public section
+public section
 
 
 noncomputable section
@@ -107,7 +107,7 @@ theorem GammaIntegral_convergent {s : ℂ} (hs : 0 < s.re) :
 
 See `Complex.GammaIntegral_convergent` for a proof of the convergence of the integral for
 `0 < re s`. -/
-def GammaIntegral (s : ℂ) : ℂ :=
+@[expose] def GammaIntegral (s : ℂ) : ℂ :=
   ∫ x in Ioi (0 : ℝ), ↑(-x).exp * ↑x ^ (s - 1)
 
 set_option backward.isDefEq.respectTransparency false in
@@ -145,7 +145,7 @@ namespace Complex
 section GammaRecurrence
 
 /-- The indefinite version of the `Γ` function, `Γ(s, X) = ∫ x ∈ 0..X, exp(-x) x ^ (s - 1)`. -/
-def partialGamma (s : ℂ) (X : ℝ) : ℂ :=
+@[expose] def partialGamma (s : ℂ) (X : ℝ) : ℂ :=
   ∫ x in 0..X, (-x).exp * x ^ (s - 1)
 
 theorem tendsto_partialGamma {s : ℂ} (hs : 0 < s.re) :
@@ -248,11 +248,11 @@ end GammaRecurrence
 section GammaDef
 
 /-- The `n`th function in this family is `Γ(s)` if `-n < s.re`, and junk otherwise. -/
-noncomputable def GammaAux : ℕ → ℂ → ℂ
+private noncomputable def GammaAux : ℕ → ℂ → ℂ
   | 0 => GammaIntegral
   | n + 1 => fun s : ℂ => GammaAux n (s + 1) / s
 
-theorem GammaAux_recurrence1 (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) :
+private theorem GammaAux_recurrence1 (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) :
     GammaAux n s = GammaAux n (s + 1) / s := by
   induction n generalizing s with
   | zero =>
@@ -267,7 +267,7 @@ theorem GammaAux_recurrence1 (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) :
       rw [add_re, one_re]; linarith
     rw [← hn (s + 1) hh1]
 
-theorem GammaAux_recurrence2 (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) :
+private theorem GammaAux_recurrence2 (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) :
     GammaAux n s = GammaAux (n + 1) s := by
   rcases n with - | n
   · simp only [CharP.cast_eq_zero, Left.neg_neg_iff] at h1
@@ -284,12 +284,13 @@ theorem GammaAux_recurrence2 (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) :
       rw [GammaAux_recurrence1 (s + 1) n hh1]
     rw [this]
 
+/- This definition is deliberately not @[expose]'d, since `GammaAux` is not mathematically
+interesting. -/
 /-- The `Γ` function (of a complex variable `s`). -/
-@[pp_nodot]
-irreducible_def Gamma (s : ℂ) : ℂ :=
+@[irreducible, pp_nodot] def Gamma (s : ℂ) : ℂ :=
   GammaAux ⌊1 - s.re⌋₊ s
 
-theorem Gamma_eq_GammaAux (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) : Gamma s = GammaAux n s := by
+private theorem Gamma_eq_GammaAux (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) : Gamma s = GammaAux n s := by
   have u : ∀ k : ℕ, GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s := fun k ↦ by
     induction k with
     | zero => simp [Gamma]
@@ -401,8 +402,7 @@ end Complex
 namespace Real
 
 /-- The `Γ` function (of a real variable `s`). -/
-@[pp_nodot]
-def Gamma (s : ℝ) : ℝ :=
+@[pp_nodot, expose] def Gamma (s : ℝ) : ℝ :=
   (Complex.Gamma s).re
 
 theorem Gamma_eq_integral {s : ℝ} (hs : 0 < s) :

Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean

@@ -336,31 +336,30 @@ theorem approx_Gamma_integral_tendsto_Gamma_integral {s : ℂ} (hs : 0 < re s) :
 
 /-- Euler's limit formula for the complex Gamma function. -/
 theorem GammaSeq_tendsto_Gamma (s : ℂ) : Tendsto (GammaSeq s) atTop (𝓝 <| Gamma s) := by
-  suffices ∀ m : ℕ, -↑m < re s → Tendsto (GammaSeq s) atTop (𝓝 <| GammaAux m s) by
-    rw [Gamma]
-    apply this
-    rw [neg_lt]
-    rcases lt_or_ge 0 (re s) with (hs | hs)
-    · exact (neg_neg_of_pos hs).trans_le (Nat.cast_nonneg _)
-    · refine (Nat.lt_floor_add_one _).trans_le ?_
-      rw [sub_eq_neg_add, Nat.floor_add_one (neg_nonneg.mpr hs), Nat.cast_add_one]
+  suffices ∀ m : ℕ, ⌊1 - s.re⌋₊ = m → Tendsto (GammaSeq s) atTop (𝓝 <| Gamma s) by tauto
   intro m
   induction m generalizing s with intro hs
   | zero => -- Base case: `0 < re s`, so Gamma is given by the integral formula
-    rw [Nat.cast_zero, neg_zero] at hs
-    rw [← Gamma_eq_GammaAux]
-    · refine Tendsto.congr' ?_ (approx_Gamma_integral_tendsto_Gamma_integral hs)
-      refine (eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn => ?_)
-      exact (GammaSeq_eq_approx_Gamma_integral hs hn).symm
-    · rwa [Nat.cast_zero, neg_lt_zero]
+    rw [Nat.floor_eq_zero, sub_lt_self_iff] at hs
+    apply (approx_Gamma_integral_tendsto_Gamma_integral hs).congr'
+    filter_upwards [eventually_ne_atTop 0] with n hn using
+      (GammaSeq_eq_approx_Gamma_integral hs hn).symm
   | succ m IH => -- Induction step: use recurrence formulae in `s` for Gamma and GammaSeq
-    rw [Nat.cast_succ, neg_add, ← sub_eq_add_neg, sub_lt_iff_lt_add, ← one_re, ← add_re] at hs
-    rw [GammaAux]
-    have := @Tendsto.congr' _ _ _ ?_ _ _
-      ((eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn => ?_)) ((IH _ hs).div_const s)
-    pick_goal 3; · exact GammaSeq_add_one_left s hn -- doesn't work if inlined?
-    conv at this => arg 1; intro n; rw [mul_comm]
-    rwa [← mul_one (GammaAux m (s + 1) / s), tendsto_mul_iff_of_ne_zero _ (one_ne_zero' ℂ)] at this
+    -- Silly case `s = 0`: both sides are zero
+    rcases eq_or_ne s 0 with rfl | hsne
+    · unfold GammaSeq
+      simp [Finset.prod_range_succ']
+    specialize IH (s + 1) ?_
+    · rw [Nat.floor_eq_iff' (by lia)] at hs
+      have : s.re ≤ -m := by grind
+      rw [Nat.floor_eq_iff <| by simpa using (show s.re ≤ 0 by grind)]
+      grind [add_re, one_re]
+    rw [Gamma_add_one _ hsne] at IH
+    have := (IH.div_const s).congr' <| by
+      filter_upwards [eventually_ne_atTop 0] with n using GammaSeq_add_one_left s
+    simp only [mul_comm _ (s.GammaSeq _)] at this
+    rwa [mul_div_cancel_left₀ _ hsne, ← mul_one (Gamma s),
+      tendsto_mul_iff_of_ne_zero _ (one_ne_zero' ℂ)] at this
     simp_rw [add_assoc]
     exact tendsto_natCast_div_add_atTop (1 + s)
 

Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean

@@ -61,43 +61,26 @@ theorem hasDerivAt_GammaIntegral {s : ℂ} (hs : 0 < s.re) :
     rw [(by simp : (1 : ℂ) = Real.exp (-0))]
     exact (continuous_ofReal.comp (Real.continuous_exp.comp continuous_neg)).continuousWithinAt
 
-theorem differentiableAt_GammaAux (s : ℂ) (n : ℕ) (h1 : 1 - s.re < n) (h2 : ∀ m : ℕ, s ≠ -m) :
-    DifferentiableAt ℂ (GammaAux n) s := by
-  induction n generalizing s with
-  | zero =>
-    refine (hasDerivAt_GammaIntegral ?_).differentiableAt
-    rw [Nat.cast_zero] at h1; linarith
-  | succ n hn =>
-    dsimp only [GammaAux]
-    specialize hn (s + 1)
-    have a : 1 - (s + 1).re < ↑n := by
-      rw [Nat.cast_succ] at h1; rw [Complex.add_re, Complex.one_re]; linarith
-    have b : ∀ m : ℕ, s + 1 ≠ -m := by
-      intro m; have := h2 (1 + m)
-      contrapose this
-      rw [← eq_sub_iff_add_eq] at this
-      simpa using this
-    refine DifferentiableAt.div (DifferentiableAt.comp _ (hn a b) ?_) ?_ ?_
-    · rw [differentiableAt_add_const_iff (1 : ℂ)]; exact differentiableAt_id
-    · exact differentiableAt_id
-    · simpa using h2 0
-
 @[fun_prop]
 theorem differentiableAt_Gamma (s : ℂ) (hs : ∀ m : ℕ, s ≠ -m) : DifferentiableAt ℂ Gamma s := by
-  let n := ⌊1 - s.re⌋₊ + 1
-  have hn : 1 - s.re < n := mod_cast Nat.lt_floor_add_one (1 - s.re)
-  apply (differentiableAt_GammaAux s n hn hs).congr_of_eventuallyEq
-  let S := {t : ℂ | 1 - t.re < n}
-  have : S ∈ 𝓝 s := by
-    rw [mem_nhds_iff]; use S
-    refine ⟨Subset.rfl, ?_, hn⟩
-    have : S = re ⁻¹' Ioi (1 - n : ℝ) := by
-      ext; rw [preimage, Ioi, mem_setOf_eq, mem_setOf_eq, mem_setOf_eq]; exact sub_lt_comm
-    rw [this]
-    exact Continuous.isOpen_preimage continuous_re _ isOpen_Ioi
-  apply eventuallyEq_of_mem this
-  intro t ht; rw [mem_setOf_eq] at ht
-  apply Gamma_eq_GammaAux; linarith
+  -- We will show, by induction on `n`, that `Gamma` is differentiable on `-n < Re s`.
+  suffices ∀ (n : ℕ) (s : ℂ) (hsre : -n < s.re) (hs : ∀ m : ℕ, s ≠ -m), DifferentiableAt ℂ _ s from
+    this (⌊-s.re⌋₊ + 1) s (by grind [Nat.lt_floor_add_one (-s.re)]) hs
+  intro n s hsre hs
+  induction n generalizing s with
+  | zero =>
+    -- Case `n = 0`: use relation to `gammaIntegral`
+    replace hsre : 0 < s.re := by simpa using hsre
+    have : IsOpen {s : ℂ | 0 < s.re} := continuous_re.isOpen_preimage _ isOpen_Ioi
+    apply (hasDerivAt_GammaIntegral (by simpa using hsre)).differentiableAt.congr_of_eventuallyEq
+    filter_upwards [this.mem_nhds hsre] with a using Gamma_eq_integral
+  | succ n IH =>
+    -- Induction step: use recurrence relation
+    have hsne : s ≠ 0 := by grind [hs 0]
+    specialize IH (s + 1) (by grind [add_re, one_re]) (fun m ↦ by grind [hs (m + 1)])
+    have := IH.comp s (show DifferentiableAt ℂ (fun s ↦ s + 1) s by fun_prop)
+    apply (this.fun_div differentiableAt_id hsne).congr_of_eventuallyEq
+    filter_upwards [isOpen_ne.mem_nhds hsne] using by grind [Gamma_add_one]
 
 theorem differentiableAt_Gamma_one : DifferentiableAt ℂ Gamma 1 :=
   differentiableAt_Gamma 1 (by norm_cast; simp)