hasSum_sub — Mathlib

English

If f has a power series within on ball, and g agrees with f on insert x s ∩ EMetric.ball x r, then g has the same power series on ball.

Русский

Если у f есть степенной ряд внутри шара, и g совпадает с f на вставке x s ∩ EMetric.ball x r, то g имеет тот же ряд в шаре.

LaTeX

$$$HasFPowerSeriesWithinOnBall\ f\ p\ s\ x\ r \land EqOn g f (insert x s \cap EMetric.ball x r) \Rightarrow HasFPowerSeriesWithinOnBall\ g\ p\ s\ x\ r$$$

Lean4

theorem hasSum_sub (hf : HasFPowerSeriesOnBall f p x r) {y : E} (hy : y ∈ EMetric.ball x r) :
    HasSum (fun n : ℕ => p n fun _ => y - x) (f y) :=
  by
  have : y - x ∈ EMetric.ball 0 r := by simpa [edist_eq_enorm_sub] using hy
  simpa only [add_sub_cancel] using hf.hasSum this

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