Source indexedlemma · leanprover/lean4:v4.32.0

ZetaAppendix.fourier_partial_sum_eq_range_cos

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3343 to 3354

Mathematical statement

Exact Lean statement

lemma fourier_partial_sum_eq_range_cos (s : ℂ) {a b : ℝ} (ha : 0 < a)
    (hab : a < b) (N : ℕ) :
    let f : ℝ → ℂ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma fourier_partial_sum_eq_range_cos (s : ℂ) {a b : ℝ} (ha : 0 < a)    (hab : a < b) (N : ℕ) :    let f : ℝ → ℂ := fun y ↦      if a ≤ y ∧ y ≤ b then (y ^ (-s.re) : ℝ) * e (-(s.im / (2 * π)) * Real.log y) else 0    ∑ n ∈ Icc 1 N, (FourierTransform.fourier f n + FourierTransform.fourier f (-n)) =      ∑ n ∈ range N,        2 * ∫ y in a..b, (y : ℂ) ^ (-s) * Real.cos (2 * π * (n + 1) * y) := by  dsimp only  rw [sum_Icc_one_eq_sum_range_succ]  apply sum_congr rfl  intro n _hn  simpa using (lemma_abadsumas_sum_fourier (s := s) (a := a) (b := b) ha hab n)