Source indexedlemma · leanprover/lean4:v4.32.0

BKLNW.eTd_hasDerivAt

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:440 to 448

Mathematical statement

Exact Lean statement

lemma eTd_hasDerivAt (c y : ℝ) : HasDerivAt (eTd c) (eTdd c y) y

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma eTd_hasDerivAt (c y : ℝ) : HasDerivAt (eTd c) (eTdd c y) y := by  unfold eTd eTdd  have hP : HasDerivAt (fun u : ℝ => 1 - c * u) (-(c * 1)) y := by    convert! (hasDerivAt_const y (1 : ℝ)).sub ((hasDerivAt_id y).const_mul c) using 1    ring  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