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.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "arithmetics/primes.ma".
13 include "arithmetics/sigma_pi.ma".
15 (* binomial coefficient *)
16 definition bc ≝ λn,k. n!/(k!*(n-k)!).
18 lemma bceq :∀n,k. bc n k = n!/(k!*(n-k)!).
21 theorem bc_n_n: ∀n. bc n n = 1.
22 #n >bceq <minus_n_n <times_n_1 @div_n_n //
25 theorem bc_n_O: ∀n. bc n O = 1.
26 #n >bceq <minus_n_O /2 by injective_plus_r/
29 theorem fact_minus: ∀n,k. k < n →
30 (n - S k)!*(n-k) = (n - k)!.
33 |#l #ltl >(minus_Sn_m k) [// |@le_S_S_to_le //]
38 ∀k. k ≤n → k!*(n-k)! ∣ 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))
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))
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
56 |#eqcm >eqcm <minus_n_n <times_n_1 //
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)) | //]
83 theorem lt_O_bc: ∀n,m. m ≤ n → O < bc n m.
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/
92 theorem binomial_law:∀a,b,n.
93 (a+b)^n = ∑_{k < S n}((bc n k)*(a^(n-k))*(b^k)).
95 -n #n #Hind normalize in ⊢ (??%?); >commutative_times
96 >bigop_Strue // >Hind >distributive_times_plus_r
97 <(minus_n_n (S n)) (* <commutative_times <(commutative_times b) *)
99 >(bigop_distr ??? 0 (mk_Dop ℕ O plusAC times (λn0:ℕ.sym_eq ℕ O (n0*O) (times_n_O n0))
100 distributive_times_plus) ? a)
101 >(bigop_distr ???? (mk_Dop ℕ O plusAC times (λn0:ℕ.sym_eq ℕ O (n0*O) (times_n_O n0))
102 distributive_times_plus) ? b)
103 >bigop_Strue in ⊢ (??(??%)?); // <associative_plus
104 <commutative_plus in ⊢ (??(? % ?) ?); >associative_plus @eq_f2
105 [<minus_n_n >bc_n_n >bc_n_n normalize //
106 |>bigop_0 >associative_plus >commutative_plus in ⊢ (??(??%)?);
107 <associative_plus >(bigop_0 n ?? plusA) @eq_f2
108 [cut (∀a,b. plus a b = plusAC a b) [//] #Hplus >Hplus
109 >(bigop_op n ??? plusAC) @same_bigop //
110 #i #ltin #_ <associative_times >(commutative_times b)
111 >(associative_times ?? b) <Hplus <(distributive_times_plus_r (b^(S i)))
112 @eq_f2 // <associative_times >(commutative_times a)
113 >associative_times cut(∀n.a*a^n = a^(S n)) [#n @commutative_times] #H
114 >H <minus_Sn_m // <(distributive_times_plus_r (a^(n-i)))
115 @eq_f2 // @sym_eq >commutative_plus @bc1 //
116 |>bc_n_O >bc_n_O normalize //
121 theorem exp_S_sigma_p:∀a,n.
122 (S a)^n = ∑_{k < S n}((bc n k)*a^(n-k)).
123 #a #n cut (S a = a + 1) // #H >H
124 >binomial_law @same_bigop //
127 (************ mid value *************)
128 lemma eqb_sym: ∀a,b. eqb a b = eqb b a.
129 #a #b cases (true_or_false (eqb a b)) #Hab
130 [>(eqb_true_to_eq … Hab) //
131 |>Hab @sym_eq @not_eq_to_eqb_false
132 @(not_to_not … (eqb_false_to_not_eq … Hab)) //
136 definition M ≝ λm.bc (S(2*m)) m.
138 lemma Mdef : ∀m. M m = bc (S(2*m)) m.
141 theorem lt_M: ∀m. O < m → M m < exp 2 (2*m).
142 #m #posm @(lt_times_n_to_lt_l 2)
143 cut (∀a,b. a^(S b) = a^b*a) [//] #expS <expS
144 cut (2 = 1+1) [//] #H2 >H2 in ⊢ (??(?%?));
147 (∑_{k < S (S (2*m)) | orb (eqb k m) (eqb k (S m))}
148 (bc (S (2*m)) k*1^(S (2*m)-k)*1^k)))
149 [>(bigop_diff ??? plusAC … m)
150 [>(bigop_diff ??? plusAC … (S m))
151 [<(pad_bigop1 … (S(S(2*m))) 0)
152 [cut (∀a,b. plus a b = plusAC a b) [//] #Hplus <Hplus <Hplus
153 whd in ⊢ (? ? (? ? (? ? %)));
154 cut (∀a. 2*a = a + a) [//] #H2a >commutative_times >H2a
155 <exp_1_n <exp_1_n <exp_1_n <exp_1_n
156 <times_n_1 <times_n_1 <times_n_1 <times_n_1
159 |>Mdef <plus_n_O >bceq >bceq
160 cut (∀a,b.S a - (S b) = a -b) [//] #Hminus >Hminus
161 normalize in ⊢ (??(??(??(?(?%?))))); <plus_n_O <minus_plus_m_m
162 <commutative_times in ⊢ (??(??%));
163 cut (S (2*m)-m = S m)
164 [>H2a >plus_n_Sm >commutative_plus <minus_plus_m_m //]
167 |#i #_ #_ >(eqb_sym i m) >(eqb_sym i (S m))
168 cases (eqb m i) cases (eqb (S m) i) //
171 |>(eqb_sym (S m) m) >(eq_to_eqb_true ? ? (refl ? (S m)))
172 >(not_eq_to_eqb_false m (S m))
173 [// |@(not_to_not … (not_eq_n_Sn m)) //]
176 |>(eq_to_eqb_true ?? (refl ? m)) //
185 [% // >(not_eq_to_eqb_false 0 (S m)) //
186 >(not_eq_to_eqb_false 0 m) // @lt_to_not_eq //
187 |>bc_n_O <exp_1_n <exp_1_n @le_n