coeff_zero — Mathlib

English

The zeroth coefficient of pf equals f(x) when HasFPowerSeriesOnBall holds.

Русский

Нулевой коэффициент pf равен f(x) при выполнении HasFPowerSeriesOnBall.

LaTeX

$$HasFPowerSeriesOnBall f pf x r → pf 0 v = f x for any v : Fin 0 → E.$$

Lean4

theorem coeff_zero (hf : HasFPowerSeriesWithinOnBall f pf s x r) (v : Fin 0 → E) : pf 0 v = f x :=
  by
  have v_eq : v = fun i => 0 := Subsingleton.elim _ _
  have zero_mem : (0 : E) ∈ EMetric.ball (0 : E) r := by simp [hf.r_pos]
  have : ∀ i, i ≠ 0 → (pf i fun _ => 0) = 0 := by
    intro i hi
    have : 0 < i := pos_iff_ne_zero.2 hi
    exact ContinuousMultilinearMap.map_coord_zero _ (⟨0, this⟩ : Fin i) rfl
  have A := (hf.hasSum (by simp) zero_mem).unique (hasSum_single _ this)
  simpa [v_eq] using A.symm

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