Source indexedlemma · leanprover/lean4:v4.32.0

Stirling.GammaAux.prod_norm_le_pow

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.GammaStirlingAux · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/GammaStirlingAux.lean:60 to 67

Source documentation

Product bound: |∏_{k < m} (s-1-k)| ≤ |s|^m

Exact Lean statement

lemma prod_norm_le_pow {s : ℂ} {m : ℕ} (h : ∀ k < m, (k : ℝ) + 1 < s.re) :
    ‖∏ k ∈ Finset.range m, (s - 1 - k)‖ ≤ ‖s‖ ^ m

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

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]