absicssaOfAbsConv_logPowMul — Mathlib

English

The abscissa of absolute convergence of logMul^[m] f equals that of f.

Русский

Абсцисса logMul^[m] f равна абсциссе f.

LaTeX

$$abscissaOfAbsConv (logMul^[m] f) = abscissaOfAbsConv f$$

Lean4

/-- The abscissa of absolute convergence of the point-wise product of a power of `log` and `f`
is the same as that of `f`. -/
@[simp]
theorem absicssaOfAbsConv_logPowMul {f : ℕ → ℂ} {m : ℕ} : abscissaOfAbsConv (logMul^[m] f) = abscissaOfAbsConv f := by
  induction m with
  | zero => simp
  | succ n ih => simp [ih, Function.iterate_succ', Function.comp_def, -Function.comp_apply, -Function.iterate_succ]

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