Source indexedlemma · leanprover/lean4:v4.32.0

dirichletKernel'_periodic

Carleson.Classical.DirichletKernel · Carleson/Classical/DirichletKernel.lean:33 to 62

Mathematical statement

Exact Lean statement

lemma dirichletKernel'_periodic : Function.Periodic (dirichletKernel' N) (2 * π)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma dirichletKernel'_periodic : Function.Periodic (dirichletKernel' N) (2 * π) := by  intro x  simp_rw [dirichletKernel']  push_cast  congr 2  · rw [mul_add, exp_add]    conv => rhs; rw [← mul_one (cexp _)]    congr 1    convert exp_int_mul_two_pi_mul_I N using 2    norm_cast    simp    ring  · congr 1    rw [mul_add, exp_add]    conv => rhs; rw [← mul_one (cexp _)]    congr    convert exp_int_mul_two_pi_mul_I (-1) using 2    ring  · rw [mul_add, exp_add]    conv => rhs; rw [← mul_one (cexp _)]    congr    convert exp_int_mul_two_pi_mul_I (-(N : ℤ)) using 2    simp    ring  · congr 1    rw [mul_add, exp_add]    conv => rhs; rw [← mul_one (cexp _)]    congr    convert exp_int_mul_two_pi_mul_I 1 using 2    ring