X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fbinomial.ma;h=6b4d3ff52764ff41ee26453c9c26c6206c2ab7b3;hb=cd2f5b59215ea771ac137b9a7b115a05175f45d5;hp=7ab00d4991c23408fc1dc76ec149a4d7f80c86a2;hpb=ddc80515997a3f56085c6234d4db326141e189aa;p=helm.git

diff --git a/matita/matita/lib/arithmetics/binomial.ma b/matita/matita/lib/arithmetics/binomial.ma
index 7ab00d499..6b4d3ff52 100644
--- a/matita/matita/lib/arithmetics/binomial.ma
+++ b/matita/matita/lib/arithmetics/binomial.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "arithmetics/sigma_pi.ma".
 include "arithmetics/primes.ma".
+include "arithmetics/sigma_pi.ma".
 
 (* binomial coefficient *)
 definition bc ≝ λn,k. n!/(k!*(n-k)!).
@@ -23,7 +23,7 @@ theorem bc_n_n: ∀n. bc n n = 1.
 qed.
 
 theorem bc_n_O: ∀n. bc n O = 1.
-#n >bceq <minus_n_O /2/
+#n >bceq <minus_n_O /2 by injective_plus_r/
 qed.
 
 theorem fact_minus: ∀n,k. k < n → 
@@ -44,12 +44,12 @@ theorem bc2 : ∀n.
      cut (m-(m-(S c)) = S c) [@plus_to_minus @plus_minus_m_m //] #eqSc     
      lapply (Hind c (le_S_S_to_le … lec)) #Hc
      lapply (Hind (m - (S c)) ?) [@le_plus_to_minus //] >eqSc #Hmc
-     >(plus_minus_m_m m c) {⊢ (??(??(?%)))} [|@le_S_S_to_le //]
+     >(plus_minus_m_m m c) in ⊢ (??(??(?%))); [|@le_S_S_to_le //]
      >commutative_plus >(distributive_times_plus ? (S c))
      @divides_plus
       [>associative_times >(commutative_times (S c))
        <associative_times @divides_times //
-      |<(fact_minus …ltcm) {⊢ (?(??%)?)}
+      |<(fact_minus …ltcm) in ⊢ (?(??%)?);
        <associative_times @divides_times //
        >commutative_times @Hmc
       ]
@@ -61,21 +61,21 @@ qed.
 theorem bc1: ∀n.∀k. k < n → 
   bc (S n) (S k) = (bc n k) + (bc n (S k)).
 #n #k #ltkn > bceq >(bceq n) >(bceq n (S k))
->(div_times_times ?? (S k)) {⊢ (???(?%?))}
+>(div_times_times ?? (S k)) in ⊢ (???(?%?));
   [|>(times_n_O 0) @lt_times // | //]
->associative_times {⊢ (???(?(??%)?))}
->commutative_times {⊢ (???(?(??(??%))?))}
-<associative_times {⊢ (???(?(??%)?))}
->(div_times_times ?? (n - k)) {⊢ (???(??%))}
+>associative_times in ⊢ (???(?(??%)?));
+>commutative_times in ⊢ (???(?(??(??%))?));
+<associative_times in ⊢ (???(?(??%)?));
+>(div_times_times ?? (n - k)) in ⊢ (???(??%)) ; 
   [|>(times_n_O 0) @lt_times // 
-   |@(le_plus_to_le_r k ??) <plus_minus_m_m /2/]
->associative_times {⊢ (???(??(??%)))}
+   |@(le_plus_to_le_r k ??) <plus_minus_m_m /2 by lt_to_le/]
+>associative_times in ⊢ (???(??(??%)));
 >fact_minus // <plus_div 
   [<distributive_times_plus
-   >commutative_plus {⊢ (???%)} <plus_n_Sm <plus_minus_m_m [|/2/] @refl
+   >commutative_plus in ⊢ (???%); <plus_n_Sm <plus_minus_m_m [|/2 by lt_to_le/] @refl
   |<fact_minus // <associative_times @divides_times // @(bc2 n (S k)) //
   |>associative_times >(commutative_times (S k))
-   <associative_times @divides_times // @bc2 /2/
+   <associative_times @divides_times // @bc2 /2 by lt_to_le/
   |>(times_n_O 0) @lt_times [@(le_1_fact (S k)) | //]
   ]
 qed.
@@ -89,46 +89,105 @@ theorem lt_O_bc: ∀n,m. m ≤ n → O < bc n m.
   ]
 qed. 
 
-(*
 theorem binomial_law:∀a,b,n.
-  (a+b)^n = Σ_{k < S n}((bc n k)*(a^(n-k))*(b^k)).
+  (a+b)^n = ∑_{k < S n}((bc n k)*(a^(n-k))*(b^k)).
 #a #b #n (elim n) //
--n #n #Hind normalize in ⊢ (? ? % ?).
->bigop_Strue // >Hind >distributive_times_plus 
-<(minus_n_n (S n)) <commutative_times <(commutative_times b)
-(* hint??? *)
->(bigop_distr ???? natDop ? a) >(bigop_distr ???? natDop ? b)
->bigop_Strue in ⊢ (??(??%)?) // <associative_plus 
-<commutative_plus in ⊢ (??(? % ?) ?) >associative_plus @eq_f2
+-n #n #Hind normalize in ⊢ (??%?); >commutative_times
+>bigop_Strue // >Hind >distributive_times_plus_r
+<(minus_n_n (S n)) (* <commutative_times <(commutative_times b) *)
+(* da capire *)
+>(bigop_distr ??? 0 (mk_Dop ℕ O plusAC times (λn0:ℕ.sym_eq ℕ O (n0*O) (times_n_O n0))
+    distributive_times_plus) ? a) 
+>(bigop_distr ???? (mk_Dop ℕ O plusAC times (λn0:ℕ.sym_eq ℕ O (n0*O) (times_n_O n0))
+    distributive_times_plus) ? b)
+>bigop_Strue in ⊢ (??(??%)?); // <associative_plus 
+<commutative_plus in ⊢ (??(? % ?) ?); >associative_plus @eq_f2
   [<minus_n_n >bc_n_n >bc_n_n normalize //
-  |>bigop_0 >associative_plus >commutative_plus in ⊢ (??(??%)?) 
-   <associative_plus >bigop_0 // @eq_f2 
-    [>(bigop_op n ??? natACop) @same_bigop //
+  |>(bigop_0 ??? plusA)  >associative_plus >commutative_plus in ⊢ (??(??%)?);
+   <associative_plus >(bigop_0 n ?? plusA) @eq_f2 
+    [cut (∀a,b. plus a b = plusAC a b) [//] #Hplus >Hplus 
+     >(bigop_op n ??? plusAC) @same_bigop //
      #i #ltin #_ <associative_times >(commutative_times b)
-     >(associative_times ?? b) <(distributive_times_plus_r (b^(S i)))
+     >(associative_times ?? b) <Hplus <(distributive_times_plus_r (b^(S i)))
      @eq_f2 // <associative_times >(commutative_times a) 
      >associative_times cut(∀n.a*a^n = a^(S n)) [#n @commutative_times] #H
      >H <minus_Sn_m // <(distributive_times_plus_r (a^(n-i)))
      @eq_f2 // @sym_eq >commutative_plus @bc1 //
-    |>bc_n_O >bc_n_O normalize //
+    |>bc_n_O >bc_n_O normalize // 
     ]
   ]
 qed.
      
 theorem exp_S_sigma_p:∀a,n.
-(S a)^n = Σ_{k < S n}((bc n k)*a^(n-k)).
+  (S a)^n = ∑_{k < S n}((bc n k)*a^(n-k)).
 #a #n cut (S a = a + 1) // #H >H
 >binomial_law @same_bigop //
 qed.
 
-(*
-theorem exp_Sn_SSO: \forall n. exp (S n) 2 = S((exp n 2) + 2*n).
-intros.simplify.
-rewrite < times_n_SO.
-rewrite < plus_n_O.
-rewrite < sym_times.simplify.
-rewrite < assoc_plus.
-rewrite < sym_plus.
-reflexivity.
-qed. *)
-*)
\ No newline at end of file
+(************ mid value *************)
+lemma eqb_sym: ∀a,b. eqb a b = eqb b a.
+#a #b cases (true_or_false (eqb a b)) #Hab
+  [>(eqb_true_to_eq … Hab) // 
+  |>Hab @sym_eq @not_eq_to_eqb_false 
+   @(not_to_not … (eqb_false_to_not_eq … Hab)) //
+  ] 
+qed-.
+
+definition M ≝ λm.bc (S(2*m)) m.
+
+lemma Mdef : ∀m. M m = bc (S(2*m)) m. 
+// qed.
+
+theorem lt_M: ∀m. O < m → M m < exp 2 (2*m).
+#m #posm  @(lt_times_n_to_lt_l 2)
+cut (∀a,b. a^(S b) = a^b*a) [//] #expS <expS  
+cut (2 = 1+1) [//] #H2 >H2 in ⊢ (??(?%?));
+>binomial_law 
+@(le_to_lt_to_lt ? 
+  (∑_{k < S (S (2*m)) | orb (eqb k m) (eqb k (S m))}
+         (bc (S (2*m)) k*1^(S (2*m)-k)*1^k)))
+  [>(bigop_diff ??? plusAC … m)
+    [>(bigop_diff ??? plusAC … (S m))
+      [<(pad_bigop1 … (S(S(2*m))) 0)
+        [cut (∀a,b. plus a b = plusAC a b) [//] #Hplus <Hplus <Hplus
+         whd in ⊢ (? ? (? ? (? ? %)));
+         cut (∀a. 2*a = a + a) [//] #H2a >commutative_times >H2a
+         <exp_1_n <exp_1_n <exp_1_n <exp_1_n
+         <times_n_1 <times_n_1 <times_n_1 <times_n_1 
+         @le_plus
+          [@le_n
+          |>Mdef <plus_n_O >bceq >bceq 
+           cut (∀a,b.S a - (S b) = a -b) [//] #Hminus >Hminus 
+           normalize in ⊢ (??(??(??(?(?%?))))); <plus_n_O <minus_plus_m_m
+           <commutative_times in ⊢ (??(??%)); 
+           cut (S (2*m)-m = S m) 
+            [>H2a >plus_n_Sm >commutative_plus <minus_plus_m_m //] 
+           #Hcut >Hcut //
+          ]
+        |#i #_ #_ >(eqb_sym i m) >(eqb_sym i (S m))
+         cases (eqb m i) cases (eqb (S m) i) //
+        |@le_O_n
+        ]
+      |>(eqb_sym (S m) m) >(eq_to_eqb_true ? ? (refl ? (S m)))
+       >(not_eq_to_eqb_false m (S m)) 
+        [// |@(not_to_not … (not_eq_n_Sn m)) //]
+      |@le_S_S @le_S_S // 
+      ]
+    |>(eq_to_eqb_true ?? (refl ? m)) //
+    |@le_S @le_S_S //
+    ]
+  |@lt_sigma_p
+    [//
+    |#i #lti #Hi @le_n
+    |%{0} %
+      [@lt_O_S
+      |%2 % 
+        [% // >(not_eq_to_eqb_false 0 (S m)) //
+         >(not_eq_to_eqb_false 0 m) // @lt_to_not_eq //
+        |>bc_n_O <exp_1_n <exp_1_n @le_n
+        ]
+      ]
+    ]
+  ]
+qed.
+