upper bound for logarithmic summation

diff --git a/helm/software/matita/library/nat/exp.ma b/helm/software/matita/library/nat/exp.ma
index cb64efee23ede4a7b329cfde8cd311178a91465a..25c81c0697bdd167b48883261e1fa5af5c62c0aa 100644 (file)
--- 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 df70accbc50dbbaad6cbe3ef920ecb0767b972f5..9378bd8dee4685787088fb23a6820134b6172753 100644 (file)
--- 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