Source indexedlemma · leanprover/lean4:v4.32.0

ZetaAppendix.cos_antideriv_norm_bound

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2891 to 2905

Mathematical statement

Exact Lean statement

lemma cos_antideriv_norm_bound (n : ℕ) (x : ℝ) :
    ‖((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * x) /
      (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ)‖ ≤
        1 / (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma cos_antideriv_norm_bound (n : ℕ) (x : ℝ) :    ‖((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * x) /      (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ)‖ ≤        1 / (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2) := by  have hden_pos : 0 < 2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2 := by positivity  have hden_norm :      ‖(2 * (Real.pi : ℂ) ^ 2 * (((n : ℝ) + 1 : ℝ) : ℂ) ^ 2)‖ =        2 * Real.pi ^ 2 * ((n : ℝ) + 1) ^ 2 := by    norm_num [Complex.norm_real, Real.norm_eq_abs, abs_of_pos hden_pos]    rw [← Complex.normSq_eq_norm_sq]    simp [Complex.normSq]    ring_nf  rw [norm_div, norm_neg, Complex.norm_real, Real.norm_eq_abs, hden_norm]  gcongr  exact Real.abs_cos_le_one _