HasFiniteFPowerSeriesAt — Mathlib

English

From HasFiniteFPowerSeriesAt to HasFPowerSeriesAt, i.e., finite ball data yields a global power series on the ball.

Русский

Из HasFiniteFPowerSeriesAt следует HasFPowerSeriesAt: конечные данные окрестности дают глобальный ряд на области.

LaTeX

$$$\text{HasFiniteFPowerSeriesAt } f p x n \Rightarrow \text{HasFPowerSeriesAt } f p x$$$

Lean4

/-- Given a function `f : E → F`, a formal multilinear series `p` and `n : ℕ`, we say that
`f` has `p` as a finite power series around `x` if `f (x + y) = ∑' pₙ yⁿ` for all `y` in a
neighborhood of `0`and `pₙ = 0` for `n ≤ m`. -/
def HasFiniteFPowerSeriesAt (f : E → F) (p : FormalMultilinearSeries 𝕜 E F) (x : E) (n : ℕ) :=
  ∃ r, HasFiniteFPowerSeriesOnBall f p x n r

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