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
hoelzl@63627
     1
(*  Title:    HOL/Analysis/Generalised_Binomial_Theorem.thy
hoelzl@62055
     2
    Author:   Manuel Eberl, TU M√ľnchen
hoelzl@62055
     3
*)
hoelzl@62055
     4
hoelzl@62055
     5
section \<open>Generalised Binomial Theorem\<close>
hoelzl@62055
     6
hoelzl@62055
     7
text \<open>
eberlm@62049
     8
  The proof of the Generalised Binomial Theorem and related results.
hoelzl@62055
     9
  We prove the generalised binomial theorem for complex numbers, following the proof at:
hoelzl@62055
    10
  \url{https://proofwiki.org/wiki/Binomial_Theorem/General_Binomial_Theorem}
hoelzl@62055
    11
\<close>
hoelzl@62055
    12
eberlm@62049
    13
theory Generalised_Binomial_Theorem
hoelzl@63594
    14
imports
hoelzl@63594
    15
  Complex_Main
eberlm@62049
    16
  Complex_Transcendental
hoelzl@63594
    17
  Summation_Tests
eberlm@62049
    18
begin
eberlm@62049
    19
eberlm@62049
    20
lemma gbinomial_ratio_limit:
eberlm@62049
    21
  fixes a :: "'a :: real_normed_field"
eberlm@62049
    22
  assumes "a \<notin> \<nat>"
eberlm@62049
    23
  shows "(\<lambda>n. (a gchoose n) / (a gchoose Suc n)) \<longlonglongrightarrow> -1"
eberlm@62049
    24
proof (rule Lim_transform_eventually)
eberlm@62049
    25
  let ?f = "\<lambda>n. inverse (a / of_nat (Suc n) - of_nat n / of_nat (Suc n))"
eberlm@62049
    26
  from eventually_gt_at_top[of "0::nat"]
eberlm@62049
    27
    show "eventually (\<lambda>n. ?f n = (a gchoose n) /(a gchoose Suc n)) sequentially"
eberlm@62049
    28
  proof eventually_elim
eberlm@62049
    29
    fix n :: nat assume n: "n > 0"
haftmann@63417
    30
    then obtain q where q: "n = Suc q" by (cases n) blast
haftmann@63417
    31
    let ?P = "\<Prod>i=0..<n. a - of_nat i"
eberlm@62049
    32
    from n have "(a gchoose n) / (a gchoose Suc n) = (of_nat (Suc n) :: 'a) *
haftmann@63417
    33
                   (?P / (\<Prod>i=0..n. a - of_nat i))"
nipkow@64272
    34
      by (simp add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
haftmann@63417
    35
    also from q have "(\<Prod>i=0..n. a - of_nat i) = ?P * (a - of_nat n)"
nipkow@64272
    36
      by (simp add: prod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
eberlm@62049
    37
    also have "?P / \<dots> = (?P / ?P) / (a - of_nat n)" by (rule divide_divide_eq_left[symmetric])
eberlm@62049
    38
    also from assms have "?P / ?P = 1" by auto
hoelzl@63594
    39
    also have "of_nat (Suc n) * (1 / (a - of_nat n)) =
eberlm@62049
    40
                   inverse (inverse (of_nat (Suc n)) * (a - of_nat n))" by (simp add: field_simps)
eberlm@62049
    41
    also have "inverse (of_nat (Suc n)) * (a - of_nat n) = a / of_nat (Suc n) - of_nat n / of_nat (Suc n)"
eberlm@62049
    42
      by (simp add: field_simps del: of_nat_Suc)
eberlm@62049
    43
    finally show "?f n = (a gchoose n) / (a gchoose Suc n)" by simp
eberlm@62049
    44
  qed
eberlm@62049
    45
hoelzl@63594
    46
  have "(\<lambda>n. norm a / (of_nat (Suc n))) \<longlonglongrightarrow> 0"
eberlm@62049
    47
    unfolding divide_inverse
eberlm@62049
    48
    by (intro tendsto_mult_right_zero LIMSEQ_inverse_real_of_nat)
eberlm@62049
    49
  hence "(\<lambda>n. a / of_nat (Suc n)) \<longlonglongrightarrow> 0"
eberlm@62049
    50
    by (subst tendsto_norm_zero_iff[symmetric]) (simp add: norm_divide del: of_nat_Suc)
eberlm@62049
    51
  hence "?f \<longlonglongrightarrow> inverse (0 - 1)"
eberlm@62049
    52
    by (intro tendsto_inverse tendsto_diff LIMSEQ_n_over_Suc_n) simp_all
eberlm@62049
    53
  thus "?f \<longlonglongrightarrow> -1" by simp
eberlm@62049
    54
qed
eberlm@62049
    55
eberlm@62049
    56
lemma conv_radius_gchoose:
eberlm@62049
    57
  fixes a :: "'a :: {real_normed_field,banach}"
eberlm@62049
    58
  shows "conv_radius (\<lambda>n. a gchoose n) = (if a \<in> \<nat> then \<infinity> else 1)"
eberlm@62049
    59
proof (cases "a \<in> \<nat>")
eberlm@62049
    60
  assume a: "a \<in> \<nat>"
eberlm@62049
    61
  have "eventually (\<lambda>n. (a gchoose n) = 0) sequentially"
eberlm@62049
    62
    using eventually_gt_at_top[of "nat \<lfloor>norm a\<rfloor>"]
eberlm@62049
    63
    by eventually_elim (insert a, auto elim!: Nats_cases simp: binomial_gbinomial[symmetric])
eberlm@66466
    64
  from conv_radius_cong'[OF this] a show ?thesis by simp
eberlm@62049
    65
next
eberlm@62049
    66
  assume a: "a \<notin> \<nat>"
eberlm@62049
    67
  from tendsto_norm[OF gbinomial_ratio_limit[OF this]]
eberlm@62049
    68
    have "conv_radius (\<lambda>n. a gchoose n) = 1"
eberlm@62049
    69
    by (intro conv_radius_ratio_limit_nonzero[of _ 1]) (simp_all add: norm_divide)
eberlm@62049
    70
  with a show ?thesis by simp
eberlm@62049
    71
qed
eberlm@62049
    72
eberlm@68643
    73
theorem gen_binomial_complex:
eberlm@62049
    74
  fixes z :: complex
eberlm@62049
    75
  assumes "norm z < 1"
eberlm@62049
    76
  shows   "(\<lambda>n. (a gchoose n) * z^n) sums (1 + z) powr a"
eberlm@62049
    77
proof -
wenzelm@63040
    78
  define K where "K = 1 - (1 - norm z) / 2"
eberlm@62049
    79
  from assms have K: "K > 0" "K < 1" "norm z < K"
eberlm@62049
    80
     unfolding K_def by (auto simp: field_simps intro!: add_pos_nonneg)
eberlm@62049
    81
  let ?f = "\<lambda>n. a gchoose n" and ?f' = "diffs (\<lambda>n. a gchoose n)"
eberlm@62049
    82
  have summable_strong: "summable (\<lambda>n. ?f n * z ^ n)" if "norm z < 1" for z using that
eberlm@62049
    83
    by (intro summable_in_conv_radius) (simp_all add: conv_radius_gchoose)
eberlm@62049
    84
  with K have summable: "summable (\<lambda>n. ?f n * z ^ n)" if "norm z < K" for z using that by auto
eberlm@62049
    85
  hence summable': "summable (\<lambda>n. ?f' n * z ^ n)" if "norm z < K" for z using that
eberlm@62049
    86
    by (intro termdiff_converges[of _ K]) simp_all
hoelzl@63594
    87
wenzelm@63040
    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
eberlm@62049
    89
  {
eberlm@62049
    90
    fix z :: complex assume z: "norm z < K"
eberlm@62049
    91
    from summable_mult2[OF summable'[OF z], of z]
eberlm@62049
    92
      have summable1: "summable (\<lambda>n. ?f' n * z ^ Suc n)" by (simp add: mult_ac)
hoelzl@63594
    93
    hence summable2: "summable (\<lambda>n. of_nat n * ?f n * z^n)"
eberlm@62049
    94
      unfolding diffs_def by (subst (asm) summable_Suc_iff)
eberlm@62049
    95
eberlm@62049
    96
    have "(1 + z) * f' z = (\<Sum>n. ?f' n * z^n) + (\<Sum>n. ?f' n * z^Suc n)"
wenzelm@63040
    97
      unfolding f_f'_def using summable' z by (simp add: algebra_simps suminf_mult)
eberlm@62049
    98
    also have "(\<Sum>n. ?f' n * z^n) = (\<Sum>n. of_nat (Suc n) * ?f (Suc n) * z^n)"
eberlm@62049
    99
      by (intro suminf_cong) (simp add: diffs_def)
hoelzl@63594
   100
    also have "(\<Sum>n. ?f' n * z^Suc n) = (\<Sum>n. of_nat n * ?f n * z ^ n)"
eberlm@62049
   101
      using summable1 suminf_split_initial_segment[OF summable1] unfolding diffs_def
eberlm@62049
   102
      by (subst suminf_split_head, subst (asm) summable_Suc_iff) simp_all
eberlm@62049
   103
    also have "(\<Sum>n. of_nat (Suc n) * ?f (Suc n) * z^n) + (\<Sum>n. of_nat n * ?f n * z^n) =
eberlm@62049
   104
                 (\<Sum>n. a * ?f n * z^n)"
eberlm@62049
   105
      by (subst gbinomial_mult_1, subst suminf_add)
hoelzl@63594
   106
         (insert summable'[OF z] summable2,
eberlm@62049
   107
          simp_all add: summable_powser_split_head algebra_simps diffs_def)
wenzelm@63040
   108
    also have "\<dots> = a * f z" unfolding f_f'_def
eberlm@62049
   109
      by (subst suminf_mult[symmetric]) (simp_all add: summable[OF z] mult_ac)
eberlm@62049
   110
    finally have "a * f z = (1 + z) * f' z" by simp
eberlm@62049
   111
  } note deriv = this
eberlm@62049
   112
eberlm@62049
   113
  have [derivative_intros]: "(f has_field_derivative f' z) (at z)" if "norm z < of_real K" for z
wenzelm@63040
   114
    unfolding f_f'_def using K that
eberlm@62049
   115
    by (intro termdiffs_strong[of "?f" K z] summable_strong) simp_all
wenzelm@63040
   116
  have "f 0 = (\<Sum>n. if n = 0 then 1 else 0)" unfolding f_f'_def by (intro suminf_cong) simp
eberlm@62049
   117
  also have "\<dots> = 1" using sums_single[of 0 "\<lambda>_. 1::complex"] unfolding sums_iff by simp
eberlm@62049
   118
  finally have [simp]: "f 0 = 1" .
eberlm@62049
   119
eberlm@62049
   120
  have "\<exists>c. \<forall>z\<in>ball 0 K. f z * (1 + z) powr (-a) = c"
eberlm@62049
   121
  proof (rule has_field_derivative_zero_constant)
eberlm@62049
   122
    fix z :: complex assume z': "z \<in> ball 0 K"
haftmann@63417
   123
    hence z: "norm z < K" by simp
eberlm@62049
   124
    with K have nz: "1 + z \<noteq> 0" by (auto dest!: minus_unique)
eberlm@62049
   125
    from z K have "norm z < 1" by simp
lp15@65274
   126
    hence "(1 + z) \<notin> \<real>\<^sub>\<le>\<^sub>0" by (cases z) (auto simp: Complex_eq complex_nonpos_Reals_iff)
hoelzl@63594
   127
    hence "((\<lambda>z. f z * (1 + z) powr (-a)) has_field_derivative
eberlm@62049
   128
              f' z * (1 + z) powr (-a) - a * f z * (1 + z) powr (-a-1)) (at z)" using z
eberlm@62049
   129
      by (auto intro!: derivative_eq_intros)
eberlm@62049
   130
    also from z have "a * f z = (1 + z) * f' z" by (rule deriv)
hoelzl@63594
   131
    finally show "((\<lambda>z. f z * (1 + z) powr (-a)) has_field_derivative 0) (at z within ball 0 K)"
lp15@65583
   132
      using nz by (simp add: field_simps powr_diff at_within_open[OF z'])
eberlm@62049
   133
  qed simp_all
eberlm@62049
   134
  then obtain c where c: "\<And>z. z \<in> ball 0 K \<Longrightarrow> f z * (1 + z) powr (-a) = c" by blast
eberlm@62049
   135
  from c[of 0] and K have "c = 1" by simp
hoelzl@63594
   136
  with c[of z] have "f z = (1 + z) powr a" using K
lp15@65583
   137
    by (simp add: powr_minus field_simps dist_complex_def)
wenzelm@63040
   138
  with summable K show ?thesis unfolding f_f'_def by (simp add: sums_iff)
eberlm@62049
   139
qed
eberlm@62049
   140
eberlm@62049
   141
lemma gen_binomial_complex':
eberlm@62049
   142
  fixes x y :: real and a :: complex
eberlm@62049
   143
  assumes "\<bar>x\<bar> < \<bar>y\<bar>"
hoelzl@63594
   144
  shows   "(\<lambda>n. (a gchoose n) * of_real x^n * of_real y powr (a - of_nat n)) sums
eberlm@62049
   145
               of_real (x + y) powr a" (is "?P x y")
eberlm@62049
   146
proof -
eberlm@62049
   147
  {
eberlm@62049
   148
    fix x y :: real assume xy: "\<bar>x\<bar> < \<bar>y\<bar>" "y \<ge> 0"
eberlm@62049
   149
    hence "y > 0" by simp
eberlm@62049
   150
    note xy = xy this
eberlm@62049
   151
    from xy have "(\<lambda>n. (a gchoose n) * of_real (x / y) ^ n) sums (1 + of_real (x / y)) powr a"
eberlm@62049
   152
        by (intro gen_binomial_complex) (simp add: norm_divide)
hoelzl@63594
   153
    hence "(\<lambda>n. (a gchoose n) * of_real (x / y) ^ n * y powr a) sums
eberlm@62049
   154
               ((1 + of_real (x / y)) powr a * y powr a)"
eberlm@62049
   155
      by (rule sums_mult2)
eberlm@62049
   156
    also have "(1 + complex_of_real (x / y)) = complex_of_real (1 + x/y)" by simp
eberlm@62049
   157
    also from xy have "\<dots> powr a * of_real y powr a = (\<dots> * y) powr a"
eberlm@62049
   158
      by (subst powr_times_real[symmetric]) (simp_all add: field_simps)
eberlm@62049
   159
    also from xy have "complex_of_real (1 + x / y) * complex_of_real y = of_real (x + y)"
eberlm@62049
   160
      by (simp add: field_simps)
lp15@65583
   161
    finally have "?P x y" using xy by (simp add: field_simps powr_diff powr_nat)
eberlm@62049
   162
  } note A = this
eberlm@62049
   163
eberlm@62049
   164
  show ?thesis
eberlm@62049
   165
  proof (cases "y < 0")
eberlm@62049
   166
    assume y: "y < 0"
eberlm@62049
   167
    with assms have xy: "x + y < 0" by simp
eberlm@62049
   168
    with assms have "\<bar>-x\<bar> < \<bar>-y\<bar>" "-y \<ge> 0" by simp_all
eberlm@62049
   169
    note A[OF this]
eberlm@62049
   170
    also have "complex_of_real (-x + -y) = - complex_of_real (x + y)" by simp
eberlm@62049
   171
    also from xy assms have "... powr a = (-1) powr -a * of_real (x + y) powr a"
nipkow@62390
   172
      by (subst powr_neg_real_complex) (simp add: abs_real_def split: if_split_asm)
eberlm@62049
   173
    also {
eberlm@62049
   174
      fix n :: nat
hoelzl@63594
   175
      from y have "(a gchoose n) * of_real (-x) ^ n * of_real (-y) powr (a - of_nat n) =
eberlm@62049
   176
                       (a gchoose n) * (-of_real x / -of_real y) ^ n * (- of_real y) powr a"
lp15@65583
   177
        by (subst power_divide) (simp add: powr_diff powr_nat)
eberlm@62049
   178
      also from y have "(- of_real y) powr a = (-1) powr -a * of_real y powr a"
eberlm@62049
   179
        by (subst powr_neg_real_complex) simp
eberlm@62049
   180
      also have "-complex_of_real x / -complex_of_real y = complex_of_real x / complex_of_real y"
eberlm@62049
   181
        by simp
eberlm@62049
   182
      also have "... ^ n = of_real x ^ n / of_real y ^ n" by (simp add: power_divide)
hoelzl@63594
   183
      also have "(a gchoose n) * ... * ((-1) powr -a * of_real y powr a) =
eberlm@62049
   184
                   (-1) powr -a * ((a gchoose n) * of_real x ^ n * of_real y powr (a - n))"
lp15@65583
   185
        by (simp add: algebra_simps powr_diff powr_nat)
eberlm@62049
   186
      finally have "(a gchoose n) * of_real (- x) ^ n * of_real (- y) powr (a - of_nat n) =
eberlm@62049
   187
                      (-1) powr -a * ((a gchoose n) * of_real x ^ n * of_real y powr (a - of_nat n))" .
eberlm@62049
   188
    }
eberlm@62049
   189
    note sums_cong[OF this]
eberlm@62049
   190
    finally show ?thesis by (simp add: sums_mult_iff)
eberlm@62049
   191
  qed (insert A[of x y] assms, simp_all add: not_less)
eberlm@62049
   192
qed
eberlm@62049
   193
eberlm@62049
   194
lemma gen_binomial_complex'':
eberlm@62049
   195
  fixes x y :: real and a :: complex
eberlm@62049
   196
  assumes "\<bar>y\<bar> < \<bar>x\<bar>"
hoelzl@63594
   197
  shows   "(\<lambda>n. (a gchoose n) * of_real x powr (a - of_nat n) * of_real y ^ n) sums
eberlm@62049
   198
               of_real (x + y) powr a"
eberlm@62049
   199
  using gen_binomial_complex'[OF assms] by (simp add: mult_ac add.commute)
eberlm@62049
   200
eberlm@62049
   201
lemma gen_binomial_real:
eberlm@62049
   202
  fixes z :: real
eberlm@62049
   203
  assumes "\<bar>z\<bar> < 1"
eberlm@62049
   204
  shows   "(\<lambda>n. (a gchoose n) * z^n) sums (1 + z) powr a"
eberlm@62049
   205
proof -
eberlm@62049
   206
  from assms have "norm (of_real z :: complex) < 1" by simp
eberlm@62049
   207
  from gen_binomial_complex[OF this]
eberlm@62049
   208
    have "(\<lambda>n. (of_real a gchoose n :: complex) * of_real z ^ n) sums
eberlm@62049
   209
              (of_real (1 + z)) powr (of_real a)" by simp
eberlm@62049
   210
  also have "(of_real (1 + z) :: complex) powr (of_real a) = of_real ((1 + z) powr a)"
eberlm@62049
   211
    using assms by (subst powr_of_real) simp_all
hoelzl@63594
   212
  also have "(of_real a gchoose n :: complex) = of_real (a gchoose n)" for n
nipkow@64272
   213
    by (simp add: gbinomial_prod_rev)
eberlm@62049
   214
  hence "(\<lambda>n. (of_real a gchoose n :: complex) * of_real z ^ n) =
eberlm@62049
   215
           (\<lambda>n. of_real ((a gchoose n) * z ^ n))" by (intro ext) simp
eberlm@62049
   216
  finally show ?thesis by (simp only: sums_of_real_iff)
hoelzl@63594
   217
qed
eberlm@62049
   218
eberlm@62049
   219
lemma gen_binomial_real':
eberlm@62049
   220
  fixes x y a :: real
eberlm@62049
   221
  assumes "\<bar>x\<bar> < y"
eberlm@62049
   222
  shows   "(\<lambda>n. (a gchoose n) * x^n * y powr (a - of_nat n)) sums (x + y) powr a"
eberlm@62049
   223
proof -
eberlm@62049
   224
  from assms have "y > 0" by simp
eberlm@62049
   225
  note xy = this assms
eberlm@62049
   226
  from assms have "\<bar>x / y\<bar> < 1" by simp
eberlm@62049
   227
  hence "(\<lambda>n. (a gchoose n) * (x / y) ^ n) sums (1 + x / y) powr a"
eberlm@62049
   228
    by (rule gen_binomial_real)
eberlm@62049
   229
  hence "(\<lambda>n. (a gchoose n) * (x / y) ^ n * y powr a) sums ((1 + x / y) powr a * y powr a)"
eberlm@62049
   230
    by (rule sums_mult2)
hoelzl@63594
   231
  with xy show ?thesis
lp15@65583
   232
    by (simp add: field_simps powr_divide powr_diff powr_realpow)
eberlm@62049
   233
qed
eberlm@62049
   234
eberlm@62049
   235
lemma one_plus_neg_powr_powser:
eberlm@62049
   236
  fixes z s :: complex
eberlm@62049
   237
  assumes "norm (z :: complex) < 1"
eberlm@62049
   238
  shows "(\<lambda>n. (-1)^n * ((s + n - 1) gchoose n) * z^n) sums (1 + z) powr (-s)"
eberlm@62049
   239
    using gen_binomial_complex[OF assms, of "-s"] by (simp add: gbinomial_minus)
eberlm@62049
   240
eberlm@62049
   241
lemma gen_binomial_real'':
eberlm@62049
   242
  fixes x y a :: real
eberlm@62049
   243
  assumes "\<bar>y\<bar> < x"
eberlm@62049
   244
  shows   "(\<lambda>n. (a gchoose n) * x powr (a - of_nat n) * y^n) sums (x + y) powr a"
eberlm@62049
   245
  using gen_binomial_real'[OF assms] by (simp add: mult_ac add.commute)
eberlm@62049
   246
eberlm@62049
   247
lemma sqrt_series':
hoelzl@63594
   248
  "\<bar>z\<bar> < a \<Longrightarrow> (\<lambda>n. ((1/2) gchoose n) * a powr (1/2 - real_of_nat n) * z ^ n) sums
eberlm@62049
   249
                  sqrt (a + z :: real)"
eberlm@62049
   250
  using gen_binomial_real''[of z a "1/2"] by (simp add: powr_half_sqrt)
eberlm@62049
   251
eberlm@62049
   252
lemma sqrt_series:
eberlm@62049
   253
  "\<bar>z\<bar> < 1 \<Longrightarrow> (\<lambda>n. ((1/2) gchoose n) * z ^ n) sums sqrt (1 + z)"
eberlm@62049
   254
  using gen_binomial_real[of z "1/2"] by (simp add: powr_half_sqrt)
eberlm@62049
   255
nipkow@62390
   256
end