Source indexedlemma · leanprover/lean4:v4.32.0

ZetaAppendix.hasDerivAt_sine_antideriv

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2513 to 2536

Mathematical statement

Exact Lean statement

lemma hasDerivAt_sine_antideriv (n : ℕ) (x : ℝ) :
    HasDerivAt
      (fun y : ℝ ↦
        ((Real.sin (2 * Real.pi * (n + 1 : ℝ) * y) /
          (Real.pi * (n + 1 : ℝ))) : ℂ))
      ((2 * Real.cos (2 * Real.pi * (n + 1 : ℝ) * x)) : ℂ) x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma hasDerivAt_sine_antideriv (n : ℕ) (x : ℝ) :    HasDerivAt      (fun y : ℝ ↦        ((Real.sin (2 * Real.pi * (n + 1 : ℝ) * y) /          (Real.pi * (n + 1 : ℝ))) : ℂ))      ((2 * Real.cos (2 * Real.pi * (n + 1 : ℝ) * x)) : ℂ) x := by  have hden : Real.pi * (n + 1 : ℝ) ≠ 0 := by positivity  have hsin :      HasDerivAt        (fun y : ℝ ↦ Real.sin (2 * Real.pi * (n + 1 : ℝ) * y))        ((2 * Real.pi * (n + 1 : ℝ)) *          Real.cos (2 * Real.pi * (n + 1 : ℝ) * x)) x := by    convert!      (Real.hasDerivAt_sin (2 * Real.pi * (n + 1 : ℝ) * x)).comp x        ((hasDerivAt_id x).const_mul (2 * Real.pi * (n + 1 : ℝ))) using 1    ring_nf  have hreal :      HasDerivAt        (fun y : ℝ ↦ Real.sin (2 * Real.pi * (n + 1 : ℝ) * y) /          (Real.pi * (n + 1 : ℝ)))        (2 * Real.cos (2 * Real.pi * (n + 1 : ℝ) * x)) x := by    convert! hsin.div_const (Real.pi * (n + 1 : ℝ)) using 1    field_simp [hden]  simpa using hreal.ofReal_comp