hasFiniteFPowerSeriesOnBall_changeOrigin

English

For p with hn, HasFiniteFPowerSeriesOnBall (p.changeOrigin · k) (p.changeOriginSeries k) 0 n ⊤ holds; i.e., the shifted series remains finite on a ball.

Русский

Для p со свойством hn, остается конечная степенная серия после смещения для шарa: HasFiniteFPowerSeriesOnBall (p.changeOrigin · k) (p.changeOriginSeries k) 0 n ⊤.

LaTeX

$$HasFiniteFPowerSeriesOnBall (p.changeOrigin · k) (p.changeOriginSeries k) 0 n ⊤$$

Lean4

theorem hasFiniteFPowerSeriesOnBall_changeOrigin (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (k : ℕ)
    (hn : ∀ (m : ℕ), n + k ≤ m → p m = 0) :
    HasFiniteFPowerSeriesOnBall (p.changeOrigin · k) (p.changeOriginSeries k) 0 n ⊤ :=
  (p.changeOriginSeries k).hasFiniteFPowerSeriesOnBall_of_finite
    (fun _ hm => p.changeOriginSeries_finite_of_finite hn k (by rw [add_comm n k]; apply add_le_add_left hm))

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