Source indexedlemma · leanprover/lean4:v4.32.0

ZetaAppendix.hasSum_cos_over_pi_sq_unit_raw

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2613 to 2628

Mathematical statement

Exact Lean statement

lemma hasSum_cos_over_pi_sq_unit_raw {x : ℝ} (hx : x ∈ Set.Icc (0 : ℝ) 1) :
    HasSum
      (fun n : ℕ ↦
        ((n + 1 : ℝ) ^ (2 * 1))⁻¹ *
          Real.cos (2 * Real.pi * (n + 1 : ℝ) * x) / Real.pi ^ 2)
      (x ^ 2 - x + 1 / 6)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma hasSum_cos_over_pi_sq_unit_raw {x : ℝ} (hx : x ∈ Set.Icc (0 : ℝ) 1) :    HasSum      (fun n : ℕ ↦        ((n + 1 : ℝ) ^ (2 * 1))⁻¹ *          Real.cos (2 * Real.pi * (n + 1 : ℝ) * x) / Real.pi ^ 2)      (x ^ 2 - x + 1 / 6) := by  have h := hasSum_one_div_nat_pow_mul_cos (k := 1) one_ne_zero hx  rw [← hasSum_nat_add_iff' 1] at h  norm_num at h  have h_eval :      (Polynomial.aeval x) (Polynomial.bernoulli 2) =        x ^ 2 - x + 1 / 6 := by    simpa [bernoulliFun] using bernoulliFun_two x  convert! h.div_const (Real.pi ^ 2) using 1  rw [h_eval]  field_simp [Real.pi_ne_zero]