has_fpower_series_iterate_dslope_fslope

English

If p.radius < ‖x‖₊, then ∑ ‖p_n‖ × ‖x‖^n is not summable.

Русский

Если p.radius < ‖x‖₊, то сумма не суммируема.

LaTeX

$$$p.radius < \\|x\\|_+ \\Rightarrow \\lnot \\ Summable_n ( \\|p_n\\| × \\|x\\|^n ).$$$

Lean4

theorem has_fpower_series_iterate_dslope_fslope (n : ℕ) (hp : HasFPowerSeriesAt f p z₀) :
    HasFPowerSeriesAt ((swap dslope z₀)^[n] f) (fslope^[n] p) z₀ := by
  induction n generalizing f p with
  | zero => exact hp
  | succ n ih => simpa using ih (has_fpower_series_dslope_fslope hp)

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