IsRestricted — Mathlib

English

IsRestricted is defined by the condition that the sequence ∥coeff_i f∥ · c^i tends to 0 as i → ∞.

Русский

IsRestricted задаётся условием, что последовательность ∥coeff_i f∥ · c^i сходится к 0 по i.

LaTeX

$$$\mathrm{IsRestricted}(\,f\,, c) := \mathrm{Tendsto}(i \mapsto \lVert \mathrm{coeff}_i f \rVert \cdot c^i)_{i\to\infty} (\mathrm{nhds}(0))$$$

Lean4

/-- A power series over `R` is restricted of paramerter `c` if we have
`‖coeff R i f‖ * c ^ i → 0`. -/
def IsRestricted (f : PowerSeries R) :=
  Tendsto (fun (i : ℕ) ↦ (norm (coeff i f)) * c ^ i) atTop (𝓝 0)

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