Source indexedtheorem · leanprover/lean4:v4.32.0

fejer_integrand_periodic

PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:620 to 628

Mathematical statement

Exact Lean statement

theorem fejer_integrand_periodic (f : ℝ → ℝ) (hf_per : Function.Periodic f (2 * Real.pi)) (n : ℕ) (x : ℝ) :
    Function.Periodic (fun t => f (x - t) * fejer_kernel n t) (2 * Real.pi)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem fejer_integrand_periodic (f : ℝ → ℝ) (hf_per : Function.Periodic f (2 * Real.pi)) (n : ℕ) (x : ℝ) :    Function.Periodic (fun t => f (x - t) * fejer_kernel n t) (2 * Real.pi) := by      intro t; unfold fejer_kernel; simp +decide [ *, Real.sin_two_mul _, mul_assoc ] ; ring_nf;      simp +decide [ mul_assoc, mul_comm Real.pi _, mul_left_comm Real.pi _, add_comm, add_left_comm, add_assoc, hf_per ];      rw [ show x + ( -t - 2 * Real.pi ) = x - t - 2 * Real.pi by ring ] ; rw [ ← hf_per ] ; simp +decide [ sub_eq_add_neg, add_assoc, add_left_comm, add_comm, Finset.sum_add_distrib ] ; ring;      simp +decide [ mul_two, Real.sin_add, Real.cos_add, dirichlet_kernel ];      norm_num [ add_assoc, mul_add, Real.cos_add ];      norm_num [ ← sq, Real.cos_sq' ];      norm_num [ ← two_mul, Real.sin_two_mul ]