English
The derivative of the term term f z n at z = s is given by HasDerivAt (term f z n) at s equals the negative of the term of logMul f at s, n.
Русский
Производная по z от терма L‑серии в точке s равна минусу терма logMul f в s и индексe n.
LaTeX
$$HasDerivAt (\lambda z, term f z n) (-(term (logMul f) s n)) s$$
Lean4
/-- The derivative of the terms of an L-series. -/
theorem hasDerivAt_term (f : ℕ → ℂ) (n : ℕ) (s : ℂ) : HasDerivAt (fun z ↦ term f z n) (-(term (logMul f) s n)) s :=
by
rcases eq_or_ne n 0 with rfl | hn
· simp [hasDerivAt_const]
simp_rw [term_of_ne_zero hn, ← neg_div, ← neg_mul, mul_comm, mul_div_assoc, div_eq_mul_inv, ← cpow_neg]
exact
HasDerivAt.const_mul (f n)
(by
simpa only [mul_comm, ← mul_neg_one (log n), ← mul_assoc] using
(hasDerivAt_neg' s).const_cpow (Or.inl <| Nat.cast_ne_zero.mpr hn))
/- This lemma proves two things at once, since their proofs are intertwined; we give separate
non-private lemmas below that extract the two statements. -/
