From 9475bcd66c14f82b84c27d4c759aa94783ec08d3 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 11 Dec 2007 15:26:48 +0000 Subject: [PATCH] Partial progress. --- helm/software/matita/library/nat/exp.ma | 9 + helm/software/matita/library/nat/log.ma | 11 +- helm/software/matita/library/nat/neper.ma | 230 +++++++++++++++++++++- 3 files changed, 237 insertions(+), 13 deletions(-) diff --git a/helm/software/matita/library/nat/exp.ma b/helm/software/matita/library/nat/exp.ma index c94e713b1..cb64efee2 100644 --- a/helm/software/matita/library/nat/exp.ma +++ b/helm/software/matita/library/nat/exp.ma @@ -153,6 +153,15 @@ apply nat_elim2 ] qed. +theorem lt_exp1: \forall n,m,p:nat. O < p \to n < m \to exp n p < exp m p. +intros. +elim H + [rewrite < exp_n_SO.rewrite < exp_n_SO.assumption + |simplify. + apply lt_times;assumption + ] +qed. + theorem le_exp_to_le: \forall a,n,m. S O < a \to exp a n \le exp a m \to n \le m. intro. diff --git a/helm/software/matita/library/nat/log.ma b/helm/software/matita/library/nat/log.ma index d4e1b2bd9..3c4f0ad05 100644 --- a/helm/software/matita/library/nat/log.ma +++ b/helm/software/matita/library/nat/log.ma @@ -350,6 +350,7 @@ intros.apply (lt_O_n_elim ? H).intros. simplify.reflexivity. qed. +(* theorem tech1: \forall n,i.O < n \to (exp (S n) (S(S i)))/(exp n (S i)) \le ((exp n i) + (exp (S n) (S i)))/(exp n i). intros. @@ -358,9 +359,8 @@ rewrite < eq_div_div_div_times [apply monotonic_div [apply lt_O_exp.assumption |apply le_S_S_to_le. - apply lt_times_to_lt_div - [assumption - |change in ⊢ (? % ?) with ((exp (S n) (S i)) + n*(exp (S n) (S i))). + apply lt_times_to_lt_div. + change in ⊢ (? % ?) with ((exp (S n) (S i)) + n*(exp (S n) (S i))). |apply (trans_le ? ((n)\sup(i)*(S n)\sup(S i)/(n)\sup(S i))) @@ -369,15 +369,13 @@ rewrite < eq_div_div_div_times |apply le_times_to_le_div2 [apply lt_O_exp.assumption |simplify. -*) -(* falso + theorem tech1: \forall a,b,n,m.O < m \to n/m \le b \to (a*n)/m \le a*b. intros. apply le_times_to_le_div2 [assumption | -*) theorem tech2: \forall n,m. O < n \to (exp (S n) m) / (exp n m) \le (n + m)/n. @@ -409,3 +407,4 @@ elim n |rewrite > true_to_sigma_p_Sn [apply (trans_le ? (m/n1+(log p (exp n1 m)))) [ +*) \ No newline at end of file diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma index fe9b7ac1a..644db0630 100644 --- a/helm/software/matita/library/nat/neper.ma +++ b/helm/software/matita/library/nat/neper.ma @@ -17,6 +17,7 @@ set "baseuri" "cic:/matita/nat/neper". include "nat/iteration2.ma". include "nat/div_and_mod_diseq.ma". include "nat/binomial.ma". +include "nat/log.ma". theorem sigma_p_div_exp: \forall n,m. sigma_p n (\lambda i.true) (\lambda i.m/(exp (S(S O)) i)) \le @@ -211,10 +212,11 @@ intro.elim n ] qed. -theorem le_exp_Sn_n_SSSO: \forall n. (exp (S n) n) \le (S(S(S O)))*(exp n n). -intro. -apply (trans_le ? (sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!))) - [apply le_exp_sigma_p_exp +theorem lt_SO_to_lt_exp_Sn_n_SSSO: \forall n. S O < n \to +(exp (S n) n) < (S(S(S O)))*(exp n n). +intros. +apply (lt_to_le_to_lt ? (sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!))) + [apply lt_exp_sigma_p_exp.assumption |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) (pred i))))) [apply le_sigma_p.intros. apply le_times_to_le_div @@ -248,9 +250,223 @@ apply (trans_le ? (sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!))) ] ] ] -qed. - - +qed. +theorem lt_exp_Sn_n_SSSO: \forall n. +(exp (S n) n) < (S(S(S O)))*(exp n n). +intro.cases n;intros + [simplify.apply le_S.apply le_n + |cases n1;intros + [simplify.apply le_n + |apply lt_SO_to_lt_exp_Sn_n_SSSO. + apply le_S_S.apply le_S_S.apply le_O_n + ] + ] +qed. + +theorem lt_exp_Sn_m_SSSO: \forall n,m. O < m \to +divides n m \to +(exp (S n) m) < (exp (S(S(S O))) (m/n)) *(exp n m). +intros. +elim H1.rewrite > H2. +rewrite < exp_exp_times. +rewrite < exp_exp_times. +rewrite > sym_times in ⊢ (? ? (? (? ? (? % ?)) ?)). +rewrite > lt_O_to_div_times + [rewrite > times_exp. + apply lt_exp1 + [apply (O_lt_times_to_O_lt ? n). + rewrite > sym_times. + rewrite < H2. + assumption + |apply lt_exp_Sn_n_SSSO + ] + |apply (O_lt_times_to_O_lt ? n2). + rewrite < H2. + assumption + ] +qed. + +theorem le_log_exp_Sn_log_exp_n: \forall n,m,p. O < m \to S O < p \to +divides n m \to +log p (exp (S n) m) \le S((m/n)*S(log p (S(S(S O))))) + log p (exp n m). +intros. +apply (trans_le ? (log p (((S(S(S O))))\sup(m/n)*((n)\sup(m))))) + [apply le_log + [assumption + |apply lt_O_exp. + apply lt_O_S + |apply lt_to_le. + apply lt_exp_Sn_m_SSSO;assumption + ] + |apply (trans_le ? (S(log p (exp (S(S(S O))) (m/n)) + log p (exp n m)))) + [apply log_times. + assumption + |change in ⊢ (? ? %) with (S (m/n*S (log p (S(S(S O))))+log p ((n)\sup(m)))). + apply le_S_S. + apply le_plus_l. + apply log_exp1. + assumption + ] + ] +qed. + +theorem le_log_exp_Sn_log_exp_n: \forall a,b,n,p. S O < p \to +a \le b \to b \le n \to +log p (exp b n!) - log p (exp a n!) \le +sigma_p b (\lambda i.leb a i) (\lambda i.S((n!/i)*S(log p (S(S(S O)))))). +intros 6. +elim b + [simplify. + apply (lt_O_n_elim ? (lt_O_fact n)).intro. + apply le_n. + |apply (bool_elim ? (leb a n1));intro + [rewrite > true_to_sigma_p_Sn + [apply (trans_le ? (S (n!/n1*S (log p (S(S(S O)))))+(log p ((n1)\sup(n!))-log p ((a)\sup(n!))))) + [rewrite > sym_plus. + rewrite > plus_minus + [apply le_plus_to_minus_r. + rewrite < plus_minus_m_m + [rewrite > sym_plus. + apply le_log_exp_Sn_log_exp_n + [apply lt_O_fact + |assumption + | + +theorem le_log_exp_Sn_log_exp_n: \forall n,m,a,p. O < m \to S O < p \to +divides n m \to +log p (exp n m) - log p (exp a m) \le +sigma_p (S n) (\lambda i.leb (S a) i) (\lambda i.S((m/i)*S(log p (S(S(S O)))))). +intros. +elim n + [rewrite > false_to_sigma_p_Sn. + simplify. + apply (lt_O_n_elim ? H).intro. + simplify.apply le_O_n + |apply (bool_elim ? (leb a n1));intro + [rewrite > true_to_sigma_p_Sn + [apply (trans_le ? (S (m/S n1*S (log p (S(S(S O)))))+(log p ((n1)\sup(m))-log p ((a)\sup(m))))) + [rewrite > sym_plus. + rewrite > plus_minus + [apply le_plus_to_minus_r. + rewrite < plus_minus_m_m + [rewrite > sym_plus. + apply le_log_exp_Sn_log_exp_n. + + +(* a generalization +theorem le_exp_sigma_p_exp_m: \forall m,n. (exp (S m) n) \le +sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)). +intros. +rewrite > exp_S_sigma_p. +apply le_sigma_p. +intros.unfold bc. +apply (trans_le ? ((exp m (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 + ] + |apply le_times_div_div_times. + apply lt_O_fact + ] +qed. +theorem lt_exp_sigma_p_exp_m: \forall m,n. S O < n \to +(exp (S m) n) < +sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)). +intros. +rewrite > exp_S_sigma_p. +apply lt_sigma_p + [intros.unfold bc. + apply (trans_le ? ((exp m (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 + ] + |apply le_times_div_div_times. + apply lt_O_fact + ] + |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. + rewrite < plus_n_O. + apply le_fact_exp1. + assumption + ] + ] + ] +qed. +theorem lt_SO_to_lt_exp_Sn_n_SSSO_bof: \forall m,n. S O < n \to +(exp (S m) n) < (S(S(S O)))*(exp m n). +intros. +apply (lt_to_le_to_lt ? (sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)))) + [apply lt_exp_sigma_p_exp_m.assumption + |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) (pred i))))) + [apply le_sigma_p.intros. + apply le_times_to_le_div + [apply lt_O_exp. + apply lt_O_S + |apply (trans_le ? ((S(S O))\sup (pred i)* n \sup n/i!)) + [apply le_times_div_div_times. + apply lt_O_fact + |apply le_times_to_le_div2 + [apply lt_O_fact + |rewrite < sym_times. + apply le_times_r. + apply le_exp_SSO_fact + ] + ] + ] + |rewrite > eq_sigma_p_pred + [rewrite > div_SO. + rewrite > sym_plus. + change in ⊢ (? ? %) with ((exp n n)+(S(S O)*(exp n n))). + apply le_plus_r. + apply (trans_le ? (((S(S O))*(exp n n)*(exp (S(S O)) n) - (S(S O))*(exp n n))/(exp (S(S O)) n))) + [apply sigma_p_div_exp + |apply le_times_to_le_div2 + [apply lt_O_exp. + apply lt_O_S. + |apply le_minus_m + ] + ] + |reflexivity + ] + ] + ] +qed. +*) \ No newline at end of file -- 2.39.2