hasFPowerSeriesOnBall_changeOrigin

English

Compatibility between origin-change term and the index equivalence: the formula holds under the symmetrized index replacement.

Русский

Совместимость терма изменения начала и симметричной перестановки индексов: формула сохраняется при симметризованной подстановке индексов.

LaTeX

$$For all x,y, n, t, with s := changeOriginIndexEquiv.symm ⟨n,t⟩,$$

Lean4

theorem hasFPowerSeriesOnBall_changeOrigin (k : ℕ) (hr : 0 < p.radius) :
    HasFPowerSeriesOnBall (fun x => p.changeOrigin x k) (p.changeOriginSeries k) 0 p.radius :=
  have := p.le_changeOriginSeries_radius k
  ((p.changeOriginSeries k).hasFPowerSeriesOnBall (hr.trans_le this)).mono hr this

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