equal
deleted
inserted
replaced
182 |
182 |
183 lemma convergent_powser'_exp: |
183 lemma convergent_powser'_exp: |
184 "convergent_powser' (msllist_of_msstream exp_series_stream) exp" |
184 "convergent_powser' (msllist_of_msstream exp_series_stream) exp" |
185 proof - |
185 proof - |
186 have "(\<lambda>n. lcoeff (msllist_of_msstream exp_series_stream) n * x ^ n) sums exp x" for x :: real |
186 have "(\<lambda>n. lcoeff (msllist_of_msstream exp_series_stream) n * x ^ n) sums exp x" for x :: real |
187 using exp_converges[of x] by (simp add: mssnth_exp_series_stream divide_simps) |
187 using exp_converges[of x] by (simp add: mssnth_exp_series_stream field_split_simps) |
188 thus ?thesis by (auto intro: exI[of _ "1::real"] simp: convergent_powser'_def) |
188 thus ?thesis by (auto intro: exI[of _ "1::real"] simp: convergent_powser'_def) |
189 qed |
189 qed |
190 |
190 |
191 |
191 |
192 subsubsection \<open>Logarithm series\<close> |
192 subsubsection \<open>Logarithm series\<close> |
615 have B: "summable (\<lambda>n. arctan_coeffs n * x ^ n)" if "norm x < 1" for x :: real |
615 have B: "summable (\<lambda>n. arctan_coeffs n * x ^ n)" if "norm x < 1" for x :: real |
616 proof (rule summable_comparison_test) |
616 proof (rule summable_comparison_test) |
617 show "\<exists>N. \<forall>n\<ge>N. norm (arctan_coeffs n * x ^ n) \<le> 1 * norm x ^ n" |
617 show "\<exists>N. \<forall>n\<ge>N. norm (arctan_coeffs n * x ^ n) \<le> 1 * norm x ^ n" |
618 unfolding norm_mult norm_power |
618 unfolding norm_mult norm_power |
619 by (intro exI[of _ "0::nat"] allI impI mult_right_mono) |
619 by (intro exI[of _ "0::nat"] allI impI mult_right_mono) |
620 (simp_all add: arctan_coeffs_def divide_simps) |
620 (simp_all add: arctan_coeffs_def field_split_simps) |
621 from that show "summable (\<lambda>n. 1 * norm x ^ n)" |
621 from that show "summable (\<lambda>n. 1 * norm x ^ n)" |
622 by (intro summable_mult summable_geometric) simp_all |
622 by (intro summable_mult summable_geometric) simp_all |
623 qed |
623 qed |
624 |
624 |
625 define F :: "real \<Rightarrow> real" where "F = (\<lambda>x. \<Sum>n. arctan_coeffs n * x ^ n)" |
625 define F :: "real \<Rightarrow> real" where "F = (\<lambda>x. \<Sum>n. arctan_coeffs n * x ^ n)" |
3332 qed |
3332 qed |
3333 |
3333 |
3334 lemma expands_to_div': |
3334 lemma expands_to_div': |
3335 assumes "basis_wf basis" "(f expands_to F) basis" "((\<lambda>x. inverse (g x)) expands_to G) basis" |
3335 assumes "basis_wf basis" "(f expands_to F) basis" "((\<lambda>x. inverse (g x)) expands_to G) basis" |
3336 shows "((\<lambda>x. f x / g x) expands_to F * G) basis" |
3336 shows "((\<lambda>x. f x / g x) expands_to F * G) basis" |
3337 using expands_to_mult[OF assms] by (simp add: divide_simps) |
3337 using expands_to_mult[OF assms] by (simp add: field_split_simps) |
3338 |
3338 |
3339 lemma expands_to_basic: |
3339 lemma expands_to_basic: |
3340 assumes "basis_wf (b # basis)" "length basis = expansion_level TYPE('a::multiseries)" |
3340 assumes "basis_wf (b # basis)" "length basis = expansion_level TYPE('a::multiseries)" |
3341 shows "(b expands_to MS (MSLCons (const_expansion 1 :: 'a, 1) MSLNil) b) (b # basis)" |
3341 shows "(b expands_to MS (MSLCons (const_expansion 1 :: 'a, 1) MSLNil) b) (b # basis)" |
3342 proof - |
3342 proof - |
4268 using expands_to_exp_0_pull_out2[OF assms(1-2)] |
4268 using expands_to_exp_0_pull_out2[OF assms(1-2)] |
4269 proof (rule expands_to_cong') |
4269 proof (rule expands_to_cong') |
4270 from assms(2) have "eventually (\<lambda>x. b x > 0) at_top" |
4270 from assms(2) have "eventually (\<lambda>x. b x > 0) at_top" |
4271 by (simp add: filterlim_at_top_dense basis_wf_Cons) |
4271 by (simp add: filterlim_at_top_dense basis_wf_Cons) |
4272 with assms(3) show "eventually (\<lambda>x. b x powr c * g x = g x / b x ^ n) at_top" |
4272 with assms(3) show "eventually (\<lambda>x. b x powr c * g x = g x / b x ^ n) at_top" |
4273 by (auto elim!: eventually_mono simp: powr_realpow powr_minus divide_simps) |
4273 by (auto elim!: eventually_mono simp: powr_realpow powr_minus field_split_simps) |
4274 qed |
4274 qed |
4275 |
4275 |
4276 lemma eval_monom_collapse: "c * eval_monom (c', es) basis x = eval_monom (c * c', es) basis x" |
4276 lemma eval_monom_collapse: "c * eval_monom (c', es) basis x = eval_monom (c * c', es) basis x" |
4277 by (simp add: eval_monom_def) |
4277 by (simp add: eval_monom_def) |
4278 |
4278 |
4490 proof - |
4490 proof - |
4491 from assms have [simp]: "c' \<noteq> 0" |
4491 from assms have [simp]: "c' \<noteq> 0" |
4492 by (auto simp: compare_expansions_def trimmed_imp_dominant_term_nz split: cmp_result.splits) |
4492 by (auto simp: compare_expansions_def trimmed_imp_dominant_term_nz split: cmp_result.splits) |
4493 have "(\<lambda>x. inverse c * (c' * f x)) \<sim>[at_top] (\<lambda>x. inverse c * (c * g x))" |
4493 have "(\<lambda>x. inverse c * (c' * f x)) \<sim>[at_top] (\<lambda>x. inverse c * (c * g x))" |
4494 by (rule asymp_equiv_mult[OF asymp_equiv_refl]) (rule compare_expansions_EQ[OF assms(1-6)]) |
4494 by (rule asymp_equiv_mult[OF asymp_equiv_refl]) (rule compare_expansions_EQ[OF assms(1-6)]) |
4495 with assms(7) show ?thesis by (simp add: divide_simps) |
4495 with assms(7) show ?thesis by (simp add: field_split_simps) |
4496 qed |
4496 qed |
4497 |
4497 |
4498 lemma compare_expansions_EQ_imp_bigtheta: |
4498 lemma compare_expansions_EQ_imp_bigtheta: |
4499 assumes "compare_expansions F G = (EQ, c, c')" "trimmed F" "trimmed G" |
4499 assumes "compare_expansions F G = (EQ, c, c')" "trimmed F" "trimmed G" |
4500 "(f expands_to F) basis" "(g expands_to G) basis" "basis_wf basis" |
4500 "(f expands_to F) basis" "(g expands_to G) basis" "basis_wf basis" |
4571 also from assms(2,4,7) have *: "(\<lambda>x. c' * eval C x) \<sim>[at_top] (\<lambda>x. c * g x)" |
4571 also from assms(2,4,7) have *: "(\<lambda>x. c' * eval C x) \<sim>[at_top] (\<lambda>x. c * g x)" |
4572 by (intro compare_expansions_EQ[OF assms(1) _ assms(3) _ assms(5)]) |
4572 by (intro compare_expansions_EQ[OF assms(1) _ assms(3) _ assms(5)]) |
4573 (auto intro: expands_to_hd'' simp: trimmed_ms_aux_MSLCons basis_wf_Cons) |
4573 (auto intro: expands_to_hd'' simp: trimmed_ms_aux_MSLCons basis_wf_Cons) |
4574 have "(\<lambda>x. inverse c' * (c' * eval C x)) \<sim>[at_top] (\<lambda>x. inverse c' * (c * g x))" |
4574 have "(\<lambda>x. inverse c' * (c' * eval C x)) \<sim>[at_top] (\<lambda>x. inverse c' * (c * g x))" |
4575 by (rule asymp_equiv_mult) (insert *, simp_all) |
4575 by (rule asymp_equiv_mult) (insert *, simp_all) |
4576 hence "eval C \<sim>[at_top] (\<lambda>x. c / c' * g x)" by (simp add: divide_simps) |
4576 hence "eval C \<sim>[at_top] (\<lambda>x. c / c' * g x)" by (simp add: field_split_simps) |
4577 finally show ?thesis . |
4577 finally show ?thesis . |
4578 qed |
4578 qed |
4579 |
4579 |
4580 lemma expands_to_insert_ln: |
4580 lemma expands_to_insert_ln: |
4581 assumes "basis_wf [b]" |
4581 assumes "basis_wf [b]" |