9 We prove the generalised binomial theorem for complex numbers, following the proof at: |
9 We prove the generalised binomial theorem for complex numbers, following the proof at: |
10 \url{https://proofwiki.org/wiki/Binomial_Theorem/General_Binomial_Theorem} |
10 \url{https://proofwiki.org/wiki/Binomial_Theorem/General_Binomial_Theorem} |
11 \<close> |
11 \<close> |
12 |
12 |
13 theory Generalised_Binomial_Theorem |
13 theory Generalised_Binomial_Theorem |
14 imports |
14 imports |
15 Complex_Main |
15 Complex_Main |
16 Complex_Transcendental |
16 Complex_Transcendental |
17 Summation |
17 Summation_Tests |
18 begin |
18 begin |
19 |
19 |
20 lemma gbinomial_ratio_limit: |
20 lemma gbinomial_ratio_limit: |
21 fixes a :: "'a :: real_normed_field" |
21 fixes a :: "'a :: real_normed_field" |
22 assumes "a \<notin> \<nat>" |
22 assumes "a \<notin> \<nat>" |
34 by (simp add: gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost) |
34 by (simp add: gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost) |
35 also from q have "(\<Prod>i=0..n. a - of_nat i) = ?P * (a - of_nat n)" |
35 also from q have "(\<Prod>i=0..n. a - of_nat i) = ?P * (a - of_nat n)" |
36 by (simp add: setprod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost) |
36 by (simp add: setprod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost) |
37 also have "?P / \<dots> = (?P / ?P) / (a - of_nat n)" by (rule divide_divide_eq_left[symmetric]) |
37 also have "?P / \<dots> = (?P / ?P) / (a - of_nat n)" by (rule divide_divide_eq_left[symmetric]) |
38 also from assms have "?P / ?P = 1" by auto |
38 also from assms have "?P / ?P = 1" by auto |
39 also have "of_nat (Suc n) * (1 / (a - of_nat n)) = |
39 also have "of_nat (Suc n) * (1 / (a - of_nat n)) = |
40 inverse (inverse (of_nat (Suc n)) * (a - of_nat n))" by (simp add: field_simps) |
40 inverse (inverse (of_nat (Suc n)) * (a - of_nat n))" by (simp add: field_simps) |
41 also have "inverse (of_nat (Suc n)) * (a - of_nat n) = a / of_nat (Suc n) - of_nat n / of_nat (Suc n)" |
41 also have "inverse (of_nat (Suc n)) * (a - of_nat n) = a / of_nat (Suc n) - of_nat n / of_nat (Suc n)" |
42 by (simp add: field_simps del: of_nat_Suc) |
42 by (simp add: field_simps del: of_nat_Suc) |
43 finally show "?f n = (a gchoose n) / (a gchoose Suc n)" by simp |
43 finally show "?f n = (a gchoose n) / (a gchoose Suc n)" by simp |
44 qed |
44 qed |
45 |
45 |
46 have "(\<lambda>n. norm a / (of_nat (Suc n))) \<longlonglongrightarrow> 0" |
46 have "(\<lambda>n. norm a / (of_nat (Suc n))) \<longlonglongrightarrow> 0" |
47 unfolding divide_inverse |
47 unfolding divide_inverse |
48 by (intro tendsto_mult_right_zero LIMSEQ_inverse_real_of_nat) |
48 by (intro tendsto_mult_right_zero LIMSEQ_inverse_real_of_nat) |
49 hence "(\<lambda>n. a / of_nat (Suc n)) \<longlonglongrightarrow> 0" |
49 hence "(\<lambda>n. a / of_nat (Suc n)) \<longlonglongrightarrow> 0" |
50 by (subst tendsto_norm_zero_iff[symmetric]) (simp add: norm_divide del: of_nat_Suc) |
50 by (subst tendsto_norm_zero_iff[symmetric]) (simp add: norm_divide del: of_nat_Suc) |
51 hence "?f \<longlonglongrightarrow> inverse (0 - 1)" |
51 hence "?f \<longlonglongrightarrow> inverse (0 - 1)" |
82 have summable_strong: "summable (\<lambda>n. ?f n * z ^ n)" if "norm z < 1" for z using that |
82 have summable_strong: "summable (\<lambda>n. ?f n * z ^ n)" if "norm z < 1" for z using that |
83 by (intro summable_in_conv_radius) (simp_all add: conv_radius_gchoose) |
83 by (intro summable_in_conv_radius) (simp_all add: conv_radius_gchoose) |
84 with K have summable: "summable (\<lambda>n. ?f n * z ^ n)" if "norm z < K" for z using that by auto |
84 with K have summable: "summable (\<lambda>n. ?f n * z ^ n)" if "norm z < K" for z using that by auto |
85 hence summable': "summable (\<lambda>n. ?f' n * z ^ n)" if "norm z < K" for z using that |
85 hence summable': "summable (\<lambda>n. ?f' n * z ^ n)" if "norm z < K" for z using that |
86 by (intro termdiff_converges[of _ K]) simp_all |
86 by (intro termdiff_converges[of _ K]) simp_all |
87 |
87 |
88 define f f' where [abs_def]: "f z = (\<Sum>n. ?f n * z ^ n)" "f' z = (\<Sum>n. ?f' n * z ^ n)" for z |
88 define f f' where [abs_def]: "f z = (\<Sum>n. ?f n * z ^ n)" "f' z = (\<Sum>n. ?f' n * z ^ n)" for z |
89 { |
89 { |
90 fix z :: complex assume z: "norm z < K" |
90 fix z :: complex assume z: "norm z < K" |
91 from summable_mult2[OF summable'[OF z], of z] |
91 from summable_mult2[OF summable'[OF z], of z] |
92 have summable1: "summable (\<lambda>n. ?f' n * z ^ Suc n)" by (simp add: mult_ac) |
92 have summable1: "summable (\<lambda>n. ?f' n * z ^ Suc n)" by (simp add: mult_ac) |
93 hence summable2: "summable (\<lambda>n. of_nat n * ?f n * z^n)" |
93 hence summable2: "summable (\<lambda>n. of_nat n * ?f n * z^n)" |
94 unfolding diffs_def by (subst (asm) summable_Suc_iff) |
94 unfolding diffs_def by (subst (asm) summable_Suc_iff) |
95 |
95 |
96 have "(1 + z) * f' z = (\<Sum>n. ?f' n * z^n) + (\<Sum>n. ?f' n * z^Suc n)" |
96 have "(1 + z) * f' z = (\<Sum>n. ?f' n * z^n) + (\<Sum>n. ?f' n * z^Suc n)" |
97 unfolding f_f'_def using summable' z by (simp add: algebra_simps suminf_mult) |
97 unfolding f_f'_def using summable' z by (simp add: algebra_simps suminf_mult) |
98 also have "(\<Sum>n. ?f' n * z^n) = (\<Sum>n. of_nat (Suc n) * ?f (Suc n) * z^n)" |
98 also have "(\<Sum>n. ?f' n * z^n) = (\<Sum>n. of_nat (Suc n) * ?f (Suc n) * z^n)" |
99 by (intro suminf_cong) (simp add: diffs_def) |
99 by (intro suminf_cong) (simp add: diffs_def) |
100 also have "(\<Sum>n. ?f' n * z^Suc n) = (\<Sum>n. of_nat n * ?f n * z ^ n)" |
100 also have "(\<Sum>n. ?f' n * z^Suc n) = (\<Sum>n. of_nat n * ?f n * z ^ n)" |
101 using summable1 suminf_split_initial_segment[OF summable1] unfolding diffs_def |
101 using summable1 suminf_split_initial_segment[OF summable1] unfolding diffs_def |
102 by (subst suminf_split_head, subst (asm) summable_Suc_iff) simp_all |
102 by (subst suminf_split_head, subst (asm) summable_Suc_iff) simp_all |
103 also have "(\<Sum>n. of_nat (Suc n) * ?f (Suc n) * z^n) + (\<Sum>n. of_nat n * ?f n * z^n) = |
103 also have "(\<Sum>n. of_nat (Suc n) * ?f (Suc n) * z^n) + (\<Sum>n. of_nat n * ?f n * z^n) = |
104 (\<Sum>n. a * ?f n * z^n)" |
104 (\<Sum>n. a * ?f n * z^n)" |
105 by (subst gbinomial_mult_1, subst suminf_add) |
105 by (subst gbinomial_mult_1, subst suminf_add) |
106 (insert summable'[OF z] summable2, |
106 (insert summable'[OF z] summable2, |
107 simp_all add: summable_powser_split_head algebra_simps diffs_def) |
107 simp_all add: summable_powser_split_head algebra_simps diffs_def) |
108 also have "\<dots> = a * f z" unfolding f_f'_def |
108 also have "\<dots> = a * f z" unfolding f_f'_def |
109 by (subst suminf_mult[symmetric]) (simp_all add: summable[OF z] mult_ac) |
109 by (subst suminf_mult[symmetric]) (simp_all add: summable[OF z] mult_ac) |
110 finally have "a * f z = (1 + z) * f' z" by simp |
110 finally have "a * f z = (1 + z) * f' z" by simp |
111 } note deriv = this |
111 } note deriv = this |
122 fix z :: complex assume z': "z \<in> ball 0 K" |
122 fix z :: complex assume z': "z \<in> ball 0 K" |
123 hence z: "norm z < K" by simp |
123 hence z: "norm z < K" by simp |
124 with K have nz: "1 + z \<noteq> 0" by (auto dest!: minus_unique) |
124 with K have nz: "1 + z \<noteq> 0" by (auto dest!: minus_unique) |
125 from z K have "norm z < 1" by simp |
125 from z K have "norm z < 1" by simp |
126 hence "(1 + z) \<notin> \<real>\<^sub>\<le>\<^sub>0" by (cases z) (auto simp: complex_nonpos_Reals_iff) |
126 hence "(1 + z) \<notin> \<real>\<^sub>\<le>\<^sub>0" by (cases z) (auto simp: complex_nonpos_Reals_iff) |
127 hence "((\<lambda>z. f z * (1 + z) powr (-a)) has_field_derivative |
127 hence "((\<lambda>z. f z * (1 + z) powr (-a)) has_field_derivative |
128 f' z * (1 + z) powr (-a) - a * f z * (1 + z) powr (-a-1)) (at z)" using z |
128 f' z * (1 + z) powr (-a) - a * f z * (1 + z) powr (-a-1)) (at z)" using z |
129 by (auto intro!: derivative_eq_intros) |
129 by (auto intro!: derivative_eq_intros) |
130 also from z have "a * f z = (1 + z) * f' z" by (rule deriv) |
130 also from z have "a * f z = (1 + z) * f' z" by (rule deriv) |
131 finally show "((\<lambda>z. f z * (1 + z) powr (-a)) has_field_derivative 0) (at z within ball 0 K)" |
131 finally show "((\<lambda>z. f z * (1 + z) powr (-a)) has_field_derivative 0) (at z within ball 0 K)" |
132 using nz by (simp add: field_simps powr_diff_complex at_within_open[OF z']) |
132 using nz by (simp add: field_simps powr_diff_complex at_within_open[OF z']) |
133 qed simp_all |
133 qed simp_all |
134 then obtain c where c: "\<And>z. z \<in> ball 0 K \<Longrightarrow> f z * (1 + z) powr (-a) = c" by blast |
134 then obtain c where c: "\<And>z. z \<in> ball 0 K \<Longrightarrow> f z * (1 + z) powr (-a) = c" by blast |
135 from c[of 0] and K have "c = 1" by simp |
135 from c[of 0] and K have "c = 1" by simp |
136 with c[of z] have "f z = (1 + z) powr a" using K |
136 with c[of z] have "f z = (1 + z) powr a" using K |
137 by (simp add: powr_minus_complex field_simps dist_complex_def) |
137 by (simp add: powr_minus_complex field_simps dist_complex_def) |
138 with summable K show ?thesis unfolding f_f'_def by (simp add: sums_iff) |
138 with summable K show ?thesis unfolding f_f'_def by (simp add: sums_iff) |
139 qed |
139 qed |
140 |
140 |
141 lemma gen_binomial_complex': |
141 lemma gen_binomial_complex': |
142 fixes x y :: real and a :: complex |
142 fixes x y :: real and a :: complex |
143 assumes "\<bar>x\<bar> < \<bar>y\<bar>" |
143 assumes "\<bar>x\<bar> < \<bar>y\<bar>" |
144 shows "(\<lambda>n. (a gchoose n) * of_real x^n * of_real y powr (a - of_nat n)) sums |
144 shows "(\<lambda>n. (a gchoose n) * of_real x^n * of_real y powr (a - of_nat n)) sums |
145 of_real (x + y) powr a" (is "?P x y") |
145 of_real (x + y) powr a" (is "?P x y") |
146 proof - |
146 proof - |
147 { |
147 { |
148 fix x y :: real assume xy: "\<bar>x\<bar> < \<bar>y\<bar>" "y \<ge> 0" |
148 fix x y :: real assume xy: "\<bar>x\<bar> < \<bar>y\<bar>" "y \<ge> 0" |
149 hence "y > 0" by simp |
149 hence "y > 0" by simp |
150 note xy = xy this |
150 note xy = xy this |
151 from xy have "(\<lambda>n. (a gchoose n) * of_real (x / y) ^ n) sums (1 + of_real (x / y)) powr a" |
151 from xy have "(\<lambda>n. (a gchoose n) * of_real (x / y) ^ n) sums (1 + of_real (x / y)) powr a" |
152 by (intro gen_binomial_complex) (simp add: norm_divide) |
152 by (intro gen_binomial_complex) (simp add: norm_divide) |
153 hence "(\<lambda>n. (a gchoose n) * of_real (x / y) ^ n * y powr a) sums |
153 hence "(\<lambda>n. (a gchoose n) * of_real (x / y) ^ n * y powr a) sums |
154 ((1 + of_real (x / y)) powr a * y powr a)" |
154 ((1 + of_real (x / y)) powr a * y powr a)" |
155 by (rule sums_mult2) |
155 by (rule sums_mult2) |
156 also have "(1 + complex_of_real (x / y)) = complex_of_real (1 + x/y)" by simp |
156 also have "(1 + complex_of_real (x / y)) = complex_of_real (1 + x/y)" by simp |
157 also from xy have "\<dots> powr a * of_real y powr a = (\<dots> * y) powr a" |
157 also from xy have "\<dots> powr a * of_real y powr a = (\<dots> * y) powr a" |
158 by (subst powr_times_real[symmetric]) (simp_all add: field_simps) |
158 by (subst powr_times_real[symmetric]) (simp_all add: field_simps) |
170 also have "complex_of_real (-x + -y) = - complex_of_real (x + y)" by simp |
170 also have "complex_of_real (-x + -y) = - complex_of_real (x + y)" by simp |
171 also from xy assms have "... powr a = (-1) powr -a * of_real (x + y) powr a" |
171 also from xy assms have "... powr a = (-1) powr -a * of_real (x + y) powr a" |
172 by (subst powr_neg_real_complex) (simp add: abs_real_def split: if_split_asm) |
172 by (subst powr_neg_real_complex) (simp add: abs_real_def split: if_split_asm) |
173 also { |
173 also { |
174 fix n :: nat |
174 fix n :: nat |
175 from y have "(a gchoose n) * of_real (-x) ^ n * of_real (-y) powr (a - of_nat n) = |
175 from y have "(a gchoose n) * of_real (-x) ^ n * of_real (-y) powr (a - of_nat n) = |
176 (a gchoose n) * (-of_real x / -of_real y) ^ n * (- of_real y) powr a" |
176 (a gchoose n) * (-of_real x / -of_real y) ^ n * (- of_real y) powr a" |
177 by (subst power_divide) (simp add: powr_diff_complex powr_nat) |
177 by (subst power_divide) (simp add: powr_diff_complex powr_nat) |
178 also from y have "(- of_real y) powr a = (-1) powr -a * of_real y powr a" |
178 also from y have "(- of_real y) powr a = (-1) powr -a * of_real y powr a" |
179 by (subst powr_neg_real_complex) simp |
179 by (subst powr_neg_real_complex) simp |
180 also have "-complex_of_real x / -complex_of_real y = complex_of_real x / complex_of_real y" |
180 also have "-complex_of_real x / -complex_of_real y = complex_of_real x / complex_of_real y" |
181 by simp |
181 by simp |
182 also have "... ^ n = of_real x ^ n / of_real y ^ n" by (simp add: power_divide) |
182 also have "... ^ n = of_real x ^ n / of_real y ^ n" by (simp add: power_divide) |
183 also have "(a gchoose n) * ... * ((-1) powr -a * of_real y powr a) = |
183 also have "(a gchoose n) * ... * ((-1) powr -a * of_real y powr a) = |
184 (-1) powr -a * ((a gchoose n) * of_real x ^ n * of_real y powr (a - n))" |
184 (-1) powr -a * ((a gchoose n) * of_real x ^ n * of_real y powr (a - n))" |
185 by (simp add: algebra_simps powr_diff_complex powr_nat) |
185 by (simp add: algebra_simps powr_diff_complex powr_nat) |
186 finally have "(a gchoose n) * of_real (- x) ^ n * of_real (- y) powr (a - of_nat n) = |
186 finally have "(a gchoose n) * of_real (- x) ^ n * of_real (- y) powr (a - of_nat n) = |
187 (-1) powr -a * ((a gchoose n) * of_real x ^ n * of_real y powr (a - of_nat n))" . |
187 (-1) powr -a * ((a gchoose n) * of_real x ^ n * of_real y powr (a - of_nat n))" . |
188 } |
188 } |
192 qed |
192 qed |
193 |
193 |
194 lemma gen_binomial_complex'': |
194 lemma gen_binomial_complex'': |
195 fixes x y :: real and a :: complex |
195 fixes x y :: real and a :: complex |
196 assumes "\<bar>y\<bar> < \<bar>x\<bar>" |
196 assumes "\<bar>y\<bar> < \<bar>x\<bar>" |
197 shows "(\<lambda>n. (a gchoose n) * of_real x powr (a - of_nat n) * of_real y ^ n) sums |
197 shows "(\<lambda>n. (a gchoose n) * of_real x powr (a - of_nat n) * of_real y ^ n) sums |
198 of_real (x + y) powr a" |
198 of_real (x + y) powr a" |
199 using gen_binomial_complex'[OF assms] by (simp add: mult_ac add.commute) |
199 using gen_binomial_complex'[OF assms] by (simp add: mult_ac add.commute) |
200 |
200 |
201 lemma gen_binomial_real: |
201 lemma gen_binomial_real: |
202 fixes z :: real |
202 fixes z :: real |
207 from gen_binomial_complex[OF this] |
207 from gen_binomial_complex[OF this] |
208 have "(\<lambda>n. (of_real a gchoose n :: complex) * of_real z ^ n) sums |
208 have "(\<lambda>n. (of_real a gchoose n :: complex) * of_real z ^ n) sums |
209 (of_real (1 + z)) powr (of_real a)" by simp |
209 (of_real (1 + z)) powr (of_real a)" by simp |
210 also have "(of_real (1 + z) :: complex) powr (of_real a) = of_real ((1 + z) powr a)" |
210 also have "(of_real (1 + z) :: complex) powr (of_real a) = of_real ((1 + z) powr a)" |
211 using assms by (subst powr_of_real) simp_all |
211 using assms by (subst powr_of_real) simp_all |
212 also have "(of_real a gchoose n :: complex) = of_real (a gchoose n)" for n |
212 also have "(of_real a gchoose n :: complex) = of_real (a gchoose n)" for n |
213 by (simp add: gbinomial_setprod_rev) |
213 by (simp add: gbinomial_setprod_rev) |
214 hence "(\<lambda>n. (of_real a gchoose n :: complex) * of_real z ^ n) = |
214 hence "(\<lambda>n. (of_real a gchoose n :: complex) * of_real z ^ n) = |
215 (\<lambda>n. of_real ((a gchoose n) * z ^ n))" by (intro ext) simp |
215 (\<lambda>n. of_real ((a gchoose n) * z ^ n))" by (intro ext) simp |
216 finally show ?thesis by (simp only: sums_of_real_iff) |
216 finally show ?thesis by (simp only: sums_of_real_iff) |
217 qed |
217 qed |
218 |
218 |
219 lemma gen_binomial_real': |
219 lemma gen_binomial_real': |
220 fixes x y a :: real |
220 fixes x y a :: real |
221 assumes "\<bar>x\<bar> < y" |
221 assumes "\<bar>x\<bar> < y" |
222 shows "(\<lambda>n. (a gchoose n) * x^n * y powr (a - of_nat n)) sums (x + y) powr a" |
222 shows "(\<lambda>n. (a gchoose n) * x^n * y powr (a - of_nat n)) sums (x + y) powr a" |
243 assumes "\<bar>y\<bar> < x" |
243 assumes "\<bar>y\<bar> < x" |
244 shows "(\<lambda>n. (a gchoose n) * x powr (a - of_nat n) * y^n) sums (x + y) powr a" |
244 shows "(\<lambda>n. (a gchoose n) * x powr (a - of_nat n) * y^n) sums (x + y) powr a" |
245 using gen_binomial_real'[OF assms] by (simp add: mult_ac add.commute) |
245 using gen_binomial_real'[OF assms] by (simp add: mult_ac add.commute) |
246 |
246 |
247 lemma sqrt_series': |
247 lemma sqrt_series': |
248 "\<bar>z\<bar> < a \<Longrightarrow> (\<lambda>n. ((1/2) gchoose n) * a powr (1/2 - real_of_nat n) * z ^ n) sums |
248 "\<bar>z\<bar> < a \<Longrightarrow> (\<lambda>n. ((1/2) gchoose n) * a powr (1/2 - real_of_nat n) * z ^ n) sums |
249 sqrt (a + z :: real)" |
249 sqrt (a + z :: real)" |
250 using gen_binomial_real''[of z a "1/2"] by (simp add: powr_half_sqrt) |
250 using gen_binomial_real''[of z a "1/2"] by (simp add: powr_half_sqrt) |
251 |
251 |
252 lemma sqrt_series: |
252 lemma sqrt_series: |
253 "\<bar>z\<bar> < 1 \<Longrightarrow> (\<lambda>n. ((1/2) gchoose n) * z ^ n) sums sqrt (1 + z)" |
253 "\<bar>z\<bar> < 1 \<Longrightarrow> (\<lambda>n. ((1/2) gchoose n) * z ^ n) sums sqrt (1 + z)" |