eq_const_of_bound_one — Mathlib

English

If f has a finite power series on a ball bounded by zero, then f is identically zero on that ball.

Русский

Если f имеет конечный степенной ряд на шаре, ограниченном нулём, то f тождественно нули на этом шаре.

LaTeX

$$HasFiniteFPowerSeriesOnBall f p x 0 r → ∀ y ∈ EMetric.ball x r, f y = 0$$

Lean4

/-- If `f` has a formal power series on a ball bounded by `1`, then `f` is constant equal
to `f x` on the ball. -/
theorem eq_const_of_bound_one (hf : HasFiniteFPowerSeriesOnBall f pf x 1 r) : ∀ y ∈ EMetric.ball x r, f y = f x :=
  by
  intro y hy
  rw [hf.eq_partialSum' y hy 1 le_rfl,
    hf.eq_partialSum' x (by rw [EMetric.mem_ball, edist_self]; exact hf.r_pos) 1 le_rfl]
  simp only [FormalMultilinearSeries.partialSum, Finset.range_one, Finset.sum_singleton]
  congr
  apply funext
  simp only [IsEmpty.forall_iff]

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