Source indexedlemma · leanprover/lean4:v4.32.0

HasDerivAt_cpow_over_var

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1268 to 1282

Mathematical statement

Exact Lean statement

lemma HasDerivAt_cpow_over_var (N : ℕ) {z : ℂ} (z_ne_zero : z ≠ 0) :
    HasDerivAt (fun z ↦ -(N : ℂ) ^ z / z)
      (((N : ℂ) ^ z / z ^ 2) - (Real.log N * N ^ z / z)) z

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma HasDerivAt_cpow_over_var (N : ℕ) {z : ℂ} (z_ne_zero : z ≠ 0) :    HasDerivAt (fun z ↦ -(N : ℂ) ^ z / z)      (((N : ℂ) ^ z / z ^ 2) - (Real.log N * N ^ z / z)) z := by  simp_rw [div_eq_mul_inv]  convert! HasDerivAt.mul (c := fun z ↦ - (N : ℂ) ^ z) (d := fun z ↦ z⁻¹)    (c' := - (N : ℂ) ^ z * Real.log N)    (d' := - (z ^ 2)⁻¹) ?_ ?_ using 1  · simp only [natCast_log, neg_mul, mul_neg, neg_neg]    ring_nf  · simp only [natCast_log, neg_mul]    apply HasDerivAt.neg    convert! HasDerivAt.const_cpow (c := (N : ℂ)) (f := id) (f' := 1) (x := z) (hasDerivAt_id z)      (by simp [z_ne_zero]) using 1    simp only [id_eq, mul_one]  · exact hasDerivAt_inv z_ne_zero