Source indexedtheorem · leanprover/lean4:v4.32.0

dirichlet_kernel_closed_form

PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:357 to 365

Mathematical statement

Exact Lean statement

theorem dirichlet_kernel_closed_form (n : ℕ) (t : ℝ) (h : Real.sin (t / 2) ≠ 0) :
    dirichlet_kernel n t = Real.sin ((n + 1 / 2) * t) / (2 * Real.sin (t / 2))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem dirichlet_kernel_closed_form (n : ℕ) (t : ℝ) (h : Real.sin (t / 2) ≠ 0) :    dirichlet_kernel n t = Real.sin ((n + 1 / 2) * t) / (2 * Real.sin (t / 2)) := by      unfold dirichlet_kernel;      induction n <;> simp_all +decide [ Finset.sum_Ioc_succ_top, Nat.Icc_succ_left ];      · ring_nf at * ; aesop;      · simp_all +decide [ ← add_assoc ];        field_simp;        rw [ ← Complex.ofReal_inj ] ; norm_num [ Complex.sin, Complex.cos ] ; ring_nf;        norm_num [ mul_assoc, ← Complex.exp_add ] ; ring_nf