From 7180662b4d33015e3cbc12a381f0cfc8839de697 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Mon, 17 Dec 2007 21:31:35 +0000 Subject: [PATCH] upper bound for logarithmic summation --- helm/software/matita/library/nat/exp.ma | 5 ++ helm/software/matita/library/nat/neper.ma | 79 ++++++++++++++++++++++- 2 files changed, 83 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/library/nat/exp.ma b/helm/software/matita/library/nat/exp.ma index cb64efee2..25c81c069 100644 --- a/helm/software/matita/library/nat/exp.ma +++ b/helm/software/matita/library/nat/exp.ma @@ -186,6 +186,11 @@ apply nat_elim2;intros ] qed. +theorem le_exp_to_le1 : \forall n,m,p.O < p \to exp n p \leq exp m p \to n \leq m. +intros;apply not_lt_to_le;intro;apply (lt_to_not_le ? ? ? H1); +apply lt_exp1;assumption. +qed. + theorem lt_exp_to_lt: \forall a,n,m. S O < a \to exp a n < exp a m \to n < m. intros. diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma index df70accbc..9378bd8de 100644 --- a/helm/software/matita/library/nat/neper.ma +++ b/helm/software/matita/library/nat/neper.ma @@ -529,7 +529,84 @@ apply (trans_le ? (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\ ] ] qed. - + +theorem le_sigma_p_div_log_div_pred_log : \forall n,b,m. S O < b \to b*b \leq n \to +sigma_p (S n) (\lambda i.leb (S n) (i*i)) (\lambda i.m/(log b i)) +\leq ((S (S O)) * n * m)/(pred (log b n)). +intros. +apply (trans_le ? (sigma_p (S n) + (\lambda i.leb (S n) (i*i)) (\lambda i.(S (S O))*m/(pred (log b n))))) + [apply le_sigma_p;intros;apply le_times_to_le_div + [rewrite > minus_n_O in ⊢ (? ? (? %));rewrite < eq_minus_S_pred; + apply le_plus_to_minus_r;simplify; + rewrite < (eq_log_exp b ? H); + apply le_log; + [assumption + |simplify;rewrite < times_n_SO;assumption] + |apply (trans_le ? ((pred (log b n) * m)/log b i)) + [apply le_times_div_div_times;apply lt_O_log + [elim (le_to_or_lt_eq ? ? (le_O_n i)) + [assumption + |apply False_ind;apply not_eq_true_false;rewrite < H3;rewrite < H4; + reflexivity] + |apply (le_exp_to_le1 ? ? (S (S O))) + [apply lt_O_S; + |apply (trans_le ? (S n)) + [apply le_S;simplify;rewrite < times_n_SO;assumption + |rewrite > exp_SSO;apply leb_true_to_le;assumption]]] + |apply le_times_to_le_div2 + [apply lt_O_log + [elim (le_to_or_lt_eq ? ? (le_O_n i)) + [assumption + |apply False_ind;apply not_eq_true_false;rewrite < H3;rewrite < H4; + reflexivity] + |apply (le_exp_to_le1 ? ? (S (S O))) + [apply lt_O_S; + |apply (trans_le ? (S n)) + [apply le_S;simplify;rewrite < times_n_SO;assumption + |rewrite > exp_SSO;apply leb_true_to_le;assumption]]] + |rewrite > sym_times in \vdash (? ? %);rewrite < assoc_times; + apply le_times_l;rewrite > sym_times; + rewrite > minus_n_O in \vdash (? (? %) ?); + rewrite < eq_minus_S_pred;apply le_plus_to_minus; + simplify;rewrite < plus_n_O;apply (trans_le ? (log b (i*i))) + [apply le_log + [assumption + |apply lt_to_le;apply leb_true_to_le;assumption] + |rewrite > sym_plus;simplify;apply log_times;assumption]]]] + |rewrite > times_n_SO in \vdash (? (? ? ? (\lambda i:?.%)) ?); + rewrite < distributive_times_plus_sigma_p; + apply (trans_le ? ((((S (S O))*m)/(pred (log b n)))*n)) + [apply le_times_r;apply (trans_le ? (sigma_p (S n) (\lambda i:nat.leb (S O) (i*i)) (\lambda Hbeta1:nat.S O))) + [apply le_sigma_p1;intros;do 2 rewrite < times_n_SO; + apply (bool_elim ? (leb (S n) (i*i))) + [intro;cut (leb (S O) (i*i) = true) + [rewrite > Hcut;apply le_n + |apply le_to_leb_true;apply (trans_le ? (S n)) + [apply le_S_S;apply le_O_n + |apply leb_true_to_le;assumption]] + |intro;simplify in \vdash (? % ?);apply le_O_n] + |elim n + [simplify;apply le_n + |apply (bool_elim ? (leb (S O) ((S n1)*(S n1))));intro + [rewrite > true_to_sigma_p_Sn + [change in \vdash (? % ?) with (S (sigma_p (S n1) (\lambda i:nat.leb (S O) (i*i)) (\lambda Hbeta1:nat.S O))); + apply le_S_S;assumption + |assumption] + |rewrite > false_to_sigma_p_Sn + [apply le_S;assumption + |assumption]]]] + |rewrite > sym_times in \vdash (? % ?); + rewrite > sym_times in \vdash (? ? (? (? % ?) ?)); + rewrite > assoc_times; + apply le_times_div_div_times; + rewrite > minus_n_O in ⊢ (? ? (? %));rewrite < eq_minus_S_pred; + apply le_plus_to_minus_r;simplify; + rewrite < (eq_log_exp b ? H); + apply le_log; + [assumption + |simplify;rewrite < times_n_SO;assumption]]] +qed. (* theorem le_log_exp_Sn_log_exp_n: \forall n,m,a,p. O < m \to S O < p \to divides n m \to -- 2.39.2