weblib/arithmetics/binomial.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/sigma_pi.ma".
  13 include "arithmetics/primes.ma".
  14
  15 (* binomial coefficient *)
  16 definition bc ≝ λn,k. n!/(k!*(n-k)!).
  17
  18 lemma bceq :∀n,k. bc n k = n!/(k!*(n-k)!).
  19 // qed.
  20
  21 theorem bc_n_n: ∀n. bc n n = 1.
  22 #n >bceq <minus_n_n <times_n_1 @div_n_n //
  23 qed.
  24
  25 theorem bc_n_O: ∀n. bc n O = 1.
  26 #n >bceq <minus_n_O /2/
  27 qed.
  28
  29 theorem fact_minus: ∀n,k. k < n →
  30   (n - S k)!*(n-k) = (n - k)!.
  31 #n #k (cases n)
  32   [#ltO @False_ind /2/
  33   |#l #ltl >(minus_Sn_m k) [// |@le_S_S_to_le //]
  34   ]
  35 qed.
  36
  37 theorem bc2 : ∀n.
  38 ∀k. k ≤n → k!*(n-k)! ∣ n!.
  39 #n (elim n)
  40   [#k #lek0 <(le_n_O_to_eq ? lek0) //
  41   |#m #Hind #k (cases k) normalize //
  42      #c #lec cases (le_to_or_lt_eq … (le_S_S_to_le …lec))
  43     [#ltcm
  44      cut (m-(m-(S c)) = S c) [@plus_to_minus @plus_minus_m_m //] #eqSc
  45      lapply (Hind c (le_S_S_to_le … lec)) #Hc
  46      lapply (Hind (m - (S c)) ?) [@le_plus_to_minus //] >eqSc #Hmc
  47      >(plus_minus_m_m m c) in ⊢ (??(??(?%))) [|@le_S_S_to_le //]
  48      >commutative_plus >(distributive_times_plus ? (S c))
  49      @divides_plus
  50       [>associative_times >(commutative_times (S c))
  51        <associative_times @divides_times //
  52       |<(fact_minus …ltcm) in ⊢ (?(??%)?)
  53        <associative_times @divides_times //
  54        >commutative_times @Hmc
  55       ]
  56     |#eqcm >eqcm <minus_n_n <times_n_1 //
  57     ]
  58   ]
  59 qed.
  60
  61 theorem bc1: ∀n.∀k. k < n →
  62   bc (S n) (S k) = (bc n k) + (bc n (S k)).
  63 #n #k #ltkn > bceq >(bceq n) >(bceq n (S k))
  64 >(div_times_times ?? (S k)) in ⊢ (???(?%?))
  65   [|>(times_n_O 0) @lt_times // | //]
  66 >associative_times in ⊢ (???(?(??%)?))
  67 >commutative_times in ⊢ (???(?(??(??%))?))
  68 <associative_times in ⊢ (???(?(??%)?))
  69 >(div_times_times ?? (n - k)) in ⊢ (???(??%))
  70   [|>(times_n_O 0) @lt_times //
  71    |@(le_plus_to_le_r k ??) <plus_minus_m_m /2/]
  72 >associative_times in ⊢ (???(??(??%)))
  73 >fact_minus // <plus_div
  74   [<distributive_times_plus
  75    >commutative_plus in ⊢ (???%) <plus_n_Sm <plus_minus_m_m [|/2/] @refl
  76   |<fact_minus // <associative_times @divides_times // @(bc2 n (S k)) //
  77   |>associative_times >(commutative_times (S k))
  78    <associative_times @divides_times // @bc2 /2/
  79   |>(times_n_O 0) @lt_times [@(le_1_fact (S k)) | //]
  80   ]
  81 qed.
  82
  83 theorem lt_O_bc: ∀n,m. m ≤ n → O < bc n m.
  84 #n (elim n)
  85   [#m #lemO @(le_n_O_elim ? lemO) //
  86   |-n #n #Hind #m (cases m) //
  87    #m #lemn cases(le_to_or_lt_eq … (le_S_S_to_le …lemn)) //
  88    #ltmn >bc1 // >(plus_O_n 0) @lt_plus @Hind /2/
  89   ]
  90 qed.
  91
  92 theorem binomial_law:∀a,b,n.
  93   (a+b)^n = Σ_{k < S n}((bc n k)*(a^(n-k))*(b^k)).
  94 #a #b #n (elim n) //
  95 -n #n #Hind normalize in ⊢ (? ? % ?).
  96 >bigop_Strue // >Hind >distributive_times_plus
  97 <(minus_n_n (S n)) <commutative_times <(commutative_times b)
  98 (* hint??? *)
  99 >(bigop_distr ???? natDop ? a) >(bigop_distr ???? natDop ? b)
 100 >bigop_Strue in ⊢ (??(??%)?) // <associative_plus
 101 <commutative_plus in ⊢ (??(? % ?) ?) >associative_plus @eq_f2
 102   [<minus_n_n >bc_n_n >bc_n_n normalize //
 103   |>bigop_0 >associative_plus >commutative_plus in ⊢ (??(??%)?)
 104    <associative_plus >bigop_0 // @eq_f2
 105     [>(bigop_op n ??? natACop) @same_bigop //
 106      #i #ltin #_ <associative_times >(commutative_times b)
 107      >(associative_times ?? b) <(distributive_times_plus_r (b^(S i)))
 108      @eq_f2 // <associative_times >(commutative_times a)
 109      >associative_times cut(∀n.a*a^n = a^(S n)) [#n @commutative_times] #H
 110      >H <minus_Sn_m // <(distributive_times_plus_r (a^(n-i)))
 111      @eq_f2 // @sym_eq >commutative_plus @bc1 //
 112     |>bc_n_O >bc_n_O normalize //
 113     ]
 114   ]
 115 qed.
 116
 117 theorem exp_S_sigma_p:∀a,n.
 118 (S a)^n = Σ_{k < S n}((bc n k)*a^(n-k)).
 119 #a #n cut (S a = a + 1) // #H >H
 120 >binomial_law @same_bigop //
 121 qed.
 122
 123 (*
 124 theorem exp_Sn_SSO: \forall n. exp (S n) 2 = S((exp n 2) + 2*n).
 125 intros.simplify.
 126 rewrite < times_n_SO.
 127 rewrite < plus_n_O.
 128 rewrite < sym_times.simplify.
 129 rewrite < assoc_plus.
 130 rewrite < sym_plus.
 131 reflexivity.
 132 qed. *)
 133