tendsto_trunc_atTop — Mathlib

English

If σ is nonempty, truncation on d tends to f as d grows.

Русский

Если множество σ непусто, обрезка по d сходится к f при росте d.

LaTeX

$$Tendsto (λ d, (trunc R d f : MvPowerSeries σ R)) atTop (nhds f)$$

Lean4

theorem tendsto_trunc_atTop [DecidableEq σ] [CommSemiring R] [Nonempty σ] (f : MvPowerSeries σ R) :
    Tendsto (fun d ↦ (trunc R d f : MvPowerSeries σ R)) atTop (𝓝 f) :=
  by
  rw [tendsto_iff_coeff_tendsto]
  intro d
  obtain ⟨s, _⟩ := (exists_const σ).mpr trivial
  apply tendsto_atTop_of_eventually_const (i₀ := d + Finsupp.single s 1)
  intro n hn
  rw [MvPolynomial.coeff_coe, coeff_trunc, if_pos]
  apply lt_of_lt_of_le _ hn
  simp only [lt_add_iff_pos_right, Finsupp.lt_def]
  refine ⟨zero_le _, ⟨s, by simp⟩⟩

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