From 1f214ad28b490ed66602eb2d80359c01ba55ee05 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 10 Dec 2007 08:43:07 +0000 Subject: [PATCH] Main inequalities for e. --- helm/software/matita/library/nat/binomial.ma | 13 ++ helm/software/matita/library/nat/exp.ma | 7 + .../software/matita/library/nat/iteration2.ma | 144 ++++++++++++++++++ helm/software/matita/library/nat/neper.ma | 138 ++++++++++++++++- 4 files changed, 300 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/library/nat/binomial.ma b/helm/software/matita/library/nat/binomial.ma index 4434f769b..950576148 100644 --- a/helm/software/matita/library/nat/binomial.ma +++ b/helm/software/matita/library/nat/binomial.ma @@ -213,4 +213,17 @@ intros.elim n |reflexivity]] |reflexivity] |reflexivity]] +qed. + +theorem exp_S_sigma_p:\forall a,n. +exp (S a) n = sigma_p (S n) (\lambda k.true) (\lambda k.(bc n k)*(exp a (n-k))). +intros. +rewrite > plus_n_SO. +rewrite > exp_plus_sigma_p. +apply eq_sigma_p;intros + [reflexivity + |rewrite < exp_SO_n. + rewrite < times_n_SO. + reflexivity + ] qed. \ No newline at end of file diff --git a/helm/software/matita/library/nat/exp.ma b/helm/software/matita/library/nat/exp.ma index 74a3be71f..c94e713b1 100644 --- a/helm/software/matita/library/nat/exp.ma +++ b/helm/software/matita/library/nat/exp.ma @@ -40,6 +40,13 @@ theorem exp_n_SO : \forall n:nat. n = n \sup (S O). intro.simplify.rewrite < times_n_SO.reflexivity. qed. +theorem exp_SO_n : \forall n:nat. S O = (S O) \sup n. +intro.elim n + [reflexivity + |simplify.rewrite < plus_n_O.assumption + ] +qed. + theorem exp_SSO: \forall n. exp n (S(S O)) = n*n. intro.simplify. rewrite < times_n_SO. diff --git a/helm/software/matita/library/nat/iteration2.ma b/helm/software/matita/library/nat/iteration2.ma index 0230362e7..ea306f455 100644 --- a/helm/software/matita/library/nat/iteration2.ma +++ b/helm/software/matita/library/nat/iteration2.ma @@ -191,7 +191,151 @@ apply (eq_iter_p_gen_gh nat O plus ? ? ? g h h1 n n1 p1 p2) ] qed. +(* monotonicity *) +theorem le_sigma_p: +\forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat. +(\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to +sigma_p n p g1 \le sigma_p n p g2. +intros. +generalize in match H. +elim n + [apply le_n. + |apply (bool_elim ? (p n1));intros + [rewrite > true_to_sigma_p_Sn + [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %) + [apply le_plus + [apply H2[apply le_n|assumption] + |apply H1. + intros. + apply H2[apply le_S.assumption|assumption] + ] + |assumption + ] + |assumption + ] + |rewrite > false_to_sigma_p_Sn + [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %) + [apply H1. + intros. + apply H2[apply le_S.assumption|assumption] + |assumption + ] + |assumption + ] + ] + ] +qed. +theorem lt_sigma_p: +\forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat. +(\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to +(\exists i. i < n \and (p i = true) \and (g1 i < g2 i)) \to +sigma_p n p g1 < sigma_p n p g2. +intros 4. +elim n + [elim H1.clear H1. + elim H2.clear H2. + elim H1.clear H1. + apply False_ind. + apply (lt_to_not_le ? ? H2). + apply le_O_n + |apply (bool_elim ? (p n1));intros + [apply (bool_elim ? (leb (S (g1 n1)) (g2 n1)));intros + [rewrite > true_to_sigma_p_Sn + [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %) + [change with + (S (g1 n1)+sigma_p n1 p g1 \le g2 n1+sigma_p n1 p g2). + apply le_plus + [apply leb_true_to_le.assumption + |apply le_sigma_p.intros. + apply H1 + [apply lt_to_le.apply le_S_S.assumption + |assumption + ] + ] + |assumption + ] + |assumption + ] + |rewrite > true_to_sigma_p_Sn + [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %) + [unfold lt. + rewrite > plus_n_Sm. + apply le_plus + [apply H1 + [apply le_n + |assumption + ] + |apply H + [intros.apply H1 + [apply lt_to_le.apply le_S_S.assumption + |assumption + ] + |elim H2.clear H2. + elim H5.clear H5. + elim H2.clear H2. + apply (ex_intro ? ? a). + split + [split + [elim (le_to_or_lt_eq a n1) + [assumption + |absurd (g1 a < g2 a) + [assumption + |apply leb_false_to_not_le. + rewrite > H2. + assumption + ] + |apply le_S_S_to_le. + assumption + ] + |assumption + ] + |assumption + ] + ] + ] + |assumption + ] + |assumption + ] + ] + |rewrite > false_to_sigma_p_Sn + [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %) + [apply H + [intros.apply H1 + [apply lt_to_le.apply le_S_S.assumption + |assumption + ] + |elim H2.clear H2. + elim H4.clear H4. + elim H2.clear H2. + apply (ex_intro ? ? a). + split + [split + [elim (le_to_or_lt_eq a n1) + [assumption + |apply False_ind. + apply not_eq_true_false. + rewrite < H6. + rewrite < H3. + rewrite < H2. + reflexivity + |apply le_S_S_to_le. + assumption + ] + |assumption + ] + |assumption + ] + ] + |assumption + ] + |assumption + ] + ] + ] +qed. + theorem sigma_p_divides: \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to \forall g: nat \to nat. diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma index e618ec568..f3db405d4 100644 --- a/helm/software/matita/library/nat/neper.ma +++ b/helm/software/matita/library/nat/neper.ma @@ -16,8 +16,9 @@ set "baseuri" "cic:/matita/nat/neper". include "nat/iteration2.ma". include "nat/div_and_mod_diseq.ma". +include "nat/binomial.ma". -theorem boh: \forall n,m. +theorem sigma_p_div_exp: \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. @@ -64,4 +65,137 @@ elim n ] ] qed. - \ No newline at end of file + +theorem le_fact_exp: \forall i,m. i \le m \to m!≤ m \sup i*(m-i)!. +intro.elim i + [rewrite < minus_n_O. + simplify.rewrite < plus_n_O. + apply le_n + |simplify. + apply (trans_le ? ((m)\sup(n)*(m-n)!)) + [apply H. + apply lt_to_le.assumption + |rewrite > sym_times in ⊢ (? ? (? % ?)). + rewrite > assoc_times. + apply le_times_r. + generalize in match H1. + cases m;intro + [apply False_ind. + apply (lt_to_not_le ? ? H2). + apply le_O_n + |rewrite > minus_Sn_m. + simplify. + apply le_plus_r. + apply le_times_l. + apply le_minus_m. + apply le_S_S_to_le. + assumption + ] + ] + ] +qed. + +theorem le_fact_exp1: \forall n. S O < n \to (S(S O))*n!≤ n \sup n. +intros.elim H + [apply le_n + |change with ((S(S O))*((S n1)*(fact n1)) \le (S n1)*(exp (S n1) n1)). + rewrite < assoc_times. + rewrite < sym_times in ⊢ (? (? % ?) ?). + rewrite > assoc_times. + apply le_times_r. + apply (trans_le ? (exp n1 n1)) + [assumption + |apply monotonic_exp1. + apply le_n_Sn + ] + ] +qed. + +theorem le_exp_sigma_p_exp: \forall n. (exp (S n) n) \le +sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!). +intro. +rewrite > exp_S_sigma_p. +apply le_sigma_p. +intros.unfold bc. +apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!))) + [rewrite > sym_times. + apply le_times_r. + rewrite > sym_times. + rewrite < eq_div_div_div_times + [apply monotonic_div + [apply lt_O_fact + |apply le_times_to_le_div2 + [apply lt_O_fact + |apply le_fact_exp. + apply le_S_S_to_le. + assumption + ] + ] + |apply lt_O_fact + |apply lt_O_fact + ] + |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?)) + [rewrite > exp_plus_times. + apply le_times_div_div_times. + apply lt_O_fact + |apply le_S_S_to_le. + assumption + ] + ] +qed. + +theorem lt_exp_sigma_p_exp: \forall n. S O < n \to +(exp (S n) n) < +sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!). +intros. +rewrite > exp_S_sigma_p. +apply lt_sigma_p + [intros.unfold bc. + apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!))) + [rewrite > sym_times. + apply le_times_r. + rewrite > sym_times. + rewrite < eq_div_div_div_times + [apply monotonic_div + [apply lt_O_fact + |apply le_times_to_le_div2 + [apply lt_O_fact + |apply le_fact_exp. + apply le_S_S_to_le. + assumption + ] + ] + |apply lt_O_fact + |apply lt_O_fact + ] + |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?)) + [rewrite > exp_plus_times. + apply le_times_div_div_times. + apply lt_O_fact + |apply le_S_S_to_le. + assumption + ] + ] + |apply (ex_intro ? ? n). + split + [split + [apply le_n + |reflexivity + ] + |rewrite < minus_n_n. + rewrite > bc_n_n. + simplify.unfold lt. + apply le_times_to_le_div + [apply lt_O_fact + |rewrite > sym_times. + apply le_fact_exp1. + assumption + ] + ] + ] +qed. + + + + + -- 2.39.2