X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fchebyshev%2Fbertrand.ma;h=8f41262e3b7519b5bb843605504e5a31c0ebc4e4;hb=aad5588b82d0f2991c336f7ac2f3fadd76768eeb;hp=df94a30f674f58030fe25e9a3fe2a883dd2f7c27;hpb=5f00537e0e589f1adaf7f3a40f0a7bcfa006dfd8;p=helm.git

diff --git a/matita/matita/lib/arithmetics/chebyshev/bertrand.ma b/matita/matita/lib/arithmetics/chebyshev/bertrand.ma
index df94a30f6..8f41262e3 100644
--- a/matita/matita/lib/arithmetics/chebyshev/bertrand.ma
+++ b/matita/matita/lib/arithmetics/chebyshev/bertrand.ma
@@ -10,8 +10,8 @@
       V_______________________________________________________________ *)
 
 include "arithmetics/sqrt.ma".
-include "arithmetics/chebyshev/chebyshev_B.ma".
-include "arithmetics/chebyshev/chebyshev_teta.ma".
+include "arithmetics/chebyshev/psi_bounds.ma". 
+include "arithmetics/chebyshev/chebyshev_theta.ma". 
 
 definition bertrand ≝ λn. ∃p.n < p ∧ p ≤ 2*n ∧ prime p.
 
@@ -85,38 +85,38 @@ theorem le_k: ∀n,p. k n p ≤ log p n.
   ]
 qed.
 
-definition B1 ≝ λn. 
+definition Bk ≝ λn. 
   ∏_{p < S n | primeb p}(exp p (k n p)).
   
-lemma B1_def : ∀n. B1 n = ∏_{p < S n | primeb p}(exp p (k n p)).
+lemma Bk_def : ∀n. Bk n = ∏_{p < S n | primeb p}(exp p (k n p)).
 // qed.
 
 definition Dexp ≝ mk_Dop nat 1 timesAC (λa,b.exp b a) ??.
   [// | normalize //]
 qed.
   
-theorem eq_B_B1: ∀n. B n = B1 n.
-#n >Bdef >B1_def @same_bigop
+theorem eq_B_Bk: ∀n. B n = Bk n.
+#n >Bdef >Bk_def @same_bigop
   [// |#i #ltiS #_ >k_def @exp_sigma_l]
 qed.
 
-definition B_split1 ≝ λn. 
+definition B1 ≝ λn. 
   ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb (k n p) 1)* (k n p))).
 
-lemma B_split1_def : ∀n.
-  B_split1 n = ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb (k n p) 1)* (k n p))).
+lemma B1_def : ∀n.
+  B1 n = ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb (k n p) 1)* (k n p))).
 // qed.
 
-definition B_split2 ≝ λn. 
+definition B2 ≝ λn. 
   ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb 2 (k n p))* (k n p))).
 
-lemma B_split2_def : ∀n.
-  B_split2 n = ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb 2 (k n p))* (k n p))).
+lemma B2_def : ∀n.
+  B2 n = ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb 2 (k n p))* (k n p))).
 // qed.
 
-theorem eq_B1_times_B_split1_B_split2: ∀n. 
-  B1 n = B_split1 n * B_split2 n.
-#n >B1_def >B_split1_def >B_split2_def <times_pi
+theorem eq_Bk_B1_B2: ∀n. 
+  Bk n = B1 n * B2 n.
+#n >Bk_def >B1_def >B2_def <times_pi
 @same_bigop
   [//
   |#p #ltp #primebp cases (true_or_false (leb (k n p) 1)) #Hc >Hc
@@ -166,7 +166,7 @@ elim (log p (2*n))
           [@leb_true_to_le //
           |>commutative_times in ⊢ (??%); > times_exp
            @(transitive_le ? (exp n 2))
-            [<associative_times >exp_2 in ⊢ (??%); @le_times //
+            [<associative_times >exp_2 in ⊢ (??%); @le_times [@le18|//]
             |@(le_exp1 … (lt_O_S ?))
              @(le_plus_to_le 3)
              cut (3+2*n/3*3 = S(2*n/3)*3) [//] #eq1 >eq1
@@ -189,9 +189,9 @@ elim (log p (2*n))
   ]
 qed.
         
-theorem le_B_split1_teta:∀n.18 ≤ n → not_bertrand n →
-  B_split1 (2*n) ≤ teta (2 * n / 3).
-#n #le18 #not_Bn >B_split1_def >teta_def
+theorem le_B1_theta:∀n.18 ≤ n → not_bertrand n →
+  B1 (2*n) ≤ theta (2 * n / 3).
+#n #le18 #not_Bn >B1_def >theta_def
 @(transitive_le ? (∏_{p < S (2*n) | primeb p} (p\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
   [@le_pi #p #ltp #primebp @le_exp
     [@prime_to_lt_O @primeb_true_to_prime //
@@ -224,9 +224,9 @@ theorem le_B_split1_teta:∀n.18 ≤ n → not_bertrand n →
   ]
 qed.
 
-theorem le_B_split2_exp: ∀n. exp 2 7 ≤ n →
-  B_split2 (2*n) ≤ exp (2*n) (pred(sqrt(2*n)/2)).
-#n #len >B_split2_def
+theorem le_B2_exp: ∀n. exp 2 7 ≤ n →
+  B2 (2*n) ≤ exp (2*n) (pred(sqrt(2*n)/2)).
+#n #len >B2_def
 cut (O < n) [@(lt_to_le_to_lt … len) @leb_true_to_le //] #posn
 @(transitive_le ? 
    (∏_{p < S (sqrt (2*n)) | primeb p}
@@ -279,12 +279,12 @@ qed.
 theorem not_bertrand_to_le_B: 
   ∀n.exp 2 7 ≤ n → not_bertrand n →
   B (2*n) ≤ (exp 2 (2*(2 * n / 3)))*(exp (2*n) (pred(sqrt(2*n)/2))).
-#n #len #notB >eq_B_B1 >eq_B1_times_B_split1_B_split2 @le_times
-  [@(transitive_le ? (teta ((2*n)/3)))
-    [@le_B_split1_teta [@(transitive_le … len) @leb_true_to_le //|//]
-    |@le_teta
+#n #len #notB >eq_B_Bk >eq_Bk_B1_B2 @le_times
+  [@(transitive_le ? (theta ((2*n)/3)))
+    [@le_B1_theta [@(transitive_le … len) @leb_true_to_le //|//]
+    |@le_theta
     ]
-  |@le_B_split2_exp //
+  |@le_B2_exp //
   ]
 qed.
 
@@ -414,7 +414,7 @@ cut (0<n) [@(lt_to_le_to_lt … len) @lt_O_S] #posn
          <exp_S <plus_minus_m_m [2:@lt_O_log //]
          -Hind #Hind <Hclog @(transitive_le … Hind)
          >(eq_log_exp … (le_n ?)) >(eq_log_exp … (le_n ?))
-         >plus_minus_commutative [2:@lt_O_log //]
+         >plus_minus_associative [2:@lt_O_log //]
          cut (2+3 ≤ 2+log 2 m) 
           [@monotonic_le_plus_r @(le_exp_to_le 2) [@le_n|>Hclog @lt_to_le @lt8m]]
          generalize in match (2+log 2 m); #a #Hle >(commutative_times 2 a)
@@ -429,7 +429,7 @@ cut (0<n) [@(lt_to_le_to_lt … len) @lt_O_S] #posn
   ]
 qed.
 
-theorem le_to_bertrand2:
+theorem bertrand_up:
    ∀n. 2^8 ≤ n → bertrand n.
 #n #len @not_not_bertrand_to_bertrand % #notBn
 @(absurd (2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n))))