|
68630
|
1 |
theory Real_Asymp
|
|
|
2 |
imports Multiseries_Expansion_Bounds
|
|
|
3 |
keywords
|
|
|
4 |
"real_limit" "real_expansion" :: diag
|
|
|
5 |
begin
|
|
|
6 |
|
|
|
7 |
ML_file \<open>real_asymp_diag.ML\<close>
|
|
|
8 |
|
|
|
9 |
(*<*)
|
|
|
10 |
(* Hide constants and lemmas to avoid polluting global namespace *)
|
|
|
11 |
hide_const (open)
|
|
|
12 |
gbinomial_series lcoeff mssnth MSSCons MSLNil MSLCons mslmap convergent_powser convergent_powser'
|
|
|
13 |
powser mssalternate basis_wf eval_monom inverse_monom is_expansion expansion_level eval
|
|
|
14 |
zero_expansion const_expansion powr_expansion power_expansion trimmed dominant_term trimmed_pos
|
|
|
15 |
trimmed_neg ms_aux_hd_exp ms_exp_gt modify_eval is_lifting expands_to asymp_powser flip_cmp_result
|
|
|
16 |
compare_lists compare_expansions compare_list_0 powr_nat rfloor rceil rnatmod
|
|
|
17 |
|
|
|
18 |
hide_fact (open)
|
|
|
19 |
convergent_powser_stl isCont_powser powser_MSLNil powser_MSLCons
|
|
|
20 |
convergent_powser'_imp_convergent_powser convergent_powser'_eventually
|
|
|
21 |
convergent_powser'_geometric convergent_powser'_exp convergent_powser'_ln gbinomial_series_abort
|
|
|
22 |
convergent_powser'_gbinomial convergent_powser'_gbinomial' convergent_powser_sin_series_stream
|
|
|
23 |
convergent_powser_cos_series_stream convergent_powser_arctan basis_wf_Nil basis_wf_Cons
|
|
|
24 |
basis_wf_snoc basis_wf_singleton basis_wf_many eval_monom_Nil1 eval_monom_Nil2 eval_monom_Cons
|
|
|
25 |
length_snd_inverse_monom eval_monom_pos eval_monom_uminus eval_monom_neg eval_monom_nonzero
|
|
|
26 |
eval_real eval_inverse_monom eval_monom_smallo' eval_monom_smallomega' eval_monom_smallo
|
|
|
27 |
eval_monom_smallomega hd_exp_powser hd_exp_inverse eval_pos_if_dominant_term_pos
|
|
|
28 |
eval_pos_if_dominant_term_pos' eval_neg_if_dominant_term_neg' eval_modify_eval trimmed_pos_real_iff
|
|
|
29 |
trimmed_pos_ms_iff not_trimmed_pos_MSLNil trimmed_pos_MSLCons is_liftingD is_lifting_lift hd_exp_map
|
|
|
30 |
is_expansion_map is_expansion_map_aux is_expansion_map_final trimmed_map_ms is_lifting_map
|
|
|
31 |
is_lifting_id is_lifting_trans is_expansion_X dominant_term_expands_to trimmed_lifting
|
|
|
32 |
trimmed_pos_lifting hd_exp_powser' compare_lists.simps compare_lists_Nil compare_lists_Cons
|
|
|
33 |
flip_compare_lists compare_lists_induct eval_monom_smallo_eval_monom eval_monom_eq
|
|
|
34 |
compare_expansions_real compare_expansions_MSLCons_eval compare_expansions_LT_I
|
|
|
35 |
compare_expansions_GT_I compare_expansions_same_exp compare_expansions_GT_flip compare_expansions_LT
|
|
|
36 |
compare_expansions_GT compare_expansions_EQ compare_expansions_EQ_imp_bigo
|
|
|
37 |
compare_expansions_EQ_same compare_expansions_EQ_imp_bigtheta compare_expansions_LT'
|
|
|
38 |
compare_expansions_GT' compare_expansions_EQ' compare_list_0.simps compare_reals_diff_sgnD
|
|
|
39 |
trimmed_realI trimmed_pos_realI trimmed_neg_realI trimmed_pos_hd_coeff lift_trimmed lift_trimmed_pos
|
|
|
40 |
lift_trimmed_neg lift_trimmed_pos' lift_trimmed_neg' trimmed_eq_cong trimmed_pos_eq_cong
|
|
|
41 |
trimmed_neg_eq_cong trimmed_hd trim_lift_eq basis_wf_manyI trimmed_pos_uminus
|
|
|
42 |
trimmed_pos_imp_trimmed trimmed_neg_imp_trimmed intyness_0 intyness_1 intyness_numeral
|
|
|
43 |
intyness_uminus intyness_of_nat intyness_simps powr_nat_of_nat powr_nat_conv_powr reify_power
|
|
|
44 |
sqrt_conv_root tan_conv_sin_cos landau_meta_eq_cong
|
|
|
45 |
asymp_equiv_meta_eq_cong eventually_lt_imp_eventually_le eventually_conv_filtermap
|
|
|
46 |
filterlim_conv_filtermap eval_simps real_eqI lift_ms_simps nhds_leI
|
|
|
47 |
(*>*)
|
|
|
48 |
|
|
|
49 |
end |