isRestricted_iff — Mathlib

English

IsRestricted c f is equivalent to the ε-N characterization: ∀ ε > 0, ∃ N such that ∀ n ≥ N, ∥coeff_n f∥ · c^n < ε.

Русский

IsRestricted c f эквивалентно ε–N характеристике: ∀ ε>0 существует N, такой что для всех n ≥ N выполняется ∥coeff_n f∥ · c^n < ε.

LaTeX

$$$\mathrm{IsRestricted}(c,f) \iff \forall \varepsilon > 0, \exists N, \forall n \ge N, \lVert \mathrm{coeff}_n f \rVert \cdot c^n < \varepsilon$$$

Lean4

theorem isRestricted_iff {f : PowerSeries R} :
    IsRestricted c f ↔ ∀ ε, 0 < ε → ∃ N, ∀ n, N ≤ n → ‖‖(coeff n) f‖ * c ^ n‖ < ε := by
  simp [IsRestricted, NormedAddCommGroup.tendsto_atTop]

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