hasSum_sub — Mathlib

English

The property of having a power-series expansion within a set holds eventually as the radius parameter tends to 0+.

Русский

Свойство наличия степенного ряда внутри множества выполняется в общем случае при стремлении радиуса к 0+.

LaTeX

$$$HasFPowerSeriesWithinAt\ f\ p\ s\ x \Rightarrow \forall\mathbf{r} \text{ small}, HasFPowerSeriesWithinOnBall\ f\ p\ s\ x\ r$$$

Lean4

theorem hasSum_sub (hf : HasFPowerSeriesWithinOnBall f p s x r) {y : E} (hy : y ∈ (insert x s) ∩ 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.2
  simpa only [add_sub_cancel] using hf.hasSum (by simpa only [add_sub_cancel] using hy.1) this

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