Source indexedlemma · leanprover/lean4:v4.32.0

BKLNW.Gp'_hasDerivAt

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:143 to 151

Mathematical statement

Exact Lean statement

lemma Gp'_hasDerivAt (A₁ A₂ E y : ℝ) : HasDerivAt (Gp' A₁ A₂ E) (Gp'' A₁ A₂ E y) y

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Gp'_hasDerivAt (A₁ A₂ E y : ℝ) : HasDerivAt (Gp' A₁ A₂ E) (Gp'' A₁ A₂ E y) y := by  unfold Gp' Gp''  have h1 := (expTd_hasDerivAt (1 / 2) y).const_mul A₁  have h2 := (expTd_hasDerivAt (2 / 3) y).const_mul A₂  have h3 : HasDerivAt (fun u : ℝ => E * (5 * u ^ 4)) (E * (20 * y ^ 3)) y := by    have h4 : HasDerivAt (fun u : ℝ => u ^ 4) (4 * y ^ 3) y := by simpa using hasDerivAt_pow 4 y    convert! (h4.const_mul (5 : ℝ)).const_mul E using 1    ring  convert! (h1.add h2).add h3 using 1