X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fchebyshev_teta.ma;h=1765b38072626e02bd6593da9f31654ac0c36d22;hb=b771a37f83637be22d9b3f1254a6a0f15dc49612;hp=bdec363910b2fe1a099607cb67183468fd4a4abb;hpb=d74bdbdea0586eaa764c53a22e2c660d5367d0d5;p=helm.git

diff --git a/helm/software/matita/library/nat/chebyshev_teta.ma b/helm/software/matita/library/nat/chebyshev_teta.ma
index bdec36391..1765b3807 100644
--- a/helm/software/matita/library/nat/chebyshev_teta.ma
+++ b/helm/software/matita/library/nat/chebyshev_teta.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/chebyshev_teta".
-
 include "nat/binomial.ma".
 include "nat/pi_p.ma".
 
@@ -385,7 +383,7 @@ apply divides_to_le
   ]
 qed.
 
-theorem lt_O_to_le_teta_M_teta: \forall m. O < m\to
+theorem lt_O_to_le_teta_exp_teta: \forall m. O < m\to
 teta (S(2*m)) < exp 2 (2*m)*teta (S m). 
 intros. 
 apply (le_to_lt_to_lt ? (M m*teta (S m)))
@@ -398,5 +396,105 @@ apply (le_to_lt_to_lt ? (M m*teta (S m)))
   ]
 qed.
 
+theorem teta_pred: \forall n. S O < n \to teta (2*n) = teta (pred (2*n)).
+intros.unfold teta.
+rewrite > false_to_pi_p_Sn
+  [rewrite < S_pred
+    [reflexivity
+    |rewrite > (times_n_O 2) in ⊢ (? % ?).
+     apply lt_times_r.
+     apply lt_to_le.assumption
+    ]
+  |apply not_prime_to_primeb_false.
+   intro.
+   elim H1.
+   apply (lt_to_not_eq ? ? H).
+   apply (injective_times_r 1).
+   rewrite < times_n_SO.
+   apply H3
+    [apply (witness ? ? n).reflexivity
+    |apply le_n
+    ]
+  ]
+qed.
   
+theorem le_teta: \forall m.teta m \le exp 2 (2*m).
+intro.apply (nat_elim1 m).intros.
+elim (or_eq_eq_S m1).
+elim H1
+  [rewrite > H2.
+   generalize in match H2.
+   cases a
+    [intro.apply le_n
+    |cases n;intros
+      [apply leb_true_to_le.reflexivity
+      |rewrite > teta_pred
+        [rewrite > times_SSO.
+         change in ⊢ (? (? %) ?) with (S (2*S n1)).
+         apply (trans_le ? (exp 2 (2*(S n1))*teta (S (S n1))))
+          [apply lt_to_le.
+           apply lt_O_to_le_teta_exp_teta.
+           apply lt_O_S
+          |rewrite < times_SSO.
+           change in ⊢ (? ? (? ? %)) with ((2*S (S n1))+((2*S (S n1)) + O)).
+           rewrite < plus_n_O.
+           rewrite > exp_plus_times.
+           apply le_times
+            [apply le_exp
+              [apply lt_O_S
+              |apply le_times_r.
+               apply le_n_Sn
+              ]
+            |apply H.
+             rewrite > H3. 
+             apply lt_m_nm
+              [apply lt_O_S
+              |apply le_n
+              ]
+            ]
+          ]
+        |apply le_S_S.apply lt_O_S
+        ]
+      ]
+    ]
+  |rewrite > H2.
+   generalize in match H2.
+   cases a;intro
+    [apply leb_true_to_le.reflexivity
+    |apply (trans_le ? (exp 2 (2*(S n))*teta (S (S n))))
+      [apply lt_to_le.
+       apply lt_O_to_le_teta_exp_teta.
+       apply lt_O_S
+      |change in ⊢ (? ? (? ? %)) with (S (2*S n) + (S (2*S n) +O)).
+       rewrite < plus_n_O.
+       rewrite < plus_n_Sm.
+       rewrite < sym_plus.
+       rewrite > plus_n_Sm.
+       rewrite > exp_plus_times.
+       apply le_times_r.
+       rewrite < times_SSO.
+       apply H.
+       rewrite > H3.
+       apply le_S_S.
+       apply lt_m_nm
+        [apply lt_O_S
+        |apply le_n
+        ]
+      ]
+    ]
+  ]
+qed.
+   
+(*             
+alias id "sqrt" = "cic:/matita/nat/sqrt/sqrt.con".
+alias id "not" = "cic:/matita/logic/connectives/Not.con".
+theorem absurd_bound: \forall n. exp 2 7 \le n \to 
+(\forall p. n < p \to p < 2*n \to not (prime p)) \to
+bc (2*n) n < exp (2*n) (div (sqrt (2*n)) 2 - 1)*exp 4 (div (2*n) 3).
+intros.
+cut (O < n)
+  [cut (sqrt (2*n) < div (2*n) 3)
+    [
+  |
+*)