Source indexedlemma · leanprover/lean4:v4.32.0

BKLNW.pTd_hasDerivAt

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:551 to 563

Mathematical statement

Exact Lean statement

lemma pTd_hasDerivAt (m : ℕ) (c y : ℝ) : HasDerivAt (pTd m c) (pTdd m c y) y

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma pTd_hasDerivAt (m : ℕ) (c y : ℝ) : HasDerivAt (pTd m c) (pTdd m c y) y := by  unfold pTd pTdd  have hP : HasDerivAt (fun u : ℝ => ((m + 2 : ℕ) : ℝ) * u ^ (m + 1) - c * u ^ (m + 2))      (((m + 2 : ℕ) : ℝ) * (((m + 1 : ℕ) : ℝ) * y ^ m) - c * (((m + 2 : ℕ) : ℝ) * y ^ (m + 1))) y := by    have ha : HasDerivAt (fun u : ℝ => u ^ (m + 1)) (((m + 1 : ℕ) : ℝ) * y ^ m) y :=      hasDerivAt_pow (m + 1) y    have hb : HasDerivAt (fun u : ℝ => u ^ (m + 2)) (((m + 2 : ℕ) : ℝ) * y ^ (m + 1)) y :=      hasDerivAt_pow (m + 2) y    exact (ha.const_mul _).sub (hb.const_mul _)  have hlin : HasDerivAt (fun u : ℝ => -(c * u)) (-(c * 1)) y := ((hasDerivAt_id y).const_mul c).neg  have he : HasDerivAt (fun u : ℝ => Real.exp (-(c * u))) (Real.exp (-(c * y)) * (-(c * 1))) y := hlin.exp  convert! hP.mul he using 1  ring