Improved approximations for A and prim.

diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma
index e4ca6587a2bb8ad4b6d53919fc6619ab774545cb..317a82d15f2ebd3ae4b6648970cb3825ec3c7717 100644 (file)
--- a/helm/software/matita/library/nat/chebyshev.ma
+++ b/helm/software/matita/library/nat/chebyshev.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/chebishev".
-
 include "nat/log.ma".
 include "nat/pi_p.ma".
 include "nat/factorization.ma".
@@ -944,6 +942,30 @@ pi_p (S n) primeb
   (\lambda p.(pi_p (log p n)   
     (\lambda i.true) (\lambda i.(exp p (mod (n /(exp p (S i))) (S(S O))))))).
 
+theorem B_SSSO: B 3 = 6.
+reflexivity.
+qed.
+
+theorem B_SSSSO: B 4 = 6.
+reflexivity.
+qed.
+
+theorem B_SSSSSO: B 5 = 30.
+reflexivity.
+qed.
+
+theorem B_SSSSSSO: B 6 = 20.
+reflexivity.
+qed.
+
+theorem B_SSSSSSSO: B 7 = 140.
+reflexivity.
+qed.
+
+theorem B_SSSSSSSSO: B 8 = 70.
+reflexivity.
+qed.
+
 theorem eq_fact_B:\forall n.S O < n \to
 fact ((S(S O))*n) = exp (fact n) (S(S O)) * B((S(S O))*n).
 intros. unfold B.
@@ -1095,6 +1117,23 @@ intro.cases n
   ]
 qed.
 
+theorem lt_SSSSO_to_le_B_exp: \forall n.4 < n \to
+B (2*n) \le exp 2 ((2*n)-2).
+intros.
+apply (le_times_to_le (exp (fact n) (S(S O))))
+  [apply lt_O_exp.
+   apply lt_O_fact
+  |rewrite < eq_fact_B
+    [rewrite < sym_times in ⊢ (? ? %).
+     rewrite > exp_SSO.
+     rewrite < assoc_times.
+     apply lt_SSSSO_to_fact.assumption
+    |apply lt_to_le.apply lt_to_le.
+     apply lt_to_le.assumption
+    ]
+  ]
+qed.
+
 theorem lt_SO_to_le_exp_B: \forall n. S O < n \to
 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
 intros.
@@ -1304,6 +1343,16 @@ apply (trans_le ? (B(2*n)*A n))
   ]
 qed.
 
+theorem lt_SSSSO_to_le_A_exp: \forall n. 4 < n \to
+A(2*n) \le exp 2 ((2*n)-2)*A n.
+intros.
+apply (trans_le ? (B(2*n)*A n))
+  [apply le_A_BA
+  |apply le_times_l.
+   apply lt_SSSSO_to_le_B_exp.assumption
+  ]
+qed.
+
 theorem times_SSO_pred: \forall n. 2*(pred n) \le pred (2*n).
 intro.cases n
   [apply le_n
@@ -1723,6 +1772,138 @@ elim H2
   ]
 qed.
 
+theorem le_n_SSSSSSSSO_to_le_A_exp: 
+\forall n. n \le 8 \to A(n) \le exp 2 ((2 * n) -3).
+intro.cases n
+  [intro.apply le_n
+  |cases n1
+    [intro.apply le_n
+    |cases n2
+      [intro.apply le_n
+      |cases n3
+        [intro.apply leb_true_to_le.reflexivity
+        |cases n4
+          [intro.apply leb_true_to_le.reflexivity
+          |cases n5
+            [intro.apply leb_true_to_le.reflexivity
+            |cases n6
+              [intro.apply leb_true_to_le.reflexivity
+              |cases n7
+                [intro.apply leb_true_to_le.reflexivity
+                |cases n8
+                  [intro.apply leb_true_to_le.reflexivity
+                  |intro.apply False_ind.
+                   apply (lt_to_not_le ? ? H).
+                   apply leb_true_to_le.reflexivity
+                  ]
+                ]
+              ]
+            ]
+          ]
+        ]
+      ]
+    ]
+  ]
+qed.
+           
+theorem le_A_exp5: \forall n. A(n) \le exp 2 ((2 * n) -3).
+intro.
+apply (nat_elim1 n).
+intros.
+elim (decidable_le 9 m)
+  [elim (or_eq_eq_S m).
+   elim H2
+    [rewrite > H3 in ⊢ (? % ?).
+     apply (trans_le ? (exp 2 (pred(2*a))*A a))
+      [apply le_A_exp
+      |apply (trans_le ? (2\sup(pred(2*a))*(2\sup((2*a)-3))))
+        [apply le_times_r.
+         apply H.
+         rewrite > H3. 
+         apply lt_m_nm
+          [apply (trans_lt ? 4)
+            [apply lt_O_S
+            |apply (lt_times_to_lt 2)
+              [apply lt_O_S
+              |rewrite < H3.assumption
+              ]
+            ]
+          |apply le_n
+          ]
+        |rewrite < H3.
+         rewrite < exp_plus_times.
+         apply le_exp
+          [apply lt_O_S
+          |simplify.rewrite < plus_n_O.
+           rewrite > eq_minus_plus_plus_minus
+            [apply le_plus_l.
+             apply le_pred_n
+            |apply (trans_le ? 9)
+              [apply leb_true_to_le. reflexivity
+              |assumption
+              ]
+            ]
+          ]
+        ]
+      ]
+    |apply (trans_le ? (A (2*(S a))))
+      [apply monotonic_A.
+       rewrite > H3.
+       rewrite > times_SSO.
+       apply le_n_Sn
+      |apply (trans_le ? ((exp 2 ((2*(S a))-2))*A (S a)))
+        [apply lt_SSSSO_to_le_A_exp.
+         apply le_S_S.
+         apply (le_times_to_le 2)
+          [apply le_n_Sn.
+          |apply le_S_S_to_le.rewrite < H3.assumption
+          ]
+        |apply (trans_le ? ((2\sup((2*S a)-2))*(exp 2 ((2*(S a))-3))))
+          [apply le_times_r.
+           apply H.
+           rewrite > H3.
+           apply le_S_S. 
+           apply lt_m_nm
+            [apply (lt_to_le_to_lt ? 4)
+              [apply lt_O_S
+              |apply (le_times_to_le 2)
+                [apply lt_O_S
+                |apply le_S_S_to_le.
+                 rewrite < H3.assumption
+                ]
+              ]
+            |apply le_n
+            ]
+          |rewrite > times_SSO.
+           rewrite < H3.
+           rewrite < exp_plus_times.
+           apply le_exp
+            [apply lt_O_S
+            |cases m
+              [apply le_n
+              |cases n1
+                [apply le_n
+                |simplify.
+                 rewrite < minus_n_O.
+                 rewrite < plus_n_O.
+                 rewrite < plus_n_Sm.
+                 simplify.rewrite < minus_n_O.
+                 rewrite < plus_n_Sm.
+                 apply le_n
+                ]
+              ]
+            ]
+          ]
+        ]
+      ]
+    ]
+  |apply le_n_SSSSSSSSO_to_le_A_exp.
+   apply le_S_S_to_le.
+   apply not_le_to_lt.
+   assumption
+  ]
+qed.       
+
 theorem eq_sigma_pi_SO_n: \forall n.
 sigma_p n (\lambda i.true) (\lambda i.S O) = n.
 intro.elim n
@@ -1778,8 +1959,6 @@ apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n))))))
   ]
 qed.
 
-alias num (instance 0) = "natural number".
-
 theorem le_exp_prim4l: \forall n. O < n \to
 exp 2 (S(4*n)) \le exp (4*n) (S(prim (4*n))).
 intros.
@@ -1824,23 +2003,17 @@ rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?)
   ]
 qed.
 
-theorem le_exp_primr: \forall n. S O < n \to
-exp n (prim n) \le exp (pred n) 2*(exp 2 (2*(2*n-3))).
+theorem le_exp_primr: \forall n.
+exp n (prim n) \le exp 2 (2*(2*n-3)).
 intros.
 apply (trans_le ? (exp (A n) 2))
   [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))).
    rewrite < times_n_SO.
    apply leA_r2
-  |apply (trans_le ? (exp ((pred n)*(exp 2 (2*n - 3))) 2))
-    [apply monotonic_exp1.
-     apply le_A_exp4.
-     assumption
-    |rewrite < times_exp.
-     rewrite > exp_exp_times.
-     apply le_times_r.
-     rewrite > sym_times.
-     apply le_n
-    ]
+  |rewrite > sym_times.
+   rewrite < exp_exp_times.
+   apply monotonic_exp1.
+   apply le_A_exp5
   ]
 qed.