eventually_zero_of_bound_zero — Mathlib

English

If a function has a finite power series on a ball, then on that ball it matches its partial sums up to any order m ≥ n.

Русский

Если функция имеет конечный степенной ряд на шаре, то на этом шаре она совпадает с частичными суммами ряда до любой степени m ≥ n.

LaTeX

$$HasFiniteFPowerSeriesOnBall f p x n r → ∀ y ∈ EMetric.ball x r, ∀ m, n ≤ m → f (x + y) = p.partialSum m y$$

Lean4

/-- If `f` has a formal power series at `x` bounded by `0`, then `f` is equal to `0` in a
neighborhood of `x`. -/
theorem eventually_zero_of_bound_zero (hf : HasFiniteFPowerSeriesAt f pf x 0) : f =ᶠ[𝓝 x] 0 :=
  Filter.eventuallyEq_iff_exists_mem.mpr
    (let ⟨r, hf⟩ := hf;
    ⟨EMetric.ball x r, EMetric.ball_mem_nhds x hf.r_pos, fun y hy ↦ hf.eq_zero_of_bound_zero y hy⟩)

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