# Theory HOL-Real_Asymp.Multiseries_Expansion

section ‹Multiseries expansions›
theory Multiseries_Expansion
imports
"HOL-Library.BNF_Corec"
"HOL-Library.Landau_Symbols"
Lazy_Eval
Inst_Existentials
Eventuallize
begin
lemma real_powr_at_top:
assumes "(p::real) > 0"
shows "filterlim (λx. x powr p) at_top at_top"
proof (subst filterlim_cong[OF refl refl])
show "LIM x at_top. exp (p * ln x) :> at_top"
by (rule filterlim_compose[OF exp_at_top filterlim_tendsto_pos_mult_at_top[OF tendsto_const]])
(simp_all add: ln_at_top assms)
show "eventually (λx. x powr p = exp (p * ln x)) at_top"
using eventually_gt_at_top[of 0] by eventually_elim (simp add: powr_def)
qed
subsection ‹Streams and lazy lists›