Source indexedlemma · leanprover/lean4:v4.32.0

BKLNW.Pp'_hasDerivAt

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:606 to 615

Mathematical statement

Exact Lean statement

lemma Pp'_hasDerivAt (m : ℕ) (A₁ A₂ E y : ℝ) : HasDerivAt (Pp' m A₁ A₂ E) (Pp'' m A₁ A₂ E y) y

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Pp'_hasDerivAt (m : ℕ) (A₁ A₂ E y : ℝ) : HasDerivAt (Pp' m A₁ A₂ E) (Pp'' m A₁ A₂ E y) y := by  unfold Pp' Pp''  have h1 := (pTd_hasDerivAt m (1 / 2) y).const_mul A₁  have h2 := (pTd_hasDerivAt m (2 / 3) y).const_mul A₂  have h3 : HasDerivAt (fun u : ℝ => E * (((m + 2 : ℕ) : ℝ) * u ^ (m + 1)))      (E * (((m + 2 : ℕ) : ℝ) * (((m + 1 : ℕ) : ℝ) * y ^ m))) y := by    have hb : HasDerivAt (fun u : ℝ => u ^ (m + 1)) (((m + 1 : ℕ) : ℝ) * y ^ m) y :=      hasDerivAt_pow (m + 1) y    exact (hb.const_mul (((m + 2 : ℕ) : ℝ))).const_mul E  exact (h1.add h2).add h3