Even if the error is not localized, it was not a good idea to make the unification...

[helm.git] / helm / software / matita / library / nat / chebyshev.ma

diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma
index a7b473ec031b98325e41873374eb1355d9b2f3ba..567e40ef6bad13927c6098602f9efb7f2bdc7c98 100644 (file)
--- a/helm/software/matita/library/nat/chebyshev.ma
+++ b/helm/software/matita/library/nat/chebyshev.ma
@@ -1016,6 +1016,34 @@ intro.cases n
   ]
 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.
+apply (le_times_to_le (exp (fact n) (S(S O))))
+  [apply lt_O_exp.
+   apply lt_O_fact
+  |rewrite < assoc_times in ⊢ (? ? %).
+   rewrite > sym_times in ⊢ (? ? (? % ?)).
+   rewrite > assoc_times in ⊢ (? ? %).
+   rewrite < eq_fact_B
+    [rewrite < sym_times.
+     apply fact3.
+     apply lt_to_le.assumption
+    |assumption
+    ]
+  ]
+qed.
+
+theorem le_exp_B: \forall n. O < n \to
+exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
+intros.
+elim H
+  [apply le_n
+  |apply lt_SO_to_le_exp_B.
+   apply le_S_S.assumption
+  ]
+qed.
+
 theorem eq_A_SSO_n: \forall n.O < n \to
 A((S(S O))*n) =
  pi_p (S ((S(S O))*n)) primeb 
@@ -1317,31 +1345,6 @@ intro.elim n
   ]
 qed.
 
-theorem times_exp: 
-\forall n,m,p. exp n p * exp m p = exp (n*m) p.
-intros.elim p
-  [simplify.reflexivity
-  |simplify.
-   rewrite > assoc_times.
-   rewrite < assoc_times in ⊢ (? ? (? ? %) ?).
-   rewrite < sym_times in ⊢ (? ? (? ? (? % ?)) ?).
-   rewrite > assoc_times in ⊢ (? ? (? ? %) ?).
-   rewrite < assoc_times.
-   rewrite < H.
-   reflexivity
-  ]
-qed.
-
-theorem monotonic_exp1: \forall n.
-monotonic nat le (\lambda x.(exp x n)).
-unfold monotonic. intros.
-simplify.elim n
-  [apply le_n
-  |simplify.
-   apply le_times;assumption
-  ]
-qed.
-
 (* a better result *)
 theorem le_A_exp3: \forall n. S O < n \to
 A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n)).
@@ -1468,6 +1471,89 @@ 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
+  [reflexivity
+  |rewrite > true_to_sigma_p_Sn
+    [rewrite > H.reflexivity
+    |reflexivity
+    ]
+  ]
+qed.
+
+theorem leA_prim: \forall n.
+exp n (prim n) \le A n * pi_p (S n) primeb (λp:nat.p).
+intro.
+unfold prim.
+rewrite < (exp_sigma_p (S n) n primeb).
+unfold A.
+rewrite < times_pi_p.
+apply le_pi_p.
+intros.
+rewrite > sym_times.
+change in ⊢ (? ? %) with (exp i (S (log i n))).
+apply lt_to_le.
+apply lt_exp_log.
+apply prime_to_lt_SO.
+apply primeb_true_to_prime.
+assumption.
+qed.
+
+
+(* the inequalities *)
+theorem le_exp_priml: \forall n. O < n \to
+exp (S(S O)) ((S(S O))*n) \le exp ((S(S O))*n) (S(prim ((S(S O))*n))).
+intros.
+apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n))))))
+  [apply le_exp_B.assumption
+  |change in ⊢ (? ? %) with ((((S(S O))*n))*(((S(S O))*n))\sup (prim ((S(S O))*n))).
+   apply le_times_r.
+   apply (trans_le ? (A ((S(S O))*n)))
+    [apply le_B_A
+    |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.
+rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?)
+  [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n)))))))
+    [apply le_log
+      [apply le_n
+      |apply lt_O_exp.apply lt_O_S
+      |apply le_exp_priml.assumption
+      ]
+    |rewrite > sym_times in ⊢ (? ? %). 
+     apply log_exp1.
+     apply le_n
+    ]
+  |apply le_n
+  ]
+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)).
+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 monotonic_exp1.
+     apply le_A_exp3.
+     assumption
+    |rewrite < times_exp.
+     rewrite > exp_exp_times.
+     rewrite > exp_exp_times.
+     rewrite > sym_times in ⊢ (? (? ? (? ? %)) ?).
+     rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
+     apply le_n
+    ]
+  ]
+qed.
 
 
 (* da spostare *)