eq_partialSum — Mathlib

English

Let h be an eventual equality of f and g near x; then CPolynomialAt 𝕜 f x holds iff CPolynomialAt 𝕜 g x holds.

Русский

Пусть f и g совпадают не хуже чем в окрестности x; тогда CPolynomialAt 𝕜 f x выполняется тогда, когда выполняется CPolynomialAt 𝕜 g x.

LaTeX

$$(f =^\infty_{𝓝 x} g) → (CPolynomialAt 𝕜 f x ↔ CPolynomialAt 𝕜 g x)$$

Lean4

/-- If a function admits a finite power series expansion bounded by `n`, then it is equal to
the `m`th partial sums of this power series at every point of the disk for `n ≤ m`. -/
theorem eq_partialSum (hf : HasFiniteFPowerSeriesOnBall f p x n r) :
    ∀ y ∈ EMetric.ball (0 : E) r, ∀ m, n ≤ m → f (x + y) = p.partialSum m y := fun y hy m hm ↦
  (hf.hasSum hy).unique
    (hasSum_sum_of_ne_finset_zero (f := fun m => p m (fun _ => y)) (s := Finset.range m)
      (fun N hN => by
        simp only; simp only [Finset.mem_range, not_lt] at hN
        rw [hf.finite _ (le_trans hm hN), ContinuousMultilinearMap.zero_apply]))

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