src/HOL/Analysis/Generalised_Binomial_Theorem.thy
 author nipkow Sat Dec 29 15:43:53 2018 +0100 (6 months ago) changeset 69529 4ab9657b3257 parent 68643 3db6c9338ec1 child 70138 bd42cc1e10d0 permissions -rw-r--r--
capitalize proper names in lemma names
```     1 (*  Title:    HOL/Analysis/Generalised_Binomial_Theorem.thy
```
```     2     Author:   Manuel Eberl, TU München
```
```     3 *)
```
```     4
```
```     5 section \<open>Generalised Binomial Theorem\<close>
```
```     6
```
```     7 text \<open>
```
```     8   The proof of the Generalised Binomial Theorem and related results.
```
```     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}
```
```    11 \<close>
```
```    12
```
```    13 theory Generalised_Binomial_Theorem
```
```    14 imports
```
```    15   Complex_Main
```
```    16   Complex_Transcendental
```
```    17   Summation_Tests
```
```    18 begin
```
```    19
```
```    20 lemma gbinomial_ratio_limit:
```
```    21   fixes a :: "'a :: real_normed_field"
```
```    22   assumes "a \<notin> \<nat>"
```
```    23   shows "(\<lambda>n. (a gchoose n) / (a gchoose Suc n)) \<longlonglongrightarrow> -1"
```
```    24 proof (rule Lim_transform_eventually)
```
```    25   let ?f = "\<lambda>n. inverse (a / of_nat (Suc n) - of_nat n / of_nat (Suc n))"
```
```    26   from eventually_gt_at_top[of "0::nat"]
```
```    27     show "eventually (\<lambda>n. ?f n = (a gchoose n) /(a gchoose Suc n)) sequentially"
```
```    28   proof eventually_elim
```
```    29     fix n :: nat assume n: "n > 0"
```
```    30     then obtain q where q: "n = Suc q" by (cases n) blast
```
```    31     let ?P = "\<Prod>i=0..<n. a - of_nat i"
```
```    32     from n have "(a gchoose n) / (a gchoose Suc n) = (of_nat (Suc n) :: 'a) *
```
```    33                    (?P / (\<Prod>i=0..n. a - of_nat i))"
```
```    34       by (simp add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
```
```    35     also from q have "(\<Prod>i=0..n. a - of_nat i) = ?P * (a - of_nat n)"
```
```    36       by (simp add: prod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
```
```    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
```
```    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)
```
```    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)
```
```    43     finally show "?f n = (a gchoose n) / (a gchoose Suc n)" by simp
```
```    44   qed
```
```    45
```
```    46   have "(\<lambda>n. norm a / (of_nat (Suc n))) \<longlonglongrightarrow> 0"
```
```    47     unfolding divide_inverse
```
```    48     by (intro tendsto_mult_right_zero LIMSEQ_inverse_real_of_nat)
```
```    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)
```
```    51   hence "?f \<longlonglongrightarrow> inverse (0 - 1)"
```
```    52     by (intro tendsto_inverse tendsto_diff LIMSEQ_n_over_Suc_n) simp_all
```
```    53   thus "?f \<longlonglongrightarrow> -1" by simp
```
```    54 qed
```
```    55
```
```    56 lemma conv_radius_gchoose:
```
```    57   fixes a :: "'a :: {real_normed_field,banach}"
```
```    58   shows "conv_radius (\<lambda>n. a gchoose n) = (if a \<in> \<nat> then \<infinity> else 1)"
```
```    59 proof (cases "a \<in> \<nat>")
```
```    60   assume a: "a \<in> \<nat>"
```
```    61   have "eventually (\<lambda>n. (a gchoose n) = 0) sequentially"
```
```    62     using eventually_gt_at_top[of "nat \<lfloor>norm a\<rfloor>"]
```
```    63     by eventually_elim (insert a, auto elim!: Nats_cases simp: binomial_gbinomial[symmetric])
```
```    64   from conv_radius_cong'[OF this] a show ?thesis by simp
```
```    65 next
```
```    66   assume a: "a \<notin> \<nat>"
```
```    67   from tendsto_norm[OF gbinomial_ratio_limit[OF this]]
```
```    68     have "conv_radius (\<lambda>n. a gchoose n) = 1"
```
```    69     by (intro conv_radius_ratio_limit_nonzero[of _ 1]) (simp_all add: norm_divide)
```
```    70   with a show ?thesis by simp
```
```    71 qed
```
```    72
```
```    73 theorem gen_binomial_complex:
```
```    74   fixes z :: complex
```
```    75   assumes "norm z < 1"
```
```    76   shows   "(\<lambda>n. (a gchoose n) * z^n) sums (1 + z) powr a"
```
```    77 proof -
```
```    78   define K where "K = 1 - (1 - norm z) / 2"
```
```    79   from assms have K: "K > 0" "K < 1" "norm z < K"
```
```    80      unfolding K_def by (auto simp: field_simps intro!: add_pos_nonneg)
```
```    81   let ?f = "\<lambda>n. a gchoose n" and ?f' = "diffs (\<lambda>n. a gchoose n)"
```
```    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)
```
```    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
```
```    86     by (intro termdiff_converges[of _ K]) simp_all
```
```    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
```
```    89   {
```
```    90     fix z :: complex assume z: "norm z < K"
```
```    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)
```
```    93     hence summable2: "summable (\<lambda>n. of_nat n * ?f n * z^n)"
```
```    94       unfolding diffs_def by (subst (asm) summable_Suc_iff)
```
```    95
```
```    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)
```
```    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)
```
```   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
```
```   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) =
```
```   104                  (\<Sum>n. a * ?f n * z^n)"
```
```   105       by (subst gbinomial_mult_1, subst suminf_add)
```
```   106          (insert summable'[OF z] summable2,
```
```   107           simp_all add: summable_powser_split_head algebra_simps diffs_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)
```
```   110     finally have "a * f z = (1 + z) * f' z" by simp
```
```   111   } note deriv = this
```
```   112
```
```   113   have [derivative_intros]: "(f has_field_derivative f' z) (at z)" if "norm z < of_real K" for z
```
```   114     unfolding f_f'_def using K that
```
```   115     by (intro termdiffs_strong[of "?f" K z] summable_strong) simp_all
```
```   116   have "f 0 = (\<Sum>n. if n = 0 then 1 else 0)" unfolding f_f'_def by (intro suminf_cong) simp
```
```   117   also have "\<dots> = 1" using sums_single[of 0 "\<lambda>_. 1::complex"] unfolding sums_iff by simp
```
```   118   finally have [simp]: "f 0 = 1" .
```
```   119
```
```   120   have "\<exists>c. \<forall>z\<in>ball 0 K. f z * (1 + z) powr (-a) = c"
```
```   121   proof (rule has_field_derivative_zero_constant)
```
```   122     fix z :: complex assume z': "z \<in> ball 0 K"
```
```   123     hence z: "norm z < K" by simp
```
```   124     with K have nz: "1 + z \<noteq> 0" by (auto dest!: minus_unique)
```
```   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_eq complex_nonpos_Reals_iff)
```
```   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
```
```   129       by (auto intro!: derivative_eq_intros)
```
```   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)"
```
```   132       using nz by (simp add: field_simps powr_diff at_within_open[OF z'])
```
```   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
```
```   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
```
```   137     by (simp add: powr_minus field_simps dist_complex_def)
```
```   138   with summable K show ?thesis unfolding f_f'_def by (simp add: sums_iff)
```
```   139 qed
```
```   140
```
```   141 lemma gen_binomial_complex':
```
```   142   fixes x y :: real and a :: complex
```
```   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
```
```   145                of_real (x + y) powr a" (is "?P x y")
```
```   146 proof -
```
```   147   {
```
```   148     fix x y :: real assume xy: "\<bar>x\<bar> < \<bar>y\<bar>" "y \<ge> 0"
```
```   149     hence "y > 0" by simp
```
```   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"
```
```   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
```
```   154                ((1 + of_real (x / y)) powr a * y powr a)"
```
```   155       by (rule sums_mult2)
```
```   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"
```
```   158       by (subst powr_times_real[symmetric]) (simp_all add: field_simps)
```
```   159     also from xy have "complex_of_real (1 + x / y) * complex_of_real y = of_real (x + y)"
```
```   160       by (simp add: field_simps)
```
```   161     finally have "?P x y" using xy by (simp add: field_simps powr_diff powr_nat)
```
```   162   } note A = this
```
```   163
```
```   164   show ?thesis
```
```   165   proof (cases "y < 0")
```
```   166     assume y: "y < 0"
```
```   167     with assms have xy: "x + y < 0" by simp
```
```   168     with assms have "\<bar>-x\<bar> < \<bar>-y\<bar>" "-y \<ge> 0" by simp_all
```
```   169     note A[OF this]
```
```   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"
```
```   172       by (subst powr_neg_real_complex) (simp add: abs_real_def split: if_split_asm)
```
```   173     also {
```
```   174       fix n :: nat
```
```   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"
```
```   177         by (subst power_divide) (simp add: powr_diff powr_nat)
```
```   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
```
```   180       also have "-complex_of_real x / -complex_of_real y = complex_of_real x / complex_of_real y"
```
```   181         by simp
```
```   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) =
```
```   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 powr_nat)
```
```   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))" .
```
```   188     }
```
```   189     note sums_cong[OF this]
```
```   190     finally show ?thesis by (simp add: sums_mult_iff)
```
```   191   qed (insert A[of x y] assms, simp_all add: not_less)
```
```   192 qed
```
```   193
```
```   194 lemma gen_binomial_complex'':
```
```   195   fixes x y :: real and a :: complex
```
```   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
```
```   198                of_real (x + y) powr a"
```
```   199   using gen_binomial_complex'[OF assms] by (simp add: mult_ac add.commute)
```
```   200
```
```   201 lemma gen_binomial_real:
```
```   202   fixes z :: real
```
```   203   assumes "\<bar>z\<bar> < 1"
```
```   204   shows   "(\<lambda>n. (a gchoose n) * z^n) sums (1 + z) powr a"
```
```   205 proof -
```
```   206   from assms have "norm (of_real z :: complex) < 1" by simp
```
```   207   from gen_binomial_complex[OF this]
```
```   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
```
```   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
```
```   212   also have "(of_real a gchoose n :: complex) = of_real (a gchoose n)" for n
```
```   213     by (simp add: gbinomial_prod_rev)
```
```   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
```
```   216   finally show ?thesis by (simp only: sums_of_real_iff)
```
```   217 qed
```
```   218
```
```   219 lemma gen_binomial_real':
```
```   220   fixes x y a :: real
```
```   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"
```
```   223 proof -
```
```   224   from assms have "y > 0" by simp
```
```   225   note xy = this assms
```
```   226   from assms have "\<bar>x / y\<bar> < 1" by simp
```
```   227   hence "(\<lambda>n. (a gchoose n) * (x / y) ^ n) sums (1 + x / y) powr a"
```
```   228     by (rule gen_binomial_real)
```
```   229   hence "(\<lambda>n. (a gchoose n) * (x / y) ^ n * y powr a) sums ((1 + x / y) powr a * y powr a)"
```
```   230     by (rule sums_mult2)
```
```   231   with xy show ?thesis
```
```   232     by (simp add: field_simps powr_divide powr_diff powr_realpow)
```
```   233 qed
```
```   234
```
```   235 lemma one_plus_neg_powr_powser:
```
```   236   fixes z s :: complex
```
```   237   assumes "norm (z :: complex) < 1"
```
```   238   shows "(\<lambda>n. (-1)^n * ((s + n - 1) gchoose n) * z^n) sums (1 + z) powr (-s)"
```
```   239     using gen_binomial_complex[OF assms, of "-s"] by (simp add: gbinomial_minus)
```
```   240
```
```   241 lemma gen_binomial_real'':
```
```   242   fixes x y a :: real
```
```   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"
```
```   245   using gen_binomial_real'[OF assms] by (simp add: mult_ac add.commute)
```
```   246
```
```   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
```
```   249                   sqrt (a + z :: real)"
```
```   250   using gen_binomial_real''[of z a "1/2"] by (simp add: powr_half_sqrt)
```
```   251
```
```   252 lemma sqrt_series:
```
```   253   "\<bar>z\<bar> < 1 \<Longrightarrow> (\<lambda>n. ((1/2) gchoose n) * z ^ n) sums sqrt (1 + z)"
```
```   254   using gen_binomial_real[of z "1/2"] by (simp add: powr_half_sqrt)
```
```   255
```
```   256 end
```