LSeries_iteratedDeriv — Mathlib

English

For any natural m, the m-th derivative of LSeries f is (-1)^m times LSeries(logMul^[m] f).

Русский

Для любого натурального m m‑я производная L‑серии равна (-1)^m LSeries(logMul^[m] f).

LaTeX

$$iteratedDeriv m (LSeries f) s = (-1)^{m} * LSeries (logMul^[m] f) s$$

Lean4

/-- If `re s` is greater than the abscissa of absolute convergence of `f`, then
the `m`th derivative of this L-series is `(-1)^m` times the L-series of `log^m * f`. -/
theorem LSeries_iteratedDeriv {f : ℕ → ℂ} (m : ℕ) {s : ℂ} (h : abscissaOfAbsConv f < s.re) :
    iteratedDeriv m (LSeries f) s = (-1) ^ m * LSeries (logMul^[m] f) s := by
  induction m generalizing s with
  | zero => simp
  | succ m
    ih =>
    have ih' :
      {s | abscissaOfAbsConv f < re s}.EqOn (iteratedDeriv m (LSeries f)) ((-1) ^ m * LSeries (logMul^[m] f)) :=
      fun _ hs ↦ ih hs
    have := derivWithin_congr ih' (ih h)
    simp_rw [derivWithin_of_isOpen (isOpen_re_gt_EReal _) h] at this
    rw [iteratedDeriv_succ, this]
    simp [Pi.mul_def, pow_succ, Function.iterate_succ', LSeries_deriv <| absicssaOfAbsConv_logPowMul.symm ▸ h,
      -Function.iterate_succ]

Похожие утверждения