Source indexedlemma · leanprover/lean4:v4.32.0

Stirling.GammaAux.Gamma_iterate

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.GammaStirlingAux · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/GammaStirlingAux.lean:71 to 99

Source documentation

Product bound: |∏_{k < m} (s-1-k)| ≤ |s|^m -/ lemma prod_norm_le_pow {s : ℂ} {m : ℕ} (h : ∀ k < m, (k : ℝ) + 1 < s.re) : ‖∏ k ∈ Finset.range m, (s - 1 - k)‖ ≤ ‖s‖ ^ m := by calc ‖∏ k ∈ Finset.range m, (s - 1 - k)‖ = ∏ k ∈ Finset.range m, ‖s - 1 - k‖ := norm_prod _ _ _ ≤ ∏ _k ∈ Finset.range m, ‖s‖ := by apply Finset.prod_le_prod (fun k _ => norm_nonneg _) intro k hk; exact norm_shift_le (h k (Finset.mem_range.mp hk)) _ = ‖s‖ ^ m := by rw [Finset.prod_const, Finset.card_range]

/-! ## Iterated functional equation

Exact Lean statement

lemma Gamma_iterate {s : ℂ} {n : ℕ} (hs : ∀ k < n, s - 1 - k ≠ 0) :
    Complex.Gamma s = Complex.Gamma (s - n) * ∏ k ∈ Finset.range n, (s - 1 - k)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Gamma_iterate {s : ℂ} {n : ℕ} (hs : ∀ k < n, s - 1 - k ≠ 0) :    Complex.Gamma s = Complex.Gamma (s - n) * ∏ k ∈ Finset.range n, (s - 1 - k) := by  induction n with  | zero => simp  | succ m ih =>    have h_prev : ∀ k < m, s - 1 - k ≠ 0 := fun k hk => hs k (Nat.lt_succ_of_lt hk)    have h_curr : s - 1 - m ≠ 0 := hs m (Nat.lt_succ_self m)    have h_func : Complex.Gamma (s - m) = (s - m - 1) * Complex.Gamma (s - m - 1) := by      have h_ne : s - ↑m - 1 ≠ 0 := by convert h_curr using 1; ring      have := Complex.Gamma_add_one (s - m - 1) h_ne      simp only [sub_add_cancel] at this      exact this    have h_cast : s - ↑(m + 1) = s - m - 1 := by simp only [Nat.cast_add, Nat.cast_one]; ring    have h_prod_eq : (s - m - 1) * ∏ k ∈ Finset.range m, (s - 1 - k) =        ∏ k ∈ Finset.range (m + 1), (s - 1 - k) := by      rw [Finset.prod_range_succ]; ring    calc      Complex.Gamma s          = Complex.Gamma (s - m) * ∏ k ∈ Finset.range m, (s - 1 - k) := ih h_prev      _ = (s - m - 1) * Complex.Gamma (s - m - 1)            * ∏ k ∈ Finset.range m, (s - 1 - k) := by          rw [h_func]      _ = Complex.Gamma (s - m - 1) *            ((s - m - 1) * ∏ k ∈ Finset.range m, (s - 1 - k)) := by          ring      _ = Complex.Gamma (s - m - 1) * ∏ k ∈ Finset.range (m + 1), (s - 1 - k) := by          rw [h_prod_eq]      _ = Complex.Gamma (s - ↑(m + 1)) * ∏ k ∈ Finset.range (m + 1), (s - 1 - k) := by          rw [← h_cast]