Source indexedlemma · leanprover/lean4:v4.32.0

BKLNW.expTd_hasDerivAt

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:116 to 126

Mathematical statement

Exact Lean statement

lemma expTd_hasDerivAt (c y : ℝ) : HasDerivAt (expTd c) (expTdd c y) y

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma expTd_hasDerivAt (c y : ℝ) : HasDerivAt (expTd c) (expTdd c y) y := by  unfold expTd expTdd  have hP : HasDerivAt (fun u : ℝ => 5 * u ^ 4 - c * u ^ 5) (20 * y ^ 3 - 5 * c * y ^ 4) y := by    have h4 : HasDerivAt (fun u : ℝ => u ^ 4) (4 * y ^ 3) y := by simpa using hasDerivAt_pow 4 y    have h5 : HasDerivAt (fun u : ℝ => u ^ 5) (5 * y ^ 4) y := by simpa using hasDerivAt_pow 5 y    convert! (h4.const_mul (5 : ℝ)).sub (h5.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