--- a/src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy Thu Aug 04 18:45:28 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy Thu Aug 04 19:36:31 2016 +0200
@@ -11,10 +11,10 @@
\<close>
theory Generalised_Binomial_Theorem
-imports
- Complex_Main
+imports
+ Complex_Main
Complex_Transcendental
- Summation
+ Summation_Tests
begin
lemma gbinomial_ratio_limit:
@@ -36,14 +36,14 @@
by (simp add: setprod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
also have "?P / \<dots> = (?P / ?P) / (a - of_nat n)" by (rule divide_divide_eq_left[symmetric])
also from assms have "?P / ?P = 1" by auto
- also have "of_nat (Suc n) * (1 / (a - of_nat n)) =
+ also have "of_nat (Suc n) * (1 / (a - of_nat n)) =
inverse (inverse (of_nat (Suc n)) * (a - of_nat n))" by (simp add: field_simps)
also have "inverse (of_nat (Suc n)) * (a - of_nat n) = a / of_nat (Suc n) - of_nat n / of_nat (Suc n)"
by (simp add: field_simps del: of_nat_Suc)
finally show "?f n = (a gchoose n) / (a gchoose Suc n)" by simp
qed
- have "(\<lambda>n. norm a / (of_nat (Suc n))) \<longlonglongrightarrow> 0"
+ have "(\<lambda>n. norm a / (of_nat (Suc n))) \<longlonglongrightarrow> 0"
unfolding divide_inverse
by (intro tendsto_mult_right_zero LIMSEQ_inverse_real_of_nat)
hence "(\<lambda>n. a / of_nat (Suc n)) \<longlonglongrightarrow> 0"
@@ -84,26 +84,26 @@
with K have summable: "summable (\<lambda>n. ?f n * z ^ n)" if "norm z < K" for z using that by auto
hence summable': "summable (\<lambda>n. ?f' n * z ^ n)" if "norm z < K" for z using that
by (intro termdiff_converges[of _ K]) simp_all
-
+
define f f' where [abs_def]: "f z = (\<Sum>n. ?f n * z ^ n)" "f' z = (\<Sum>n. ?f' n * z ^ n)" for z
{
fix z :: complex assume z: "norm z < K"
from summable_mult2[OF summable'[OF z], of z]
have summable1: "summable (\<lambda>n. ?f' n * z ^ Suc n)" by (simp add: mult_ac)
- hence summable2: "summable (\<lambda>n. of_nat n * ?f n * z^n)"
+ hence summable2: "summable (\<lambda>n. of_nat n * ?f n * z^n)"
unfolding diffs_def by (subst (asm) summable_Suc_iff)
have "(1 + z) * f' z = (\<Sum>n. ?f' n * z^n) + (\<Sum>n. ?f' n * z^Suc n)"
unfolding f_f'_def using summable' z by (simp add: algebra_simps suminf_mult)
also have "(\<Sum>n. ?f' n * z^n) = (\<Sum>n. of_nat (Suc n) * ?f (Suc n) * z^n)"
by (intro suminf_cong) (simp add: diffs_def)
- also have "(\<Sum>n. ?f' n * z^Suc n) = (\<Sum>n. of_nat n * ?f n * z ^ n)"
+ also have "(\<Sum>n. ?f' n * z^Suc n) = (\<Sum>n. of_nat n * ?f n * z ^ n)"
using summable1 suminf_split_initial_segment[OF summable1] unfolding diffs_def
by (subst suminf_split_head, subst (asm) summable_Suc_iff) simp_all
also have "(\<Sum>n. of_nat (Suc n) * ?f (Suc n) * z^n) + (\<Sum>n. of_nat n * ?f n * z^n) =
(\<Sum>n. a * ?f n * z^n)"
by (subst gbinomial_mult_1, subst suminf_add)
- (insert summable'[OF z] summable2,
+ (insert summable'[OF z] summable2,
simp_all add: summable_powser_split_head algebra_simps diffs_def)
also have "\<dots> = a * f z" unfolding f_f'_def
by (subst suminf_mult[symmetric]) (simp_all add: summable[OF z] mult_ac)
@@ -124,16 +124,16 @@
with K have nz: "1 + z \<noteq> 0" by (auto dest!: minus_unique)
from z K have "norm z < 1" by simp
hence "(1 + z) \<notin> \<real>\<^sub>\<le>\<^sub>0" by (cases z) (auto simp: complex_nonpos_Reals_iff)
- hence "((\<lambda>z. f z * (1 + z) powr (-a)) has_field_derivative
+ hence "((\<lambda>z. f z * (1 + z) powr (-a)) has_field_derivative
f' z * (1 + z) powr (-a) - a * f z * (1 + z) powr (-a-1)) (at z)" using z
by (auto intro!: derivative_eq_intros)
also from z have "a * f z = (1 + z) * f' z" by (rule deriv)
- finally show "((\<lambda>z. f z * (1 + z) powr (-a)) has_field_derivative 0) (at z within ball 0 K)"
+ finally show "((\<lambda>z. f z * (1 + z) powr (-a)) has_field_derivative 0) (at z within ball 0 K)"
using nz by (simp add: field_simps powr_diff_complex at_within_open[OF z'])
qed simp_all
then obtain c where c: "\<And>z. z \<in> ball 0 K \<Longrightarrow> f z * (1 + z) powr (-a) = c" by blast
from c[of 0] and K have "c = 1" by simp
- with c[of z] have "f z = (1 + z) powr a" using K
+ with c[of z] have "f z = (1 + z) powr a" using K
by (simp add: powr_minus_complex field_simps dist_complex_def)
with summable K show ?thesis unfolding f_f'_def by (simp add: sums_iff)
qed
@@ -141,7 +141,7 @@
lemma gen_binomial_complex':
fixes x y :: real and a :: complex
assumes "\<bar>x\<bar> < \<bar>y\<bar>"
- shows "(\<lambda>n. (a gchoose n) * of_real x^n * of_real y powr (a - of_nat n)) sums
+ shows "(\<lambda>n. (a gchoose n) * of_real x^n * of_real y powr (a - of_nat n)) sums
of_real (x + y) powr a" (is "?P x y")
proof -
{
@@ -150,7 +150,7 @@
note xy = xy this
from xy have "(\<lambda>n. (a gchoose n) * of_real (x / y) ^ n) sums (1 + of_real (x / y)) powr a"
by (intro gen_binomial_complex) (simp add: norm_divide)
- hence "(\<lambda>n. (a gchoose n) * of_real (x / y) ^ n * y powr a) sums
+ hence "(\<lambda>n. (a gchoose n) * of_real (x / y) ^ n * y powr a) sums
((1 + of_real (x / y)) powr a * y powr a)"
by (rule sums_mult2)
also have "(1 + complex_of_real (x / y)) = complex_of_real (1 + x/y)" by simp
@@ -172,7 +172,7 @@
by (subst powr_neg_real_complex) (simp add: abs_real_def split: if_split_asm)
also {
fix n :: nat
- from y have "(a gchoose n) * of_real (-x) ^ n * of_real (-y) powr (a - of_nat n) =
+ from y have "(a gchoose n) * of_real (-x) ^ n * of_real (-y) powr (a - of_nat n) =
(a gchoose n) * (-of_real x / -of_real y) ^ n * (- of_real y) powr a"
by (subst power_divide) (simp add: powr_diff_complex powr_nat)
also from y have "(- of_real y) powr a = (-1) powr -a * of_real y powr a"
@@ -180,7 +180,7 @@
also have "-complex_of_real x / -complex_of_real y = complex_of_real x / complex_of_real y"
by simp
also have "... ^ n = of_real x ^ n / of_real y ^ n" by (simp add: power_divide)
- also have "(a gchoose n) * ... * ((-1) powr -a * of_real y powr a) =
+ also have "(a gchoose n) * ... * ((-1) powr -a * of_real y powr a) =
(-1) powr -a * ((a gchoose n) * of_real x ^ n * of_real y powr (a - n))"
by (simp add: algebra_simps powr_diff_complex powr_nat)
finally have "(a gchoose n) * of_real (- x) ^ n * of_real (- y) powr (a - of_nat n) =
@@ -194,7 +194,7 @@
lemma gen_binomial_complex'':
fixes x y :: real and a :: complex
assumes "\<bar>y\<bar> < \<bar>x\<bar>"
- shows "(\<lambda>n. (a gchoose n) * of_real x powr (a - of_nat n) * of_real y ^ n) sums
+ shows "(\<lambda>n. (a gchoose n) * of_real x powr (a - of_nat n) * of_real y ^ n) sums
of_real (x + y) powr a"
using gen_binomial_complex'[OF assms] by (simp add: mult_ac add.commute)
@@ -209,12 +209,12 @@
(of_real (1 + z)) powr (of_real a)" by simp
also have "(of_real (1 + z) :: complex) powr (of_real a) = of_real ((1 + z) powr a)"
using assms by (subst powr_of_real) simp_all
- also have "(of_real a gchoose n :: complex) = of_real (a gchoose n)" for n
+ also have "(of_real a gchoose n :: complex) = of_real (a gchoose n)" for n
by (simp add: gbinomial_setprod_rev)
hence "(\<lambda>n. (of_real a gchoose n :: complex) * of_real z ^ n) =
(\<lambda>n. of_real ((a gchoose n) * z ^ n))" by (intro ext) simp
finally show ?thesis by (simp only: sums_of_real_iff)
-qed
+qed
lemma gen_binomial_real':
fixes x y a :: real
@@ -228,7 +228,7 @@
by (rule gen_binomial_real)
hence "(\<lambda>n. (a gchoose n) * (x / y) ^ n * y powr a) sums ((1 + x / y) powr a * y powr a)"
by (rule sums_mult2)
- with xy show ?thesis
+ with xy show ?thesis
by (simp add: field_simps powr_divide powr_divide2[symmetric] powr_realpow)
qed
@@ -245,7 +245,7 @@
using gen_binomial_real'[OF assms] by (simp add: mult_ac add.commute)
lemma sqrt_series':
- "\<bar>z\<bar> < a \<Longrightarrow> (\<lambda>n. ((1/2) gchoose n) * a powr (1/2 - real_of_nat n) * z ^ n) sums
+ "\<bar>z\<bar> < a \<Longrightarrow> (\<lambda>n. ((1/2) gchoose n) * a powr (1/2 - real_of_nat n) * z ^ n) sums
sqrt (a + z :: real)"
using gen_binomial_real''[of z a "1/2"] by (simp add: powr_half_sqrt)