arithmetics for λδ

[helm.git] / matita / matita / lib / arithmetics / chebyshev / bertrand.ma

diff --git a/matita/matita/lib/arithmetics/chebyshev/bertrand.ma b/matita/matita/lib/arithmetics/chebyshev/bertrand.ma
index 572c512ae2d28c938c5902926ccae5a350f203b3..8f41262e3b7519b5bb843605504e5a31c0ebc4e4 100644 (file)
--- a/matita/matita/lib/arithmetics/chebyshev/bertrand.ma
+++ b/matita/matita/lib/arithmetics/chebyshev/bertrand.ma
@@ -10,12 +10,12 @@
       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 \le 2*n ∧ (prime p).
+definition bertrand ≝ λn. ∃p.n < p ∧ p ≤ 2*n ∧ prime p.
 
-definition not_bertrand ≝ λn.∀p.n < p → p ≤ 2*n → \not (prime p).
+definition not_bertrand ≝ λn.∀p.n < p → p ≤ 2*n → ¬(prime p).
 
 lemma min_prim : ∀n.∃p. n < p ∧ prime p ∧
                  ∀q.prime q → q < p → q ≤ n.
@@ -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.
 
@@ -378,8 +378,6 @@ cut (S(n+(n+n*n)+0)=n*n+(n+(S n))) [//] #Hcut >Hcut >distributive_times_plus_r
 @monotonic_lt_times_l [@(ltn_to_ltO … posn) |@posn]
 qed.
 
-(* axiom daemon : ∀P:Prop.P. *)
-
 lemma sqrt_bound: ∀n. exp 2 8 ≤ n → 2*(S(log 2 (2*n))) ≤ sqrt (2*n).
 #n #len
 cut (8 ≤ log 2 n) [<(eq_log_exp 2 8) [@le_log [@le_n|@len]|@le_n]] #Hlog
@@ -416,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)
@@ -431,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))))
@@ -447,15 +445,5 @@ theorem le_to_bertrand2:
   ]
 qed.
 
-(*
-theorem bertrand_n :
-\forall n. O < n \to bertrand n.
-intros;elim (decidable_le n 256)
-  [apply le_to_bertrand;assumption
-  |apply le_to_bertrand2;apply lt_to_le;apply not_le_to_lt;apply H1]
-qed. *)
+(* see Bertrand256 for the complete theorem *)
 
-(* test 
-theorem mod_exp: eqb (mod (exp 2 8) 13) O = false.
-reflexivity.
-*)