Source indexedlemma · leanprover/lean4:v4.32.0

Complex.Hadamard.cartanProductConstant_nonneg

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanMajorantBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanMajorantBound.lean:67 to 75

Mathematical statement

Exact Lean statement

lemma cartanProductConstant_nonneg {m : ℕ} {τ Sτ : ℝ} (hSτ : 0 ≤ Sτ) :
    0 ≤ cartanProductConstant m τ Sτ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma cartanProductConstant_nonneg {m : ℕ} {τ Sτ : ℝ} (hSτ : 0 ≤ Sτ) :    0 ≤ cartanProductConstant m τ Sτ := by  have hS : 0 ≤ Sτ + 1 := by linarith  have hA : 0 ≤ (CartanBound.Cφ + (2 : ℝ) * m) * (4 : ℝ) ^ τ + 3 := by    have hCφ : 0 ≤ CartanBound.Cφ := le_of_lt CartanBound.Cφ_pos    have hm0 : 0 ≤ (m : ℝ) := by exact_mod_cast (Nat.zero_le m)    have h4τ : 0 ≤ (4 : ℝ) ^ τ := by positivity    nlinarith [hCφ, hm0, h4τ]  simpa [cartanProductConstant] using mul_nonneg hA hS