stationaryPoint — Mathlib

English

For a PadicSeq f, stationaryPoint hf is a natural number where the norm stabilizes for nonzero f.

Русский

Для PadicSeq f точка stationaryPoint hf есть натуральное число, после которого норма стабилизируется.

LaTeX

$$\\mathrm{stationaryPoint}(f) \\in \\mathbb{N}$$

Lean4

/-- For all `n ≥ stationaryPoint f hf`, the `p`-adic norm of `f n` is the same. -/
def stationaryPoint {f : PadicSeq p} (hf : ¬f ≈ 0) : ℕ :=
  Classical.choose <| stationary hf

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