cpolynomialAt_changeOrigin_of_finite

English

If hn holds, then p.changeOrigin x k = 0 for all k with n ≤ k.

Русский

Если выполняется hn, тогда p.changeOrigin x k = 0 для всех k удовлетворяющих n ≤ k.

LaTeX

$$∀ {k}, n ≤ k → p.changeOrigin x k = 0$$

Lean4

/-- The terms of the formal multilinear series `p.changeOrigin` are continuously polynomial
as we vary the origin -/
theorem cpolynomialAt_changeOrigin_of_finite (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}
    (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (k : ℕ) : CPolynomialAt 𝕜 (p.changeOrigin · k) 0 :=
  (p.hasFiniteFPowerSeriesOnBall_changeOrigin k fun _ h ↦ hn _ (le_self_add.trans h)).cpolynomialAt

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