eventually_const_of_bound_one — Mathlib

English

Variant of the partial sum equality with y variable moved to the ball.

Русский

Вариант равенства частичных сумм, где переменная y перемещена в шар.

LaTeX

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

Lean4

/-- If `f` has a formal power series at x bounded by `1`, then `f` is constant equal
to `f x` in a neighborhood of `x`. -/
theorem eventually_const_of_bound_one (hf : HasFiniteFPowerSeriesAt f pf x 1) : f =ᶠ[𝓝 x] (fun _ => f x) :=
  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_const_of_bound_one y hy⟩)

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