]> matita.cs.unibo.it Git - helm.git/blob - weblib/arithmetics/binomial.ma
- support for atomic arities and candidates of reducibility started
[helm.git] / 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