New approximtions.

diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma
index 1f50b3212642baba2caed404e5ef98d33b3cd0f7..2c705635f6d618a7ec9cbcccca242fa4330767e0 100644 (file)
--- a/helm/software/matita/library/nat/chebyshev.ma
+++ b/helm/software/matita/library/nat/chebyshev.ma
@@ -22,7 +22,7 @@ include "nat/factorial2.ma".
 definition prim: nat \to nat \def
 \lambda n. sigma_p (S n) primeb (\lambda p.(S O)).
 
-(* This is chebishev psi funcion *)
+(* This is chebishev psi function *)
 definition A: nat \to nat \def
 \lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)).
 
@@ -975,6 +975,88 @@ apply le_exp
   ]
 qed.
 
+theorem le_B_A4: \forall n. O < n \to (S(S O))* B ((S(S(S(S O))))*n) \le A ((S(S(S(S O))))*n).
+intros.unfold B.
+rewrite > eq_A_A'.
+unfold A'.
+cut ((S(S O)) < (S ((S(S(S(S O))))*n)))
+  [cut (O<log (S(S O)) ((S(S(S(S O))))*n))
+    [rewrite > (pi_p_gi ? ? (S(S O)))
+      [rewrite > (pi_p_gi ? ? (S(S O))) in ⊢ (? ? %)
+        [rewrite < assoc_times.
+         apply le_times
+          [rewrite > (pi_p_gi ? ? O)
+            [rewrite > (pi_p_gi ? ? O) in ⊢ (? ? %)
+              [rewrite < assoc_times.
+               apply le_times
+                [rewrite < exp_n_SO.
+                 change in ⊢ (? (? ? (? ? (? (? (? % ?) ?) ?))) ?)
+                 with ((S(S O))*(S(S O))).
+                 rewrite > assoc_times.
+                 rewrite > sym_times in ⊢ (? (? ? (? ? (? (? % ?) ?))) ?).
+                 rewrite > lt_O_to_div_times
+                  [rewrite > divides_to_mod_O
+                    [apply le_n
+                    |apply lt_O_S
+                    |apply (witness ? ? n).reflexivity
+                    ]
+                  |apply lt_O_S
+                  ]
+                |apply le_pi_p.intros.
+                 rewrite > exp_n_SO in ⊢ (? ? %).
+                 apply le_exp
+                  [apply lt_O_S
+                  |apply le_S_S_to_le.
+                   apply lt_mod_m_m.
+                   apply lt_O_S
+                  ]
+                ]
+              |assumption
+              |reflexivity
+              ]
+            |assumption
+            |reflexivity
+            ]
+          |apply le_pi_p.intros.
+           apply le_pi_p.intros.
+           rewrite > exp_n_SO in ⊢ (? ? %).
+           apply le_exp
+            [apply prime_to_lt_O.
+             apply primeb_true_to_prime.
+             apply (andb_true_true ? ? H2)
+            |apply le_S_S_to_le.
+             apply lt_mod_m_m.
+             apply lt_O_S
+            ]
+          ]
+        |assumption
+        |reflexivity
+        ]
+      |assumption
+      |reflexivity
+      ]
+    |apply lt_O_log
+      [rewrite > (times_n_O (S(S(S(S O))))) in ⊢ (? % ?).
+       apply lt_times_r1
+        [apply lt_O_S
+        |assumption
+        ]
+      |rewrite > times_n_SO in ⊢ (? % ?).
+       apply le_times
+        [apply le_S.apply le_S.apply le_n
+        |assumption
+        ]
+      ]
+    ]
+  |apply le_S_S.
+   rewrite > times_n_SO in ⊢ (? % ?).
+   apply le_times
+    [apply le_S.apply le_n_Sn
+    |assumption
+    ]
+  ]
+qed.
+             
 theorem le_fact_A:\forall n.S O < n \to
 fact ((S(S O))*n) \le exp (fact n) (S(S O)) * A ((S(S O))*n).
 intros.
@@ -1594,7 +1676,6 @@ elim H2
   ]
 qed.
 
-
 theorem eq_sigma_pi_SO_n: \forall n.
 sigma_p n (\lambda i.true) (\lambda i.S O) = n.
 intro.elim n
@@ -1624,6 +1705,7 @@ apply primeb_true_to_prime.
 assumption.
 qed.
 
+
 theorem le_prim_log : \forall n,b.S O < b \to
 log b (A n) \leq prim n * (S (log b n)).
 intros;apply (trans_le ? ? ? ? (log_exp1 ? ? ? ?))
@@ -1649,6 +1731,35 @@ 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.
+apply (trans_le ? (2*(4*n*(B (4*n)))))
+  [change in ⊢ (? % ?) with (2*(exp 2 (4*n))).
+   apply le_times_r.
+   cut (4*n = 2*(2*n))
+    [rewrite > Hcut.
+     apply le_exp_B.
+     apply lt_to_le.unfold.
+     rewrite > times_n_SO in ⊢ (? % ?).
+     apply le_times_r.assumption
+    |rewrite < assoc_times.
+     reflexivity
+    ]
+  |change in ⊢ (? ? %) with ((4*n)*(4*n)\sup (prim (4*n))).
+   rewrite < assoc_times.
+   rewrite > sym_times in ⊢ (? (? % ?) ?).
+   rewrite > assoc_times.
+   apply le_times_r.
+   apply (trans_le ? (A (4*n)))
+    [apply le_B_A4.assumption
+    |apply le_Al
+    ]
+  ]
+qed.
+
 theorem le_priml: \forall n. O < n \to
 (S(S O))*n \le (S (log (S(S O)) ((S(S O))*n)))*S(prim ((S(S O))*n)).
 intros.
@@ -1667,15 +1778,15 @@ 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) ((S(S O))*(S(S O)))*(exp (S(S O)) ((S(S O))*(S(S O)) * n)).
+exp n (prim n) \le exp (pred n) ((S(S O))*(S(S O)))*(exp (S(S O)) ((S(S O))*(S(S O)) * (pred n))).
 intros.
 apply (trans_le ? (exp (A n) (S(S O))))
   [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))).
    rewrite < times_n_SO.
    apply leA_r2
-  |apply (trans_le ? (exp (exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n))) (S(S O))))
+  |apply (trans_le ? (exp (exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * (pred n)))) (S(S O))))
     [apply monotonic_exp1.
-     apply le_A_exp3.
+     apply le_A_exp4.
      assumption
     |rewrite < times_exp.
      rewrite > exp_exp_times.