From a91366d1db62090a7b665f99aa5abdd5d2449799 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 7 Dec 2007 11:41:49 +0000 Subject: [PATCH] Binomial coefficients and costant e. --- helm/software/matita/library/nat/binomial.ma | 88 ++++++++++++++++++++ helm/software/matita/library/nat/neper.ma | 67 +++++++++++++++ 2 files changed, 155 insertions(+) create mode 100644 helm/software/matita/library/nat/binomial.ma create mode 100644 helm/software/matita/library/nat/neper.ma diff --git a/helm/software/matita/library/nat/binomial.ma b/helm/software/matita/library/nat/binomial.ma new file mode 100644 index 000000000..e1b955fa8 --- /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 index 000000000..e618ec568 --- /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 -- 2.39.2