English
If hp and hq are HasFPowerSeriesAt for f and g at x and f and g coincide eventually near x, then p = q.
Русский
Если hp и hq — представления FM для f и g в точке x и f совпадает с g на некотором окне вокруг x, тогда p = q.
LaTeX
$$$\\text{HasFPowerSeriesAt}\\, f\\, p\\, x \\rightarrow \\text{HasFPowerSeriesAt}\\, g\\, q\\, x \\rightarrow f = g \\text{ eventually near } x \\Rightarrow p=q.$$$
Lean4
/-- If a function `f : 𝕜 → E` has power series representation `p` on a ball of some radius and for
each positive radius it has some power series representation, then `p` converges to `f` on the whole
`𝕜`. -/
theorem r_eq_top_of_exists {f : 𝕜 → E} {r : ℝ≥0∞} {x : 𝕜} {p : FormalMultilinearSeries 𝕜 𝕜 E}
(h : HasFPowerSeriesOnBall f p x r)
(h' : ∀ (r' : ℝ≥0) (_ : 0 < r'), ∃ p' : FormalMultilinearSeries 𝕜 𝕜 E, HasFPowerSeriesOnBall f p' x r') :
HasFPowerSeriesOnBall f p x ∞ :=
{ r_le :=
ENNReal.le_of_forall_pos_nnreal_lt fun r hr _ =>
let ⟨_, hp'⟩ := h' r hr
(h.exchange_radius hp').r_le
r_pos := ENNReal.coe_lt_top
hasSum := fun {y} _ =>
let ⟨r', hr'⟩ := exists_gt ‖y‖₊
let ⟨_, hp'⟩ := h' r' hr'.ne_bot.bot_lt
(h.exchange_radius hp').hasSum <| mem_emetric_ball_zero_iff.mpr (ENNReal.coe_lt_coe.2 hr') }
