Binomial coefficients and costant e.

diff --git a/helm/software/matita/library/nat/binomial.ma b/helm/software/matita/library/nat/binomial.ma
new file mode 100644 (file)
index 0000000..e1b955f
--- /dev/null
+++ b/helm/software/matita/library/nat/binomial.ma
@@ -0,0 +1,88 @@
+(**************************************************************************)
+(*       __                                                               *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/binomial".
+
+include "nat/iteration2.ma".
+include "nat/factorial2.ma".
+
+definition bc \def \lambda n,k. n!/(k!*(n-k)!).
+
+theorem bc_n_n: \forall n. bc n n = S O.
+intro.unfold bc.
+rewrite < minus_n_n.
+simplify in ⊢ (? ? (? ? (? ? %)) ?).
+rewrite < times_n_SO.
+apply div_n_n.
+apply lt_O_fact.
+qed.
+
+theorem bc_n_O: \forall n. bc n O = S O.
+intro.unfold bc.
+rewrite < minus_n_O.
+simplify in ⊢ (? ? (? ? %) ?).
+rewrite < plus_n_O.
+apply div_n_n.
+apply lt_O_fact.
+qed.
+
+theorem fact_minus: \forall n,k. k < n \to 
+(n-k)*(n - S k)! = (n - k)!.
+intros 2.cases n
+  [intro.apply False_ind.
+   apply (lt_to_not_le ? ? H).
+   apply le_O_n
+  |intros.
+   rewrite > minus_Sn_m.
+   reflexivity.
+   apply le_S_S_to_le.
+   assumption
+  ]
+qed.
+
+theorem bc1: \forall n.
+(\forall i. i < n \to divides (i!*(n-i)!) n!) \to
+\forall k. k < n \to 
+bc (S n) (S k) = (bc n k) + (bc n (S k)). 
+intros.unfold bc.
+rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (S k)) in ⊢ (? ? ? (? % ?))
+  [rewrite > sym_times in ⊢ (? ? ? (? (? ? %) ?)). 
+   rewrite < assoc_times in ⊢ (? ? ? (? (? ? %) ?)).
+   rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (n - k)) in ⊢ (? ? ? (? ? %))
+    [rewrite > assoc_times in ⊢ (? ? ? (? ? (? ? %))).
+     rewrite > sym_times in ⊢ (? ? ? (? ? (? ? (? ? %)))).
+     rewrite > fact_minus
+      [rewrite < eq_div_plus
+        [rewrite < distr_times_plus.
+         simplify in ⊢ (? ? ? (? (? ? %) ?)).
+         rewrite > sym_plus in ⊢ (? ? ? (? (? ? (? %)) ?)).
+         rewrite < plus_minus_m_m
+          [rewrite > sym_times in ⊢ (? ? ? (? % ?)).
+           reflexivity
+          |apply lt_to_le.
+           assumption
+          ]
+        |rewrite > (times_n_O O).
+         apply lt_times;apply lt_O_fact
+        |apply H.
+    
+    
+theorem exp_plus_sigma_p:\forall a,b,n.
+exp (a+b) n = sigma_p (S n) (\lambda k.true) 
+  (\lambda k.(bc n k)*(exp a (n-k))*(exp b k)).
+intros.elim n
+  [simplify.reflexivity
+  |simplify in ⊢ (? ? % ?).
+   rewrite > true_to_sigma_p_Sn
+    [rewrite <
\ No newline at end of file

diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma
new file mode 100644 (file)
index 0000000..e618ec5
--- /dev/null
+++ b/helm/software/matita/library/nat/neper.ma
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(*       __                                                               *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/neper".
+
+include "nat/iteration2.ma".
+include "nat/div_and_mod_diseq.ma".
+
+theorem boh: \forall n,m.
+sigma_p n (\lambda i.true) (\lambda i.m/(exp (S(S O)) i)) \le 
+((S(S O))*m*(exp (S(S O)) n) - (S(S O))*m)/(exp (S(S O)) n).
+intros.
+elim n
+  [apply le_O_n.
+  |rewrite > true_to_sigma_p_Sn
+    [apply (trans_le ? (m/(S(S O))\sup(n1)+((S(S O))*m*(S(S O))\sup(n1)-(S(S O))*m)/(S(S O))\sup(n1)))
+      [apply le_plus_r.assumption
+      |rewrite > assoc_times in ⊢ (? ? (? (? % ?) ?)).
+       rewrite < distr_times_minus.
+       change in ⊢ (? ? (? ? %)) with ((S(S O))*(exp (S(S O)) n1)).
+       rewrite > sym_times in ⊢ (? ? (? % ?)).
+       rewrite > sym_times in ⊢ (? ? (? ? %)).
+       rewrite < lt_to_lt_to_eq_div_div_times_times
+        [apply (trans_le ? ((m+((S(S O))*m*((S(S O)))\sup(n1)-(S(S O))*m))/((S(S O)))\sup(n1)))
+          [apply le_plus_div.
+           apply lt_O_exp.
+           apply lt_O_S
+          |change in ⊢ (? (? (? ? (? ? %)) ?) ?) with (m + (m +O)).
+           rewrite < plus_n_O.
+           rewrite < eq_minus_minus_minus_plus.
+           rewrite > sym_plus.
+           rewrite > sym_times in ⊢ (? (? (? (? (? (? % ?) ?) ?) ?) ?) ?).
+           rewrite > assoc_times.
+           rewrite < plus_minus_m_m
+            [apply le_n
+            |apply le_plus_to_minus_r.
+             rewrite > plus_n_O in ⊢ (? (? ? %) ?).
+             change in ⊢ (? % ?) with ((S(S O))*m). 
+             rewrite > sym_times.
+             apply le_times_r.
+             rewrite > times_n_SO in ⊢ (? % ?).
+             apply le_times_r.
+             apply lt_O_exp.
+             apply lt_O_S
+            ]
+          ]
+        |apply lt_O_S
+        |apply lt_O_exp.
+         apply lt_O_S
+        ]
+      ]
+    |reflexivity
+    ]
+  ]
+qed.
+   
\ No newline at end of file