English
If a finite power series on a ball is identically zero on its radius boundary, then the function vanishes on the ball.
Русский
Если конечный степенной ряд на шаре ограничен нулём на границе радиуса, то функция обнуляется внутри шарa.
LaTeX
$$$\forall y\in EMetric.ball x r, f y = 0$ under appropriate hypotheses (bounded by zero).$$
Lean4
theorem bound_zero_of_eq_zero (hf : ∀ y ∈ EMetric.ball x r, f y = 0) (r_pos : 0 < r) (hp : ∀ n, p n = 0) :
HasFiniteFPowerSeriesOnBall f p x 0 r :=
by
refine ⟨⟨?_, r_pos, ?_⟩, fun n _ ↦ hp n⟩
· rw [p.radius_eq_top_of_forall_image_add_eq_zero 0 (fun n ↦ by rw [add_zero]; exact hp n)]
exact le_top
· intro y hy
rw [hf (x + y)]
· convert hasSum_zero
rw [hp, ContinuousMultilinearMap.zero_apply]
·
rwa [EMetric.mem_ball, edist_eq_enorm_sub, add_comm, add_sub_cancel_right, ← edist_zero_eq_enorm, ←
EMetric.mem_ball]
