matita/matita/lib/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/primes.ma".
  13 include "arithmetics/bigops.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 by injective_plus_r/
  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 by lt_to_le/]
  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 by lt_to_le/] @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 by lt_to_le/
  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 ⊢ (??%?); >commutative_times
  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 definition M ≝ λm.bc (S(2*m)) m.
 123
 124 theorem lt_M: ∀m. O < m → M m < exp 2 (2*m).
 125 #m #posm  @(lt_times_n_to_lt_l 2)
 126   |change in ⊢ (? ? %) with (exp 2 (S(2*m))).
 127    change in ⊢ (? ? (? % ?)) with (1+1).
 128    rewrite > exp_plus_sigma_p.
 129    apply (le_to_lt_to_lt ? (sigma_p (S (S (2*m))) (λk:nat.orb (eqb k m) (eqb k (S m)))
 130             (λk:nat.bc (S (2*m)) k*(1)\sup(S (2*m)-k)*(1)\sup(k))))
 131     [rewrite > (sigma_p_gi ? ? m)
 132       [rewrite > (sigma_p_gi ? ? (S m))
 133         [rewrite > (false_to_eq_sigma_p O (S(S(2*m))))
 134           [simplify in ⊢ (? ? (? ? (? ? %))).
 135            simplify in ⊢ (? % ?).
 136            rewrite < exp_SO_n.rewrite < exp_SO_n.
 137            rewrite < exp_SO_n.rewrite < exp_SO_n.
 138            rewrite < times_n_SO.rewrite < times_n_SO.
 139            rewrite < times_n_SO.rewrite < times_n_SO.
 140            apply le_plus
 141             [unfold M.apply le_n
 142             |apply le_plus_l.unfold M.
 143              change in \vdash (? ? %) with (fact (S(2*m))/(fact (S m)*(fact ((2*m)-m)))).
 144              simplify in \vdash (? ? (? ? (? ? (? (? % ?))))).
 145              rewrite < plus_n_O.rewrite < minus_plus_m_m.
 146              rewrite < sym_times in \vdash (? ? (? ? %)).
 147              change in \vdash (? % ?) with (fact (S(2*m))/(fact m*(fact (S(2*m)-m)))).
 148              simplify in \vdash (? (? ? (? ? (? (? (? %) ?)))) ?).
 149              rewrite < plus_n_O.change in \vdash (? (? ? (? ? (? (? % ?)))) ?) with (S m + m).
 150              rewrite < minus_plus_m_m.
 151              apply le_n
 152             ]
 153           |apply le_O_n
 154           |intros.
 155            elim (eqb i m);elim (eqb i (S m));reflexivity
 156           ]
 157         |apply le_S_S.apply le_S_S.
 158          apply le_times_n.
 159          apply le_n_Sn
 160         |rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S m))).
 161          rewrite > (not_eq_to_eqb_false (S m) m)
 162           [reflexivity
 163           |intro.apply (not_eq_n_Sn m).
 164            apply sym_eq.assumption
 165           ]
 166         ]
 167       |apply le_S.apply le_S_S.
 168        apply le_times_n.
 169        apply le_n_Sn
 170       |rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S m))).
 171        reflexivity
 172       ]
 173     |rewrite > (bool_to_nat_to_eq_sigma_p (S(S(2*m))) ? (\lambda k.true) ?
 174       (\lambda k.bool_to_nat (eqb k m\lor eqb k (S m))*(bc (S (2*m)) k*(1)\sup(S (2*m)-k)*(1)\sup(k))))
 175      in \vdash (? % ?)
 176       [apply lt_sigma_p
 177         [intros.elim (eqb i m\lor eqb i (S m))
 178           [rewrite > sym_times.rewrite < times_n_SO.apply le_n
 179           |apply le_O_n
 180           ]
 181         |apply (ex_intro ? ? O).
 182          split
 183           [split[apply lt_O_S|reflexivity]
 184           |rewrite > (not_eq_to_eqb_false ? ? (not_eq_O_S m)).
 185            rewrite > (not_eq_to_eqb_false ? ? (lt_to_not_eq ? ? H)).
 186            simplify in \vdash (? % ?).
 187            rewrite < exp_SO_n.rewrite < exp_SO_n.
 188            rewrite > bc_n_O.simplify.
 189            apply le_n
 190           ]
 191         ]
 192       |intros.rewrite > sym_times in \vdash (? ? ? %).
 193        rewrite < times_n_SO.
 194        reflexivity
 195       ]
 196     ]
 197   ]
 198 qed.
 199
 200
 201 (*
 202 theorem exp_Sn_SSO: \forall n. exp (S n) 2 = S((exp n 2) + 2*n).
 203 intros.simplify.
 204 rewrite < times_n_SO.
 205 rewrite < plus_n_O.
 206 rewrite < sym_times.simplify.
 207 rewrite < assoc_plus.
 208 rewrite < sym_plus.
 209 reflexivity.
 210 qed. *)
 211 *)