Source indexedlemma · leanprover/lean4:v4.32.0

ZetaAppendix.hasDerivAt_cos_antideriv

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2749 to 2775

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma hasDerivAt_cos_antideriv (n : ℕ) (x : ℝ) :    HasDerivAt      (fun y : ℝ ↦        ((-Real.cos (2 * Real.pi * (n + 1 : ℝ) * y) /          (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2)) : ℂ))      ((Real.sin (2 * Real.pi * (n + 1 : ℝ) * x) /        (Real.pi * (n + 1 : ℝ))) : ℂ) x := by  have hden : 2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2 ≠ 0 := by positivity  have hcos :      HasDerivAt        (fun y : ℝ ↦ Real.cos (2 * Real.pi * (n + 1 : ℝ) * y))        (-(2 * Real.pi * (n + 1 : ℝ)) *          Real.sin (2 * Real.pi * (n + 1 : ℝ) * x)) x := by    convert!      (Real.hasDerivAt_cos (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.cos (2 * Real.pi * (n + 1 : ℝ) * y) /            (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2))        (Real.sin (2 * Real.pi * (n + 1 : ℝ) * x) /          (Real.pi * (n + 1 : ℝ))) x := by    convert! hcos.neg.div_const (2 * Real.pi ^ 2 * (n + 1 : ℝ) ^ 2) using 1    field_simp [hden]  simpa using hreal.ofReal_comp