update: upper bound for prim

diff --git a/helm/software/matita/library/nat/chebyshev_thm.ma b/helm/software/matita/library/nat/chebyshev_thm.ma
index 28e3ba5d20d57045db7cfa8d51ca778976a39625..c75594ab60fb23cee378548aa1568694f8809a14 100644 (file)
--- a/helm/software/matita/library/nat/chebyshev_thm.ma
+++ b/helm/software/matita/library/nat/chebyshev_thm.ma
@@ -774,6 +774,97 @@ intros.cut (1 < n)
   |apply (trans_le ? ? ? H);apply lt_to_le;apply (trans_le ? ? ? H1);
    apply le_sqrt_n_n]
 qed.
+
+lemma eq_div_div_div_times: \forall a,b,c. O < b \to O < c \to a/b/c = a/(b*c).
+intros.rewrite > (div_mod a (b*c)) in \vdash (? ? % ?)
+ [rewrite > (div_mod (a \mod (b*c)) b)
+    [rewrite < assoc_plus;
+     rewrite > sym_times in ⊢ (? ? (? (? (? (? (? ? %) ?) ?) ?) ?) ?);
+     rewrite < assoc_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?);
+     rewrite > sym_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?);
+     rewrite > sym_times in ⊢ (? ? (? (? (? (? ? %) ?) ?) ?) ?);
+     rewrite < distr_times_plus;rewrite < sym_times in ⊢ (? ? (? (? (? % ?) ?) ?) ?);
+     rewrite > (div_plus_times b)
+       [rewrite > (div_plus_times c)
+          [reflexivity
+          |apply lt_times_to_lt_div;rewrite > sym_times in \vdash (? ? %);
+           apply lt_mod_m_m;unfold lt;rewrite > times_n_SO;apply le_times;assumption]
+       |apply lt_mod_m_m;assumption]
+    |assumption]
+ |unfold lt;rewrite > times_n_SO;apply le_times;assumption]
+qed.
+
+lemma le_prim_stima: \forall n,b. S O < b \to b < sqrt n \to 
+                     (prim n) \leq 
+                      2*S (log b (pred n))/(log b n) + 2*n*S (log b 2)/(log b n)
+                      +2*S (log b (pred (sqrt n)))/(log b n)+ 2*sqrt n*S (log b 2)/(log b n)
+                      + 14*n/(log b n * log b n) + 28*n*S (log b 3)/(pred (log b n) * log b n)
+                      +4/(log b n) + 6.
+intros;
+cut (O < log b n) 
+  [|apply lt_O_log;
+        [apply lt_to_le;apply (trans_le ? ? ? H);apply (trans_le ? (sqrt n))
+           [apply lt_to_le;assumption
+           |apply le_sqrt_n_n;]
+        |apply (trans_le ? (sqrt n))
+           [apply lt_to_le;assumption
+           |apply le_sqrt_n_n]]]
+apply (trans_le ? ((2*S (log b (pred n))+2*n*S (log b 2)
+                      +(2*S (log b (pred (sqrt n)))+2*sqrt n*S (log b 2))
+                      +(14*n/log b n+28*n*S (log b 3)/pred (log b n))
+                      +4)/(log b n)))
+  [apply le_times_to_le_div
+     [assumption
+     |rewrite > sym_times;apply le_prim_log_stima;assumption]
+  |apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*n*S (log b 2)
++(2*S (log b (pred (sqrt n)))+2*sqrt n*S (log b 2))
++(14*n/log b n+28*n*S (log b 3)/pred (log b n))) 4 (log b n) ?))
+     [assumption
+     |rewrite < plus_n_Sm;apply le_S_S;rewrite > assoc_plus in \vdash (? ? %);
+      rewrite > sym_plus in \vdash (? ? (? ? %));
+      rewrite < assoc_plus in \vdash (? ? %);
+      apply le_plus_l;apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*n*S (log b 2)
++(2*S (log b (pred (sqrt n)))+2*sqrt n*S (log b 2))) (14*n/log b n+28*n*S (log b 3)/pred (log b n)) (log b n) ?));
+         [assumption
+         |rewrite < plus_n_Sm in \vdash (? ? %);apply le_S_S;
+          change in \vdash (? ? (? ? %)) with (1+3);
+          rewrite < assoc_plus in \vdash (? ? %);
+          rewrite > assoc_plus in ⊢ (? ? (? (? % ?) ?));
+          rewrite > assoc_plus in ⊢ (? ? (? % ?));
+          rewrite > sym_plus in \vdash (? ? %);rewrite < assoc_plus in \vdash (? ? %);
+          rewrite > sym_plus in \vdash (? ? (? % ?));apply le_plus
+            [apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*n*S (log b 2)) (2*S (log b (pred (sqrt n)))+2*sqrt n*S (log b 2)) (log b n) ?))
+               [assumption
+               |rewrite < plus_n_Sm;apply le_S_S;change in \vdash (? ? (? ? %)) with (1+1);
+                rewrite < assoc_plus in \vdash (? ? %);rewrite > assoc_plus in ⊢ (? ? (? (? % ?) ?));
+                rewrite > assoc_plus in ⊢ (? ? (? % ?));
+                rewrite > sym_plus in \vdash (? ? %);
+                rewrite < assoc_plus in \vdash (? ? %);
+                rewrite > sym_plus in \vdash (? ? (? % ?));
+                apply le_plus
+                  [rewrite < plus_n_Sm;rewrite < plus_n_O;apply le_div_plus_S;
+                   assumption
+                  |rewrite < plus_n_Sm;rewrite < plus_n_O;apply le_div_plus_S;
+                   assumption]]
+            |rewrite < plus_n_Sm;rewrite < plus_n_O;apply (trans_le ? ? ? (le_div_plus_S ? ? ? ?));
+               [assumption
+               |apply le_S_S;apply le_plus
+                  [rewrite > eq_div_div_div_times;
+                     [apply le_n
+                     |*:assumption]
+                  |rewrite > eq_div_div_div_times
+                     [apply le_n
+                     |rewrite > minus_n_O in \vdash (? ? (? %));
+                      rewrite < eq_minus_S_pred;apply lt_to_lt_O_minus;
+                      apply (trans_le ? (log b (sqrt n * sqrt n)))
+                        [elim daemon;
+                        |apply le_log;
+                           [assumption
+                           |elim daemon]]
+                     |assumption]]]]]]]
+qed.
+                   
+
       
 (*intros;apply lt_to_le;lapply (lt_div_S (((S (S (S (S O))))* log b (pred i)) + (S (S (S (S (S O)))))) i)
    [apply (trans_le ? ? ? Hletin);apply le_times_l;apply le_S_S;