radius_le_radius_continuousLinearMap_comp

English

There is a summability result with nnnorm: ∑ ‖p_n‖₊ r^n converges when r below radius.

Русский

Суммируемость через nnnorm: при r радиуса меньше ∑ ‖p_n‖₊ r^n сходится.

LaTeX

$$$\\text{Summable } \\sum_n \\|p_n\\|_+ r^n \\text{ for } r

Lean4

theorem radius_le_radius_continuousLinearMap_comp (p : FormalMultilinearSeries 𝕜 E F) (f : F →L[𝕜] G) :
    p.radius ≤ (f.compFormalMultilinearSeries p).radius :=
  by
  refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_
  apply le_radius_of_isBigO
  apply (IsBigO.trans_isLittleO _ (p.isLittleO_one_of_lt_radius hr)).isBigO
  refine IsBigO.mul (@IsBigOWith.isBigO _ _ _ _ _ ‖f‖ _ _ _ ?_) (isBigO_refl _ _)
  refine IsBigOWith.of_bound (Eventually.of_forall fun n => ?_)
  simpa only [norm_norm] using f.norm_compContinuousMultilinearMap_le (p n)

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