Bertrand's conjecture (weak), some work in progress

diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma
index 2a3695e8e99c401322e4491248d62c6442c4d7ef..1f50b3212642baba2caed404e5ef98d33b3cd0f7 100644 (file)
--- a/helm/software/matita/library/nat/chebyshev.ma
+++ b/helm/software/matita/library/nat/chebyshev.ma
@@ -1459,6 +1459,142 @@ elim H2
   ]
 qed.
 
+theorem le_A_exp4: \forall n. S O < n \to
+A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * (pred n))).
+intro.
+apply (nat_elim1 n).
+intros.
+elim (or_eq_eq_S m).
+elim H2
+  [elim (le_to_or_lt_eq (S O) a)
+    [rewrite > H3 in ⊢ (? % ?).
+     apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
+      [apply le_A_exp
+      |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
+         ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*(pred a)))))
+        [apply le_times_r.
+         apply H
+          [rewrite > H3.
+           rewrite > times_n_SO in ⊢ (? % ?).
+           rewrite > sym_times.
+           apply lt_times_l1
+            [apply lt_to_le.assumption
+            |apply le_n
+            ]
+          |assumption
+          ]
+        |rewrite > sym_times.
+         rewrite > assoc_times.
+         rewrite < exp_plus_times.
+         apply (trans_le ? 
+          (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*(pred m))))
+          [rewrite > assoc_times.
+           apply le_times_r.
+           rewrite < exp_plus_times.
+           apply le_exp
+            [apply lt_O_S
+            |rewrite < H3.
+             simplify.
+             rewrite < plus_n_O.
+             apply le_S.apply le_S.
+             rewrite < plus_n_O;
+             apply le_S_S_to_le;
+             rewrite > plus_n_Sm in \vdash (? ? %);
+             rewrite < S_pred;
+               [change in \vdash (? % ?) with ((S (pred a + pred a)) + m);
+                apply le_plus_l;
+                apply le_S_S_to_le;
+                rewrite < S_pred;
+                  [rewrite > plus_n_Sm;rewrite > sym_plus;
+                   rewrite > plus_n_Sm;
+                   rewrite > H3;simplify in \vdash (? ? %);
+                   rewrite < plus_n_O;rewrite < S_pred;
+                     [apply le_n
+                     |apply lt_to_le;assumption]
+                  |apply lt_to_le;assumption]
+               |apply lt_to_le;assumption]]
+          |apply le_times_l.
+           rewrite > times_exp.
+           apply monotonic_exp1.
+           rewrite > H3.
+           rewrite > sym_times.
+           cases a
+            [apply le_n
+            |simplify.
+             rewrite < plus_n_Sm.
+             apply le_S.
+             apply le_n
+            ]
+          ]
+        ]
+      ]
+    |rewrite < H4 in H3.
+     simplify in H3.
+     rewrite > H3.
+     simplify.
+     apply le_S_S.apply le_S_S.apply le_O_n
+    |apply not_lt_to_le.intro.
+     apply (lt_to_not_le ? ? H1).
+     rewrite > H3.
+     apply (le_n_O_elim a)
+      [apply le_S_S_to_le.assumption
+      |apply le_O_n
+      ]
+    ]
+  |elim (le_to_or_lt_eq O a (le_O_n ?))
+    [apply (trans_le ? (A ((S(S O))*(S a))))
+      [apply monotonic_A.
+       rewrite > H3.
+       rewrite > times_SSO.
+       apply le_n_Sn
+      |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
+        [apply le_A_exp
+        |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
+           (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
+          [apply le_times_r.
+           apply (trans_le ? ? ? (H (S a) ? ?));
+            [rewrite > H3.
+             apply le_S_S.
+             simplify.
+             rewrite > plus_n_SO.
+             apply le_plus_r.
+             rewrite < plus_n_O.
+             assumption
+            |apply le_S_S.assumption
+            |simplify in ⊢ (? (? (? % ?) ?) ?);
+             apply le_times_r;apply le_exp;
+               [apply le_S;apply le_n
+               |apply le_times_r;simplify;apply le_n]
+            ]
+          |rewrite > sym_times.
+           rewrite > assoc_times.
+           rewrite < exp_plus_times.
+           rewrite > H3;
+           change in ⊢ (? ? (? (? % ?) ?)) with ((S (S O))*a);
+           rewrite < times_exp;
+           rewrite < sym_times in \vdash (? ? (? % ?));
+           rewrite > assoc_times;
+           apply le_times_r;
+           rewrite < times_n_Sm in ⊢ (? (? ? (? ? %)) ?);
+           rewrite > sym_plus in \vdash (? (? ? %) ?);
+           rewrite > assoc_plus in \vdash (? (? ? %) ?);
+           rewrite > exp_plus_times;apply le_times_r;
+           rewrite < distr_times_plus in ⊢ (? (? ? %) ?);
+           simplify in ⊢ (? ? (? ? (? ? %)));rewrite < plus_n_O;
+           apply le_n
+          ]
+        ]
+      ]
+    |rewrite < H4 in H3.simplify in H3.
+     apply False_ind.
+     apply (lt_to_not_le ? ? H1).
+     rewrite > H3.
+     apply le_n
+    ]
+  ]
+qed.
+
+
 theorem eq_sigma_pi_SO_n: \forall n.
 sigma_p n (\lambda i.true) (\lambda i.S O) = n.
 intro.elim n
@@ -1488,6 +1624,15 @@ 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 ? ? ? ?))
+  [apply le_log
+     [assumption
+     |apply le_Al]
+  |assumption]
+qed.
+
 
 (* the inequalities *)
 theorem le_exp_priml: \forall n. O < n \to

diff --git a/helm/software/matita/library/nat/chebyshev_thm.ma b/helm/software/matita/library/nat/chebyshev_thm.ma
index c75594ab60fb23cee378548aa1568694f8809a14..248c9e3c67e041649752ac3f7262a7a789546c49 100644 (file)
--- a/helm/software/matita/library/nat/chebyshev_thm.ma
+++ b/helm/software/matita/library/nat/chebyshev_thm.ma
@@ -630,13 +630,13 @@ apply (trans_le ? (log b (A n) + (log b (C1 n * C2 n)) + 1));
 qed.
 
 lemma le_log_A1 : \forall n,b. S O < b \to S O < n \to
-                  log b (A n) \leq 2*(S (log b (pred n))) + (2*n)*(S (log b 2)) + 1.
-intros.apply (trans_le ? (log b ((exp (pred n) 2)*(exp 2 (2*n)))))
+                  log b (A n) \leq 2*(S (log b (pred n))) + (2*(pred n))*(S (log b 2)) + 1.
+intros.apply (trans_le ? (log b ((exp (pred n) 2)*(exp 2 (2*(pred n))))))
   [apply le_log
      [assumption
-     |simplify in ⊢ (? ? (? (? % ?) ?));apply le_A_exp3;assumption]
-  |rewrite < sym_plus;apply (trans_le ? (1 + ((log b (exp (pred n) 2)) + (log b (exp 2 (2*n))))));
-     [change in \vdash (? ? %) with (S (log b ((pred n)\sup(2))+log b ((2)\sup(2*n))));
+     |simplify in ⊢ (? ? (? (? % ?) ?));apply le_A_exp4;assumption]
+  |rewrite < sym_plus;apply (trans_le ? (1 + ((log b (exp (pred n) 2)) + (log b (exp 2 (2*(pred n)))))));
+     [change in \vdash (? ? %) with (S (log b ((pred n)\sup(2))+log b ((2)\sup(2*(pred n)))));
       apply log_times;assumption
      |apply le_plus_r;apply le_plus;apply log_exp1;assumption]]
 qed.
@@ -721,13 +721,13 @@ qed.
 
 lemma le_prim_log_stima: \forall n,b. S O < b \to b < sqrt n \to 
                      (prim n)*(log b n) \leq
-                      2*S (log b (pred n))+2*n*S (log b 2)
-                      +(2*S (log b (pred (sqrt n)))+2*sqrt n*S (log b 2))
+                      2*S (log b (pred n))+2*(pred n)*S (log b 2)
+                      +(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2))
                       +(14*n/log b n+28*n*S (log b 3)/pred (log b n))
                       +4.
 intros.cut (1 < n)
-  [apply (trans_le ? ((2*(S (log b (pred n))) + (2*n)*(S (log b 2)) + 1) + 
-                     (2*(S (log b (pred (sqrt n)))) + (2*(sqrt n))*(S (log b 2)) + 1) +
+  [apply (trans_le ? ((2*(S (log b (pred n))) + (2*(pred n))*(S (log b 2)) + 1) + 
+                     (2*(S (log b (pred (sqrt n)))) + (2*(pred (sqrt n)))*(S (log b 2)) + 1) +
                      ((14*n/(log b n)) + ((28*n)*(S (log b (S (S (S O)))))/pred (log b n))) + 2))
     [apply (trans_le ? ? ? (le_prim_log1 ? ? H ?))
        [apply lt_to_le;assumption
@@ -796,8 +796,8 @@ qed.
 
 lemma le_prim_stima: \forall n,b. S O < b \to b < sqrt n \to 
                      (prim n) \leq 
-                      2*S (log b (pred n))/(log b n) + 2*n*S (log b 2)/(log b n)
-                      +2*S (log b (pred (sqrt n)))/(log b n)+ 2*sqrt n*S (log b 2)/(log b n)
+                      2*S (log b (pred n))/(log b n) + 2*(pred n)*S (log b 2)/(log b n)
+                      +2*S (log b (pred (sqrt n)))/(log b n)+ 2*(pred (sqrt n))*S (log b 2)/(log b n)
                       + 14*n/(log b n * log b n) + 28*n*S (log b 3)/(pred (log b n) * log b n)
                       +4/(log b n) + 6.
 intros;
@@ -809,22 +809,22 @@ cut (O < log b n)
         |apply (trans_le ? (sqrt n))
            [apply lt_to_le;assumption
            |apply le_sqrt_n_n]]]
-apply (trans_le ? ((2*S (log b (pred n))+2*n*S (log b 2)
-                      +(2*S (log b (pred (sqrt n)))+2*sqrt n*S (log b 2))
+apply (trans_le ? ((2*S (log b (pred n))+2*(pred n)*S (log b 2)
+                      +(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2))
                       +(14*n/log b n+28*n*S (log b 3)/pred (log b n))
                       +4)/(log b n)))
   [apply le_times_to_le_div
      [assumption
      |rewrite > sym_times;apply le_prim_log_stima;assumption]
-  |apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*n*S (log b 2)
-+(2*S (log b (pred (sqrt n)))+2*sqrt n*S (log b 2))
+  |apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*(pred n)*S (log b 2)
++(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2))
 +(14*n/log b n+28*n*S (log b 3)/pred (log b n))) 4 (log b n) ?))
      [assumption
      |rewrite < plus_n_Sm;apply le_S_S;rewrite > assoc_plus in \vdash (? ? %);
       rewrite > sym_plus in \vdash (? ? (? ? %));
       rewrite < assoc_plus in \vdash (? ? %);
-      apply le_plus_l;apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*n*S (log b 2)
-+(2*S (log b (pred (sqrt n)))+2*sqrt n*S (log b 2))) (14*n/log b n+28*n*S (log b 3)/pred (log b n)) (log b n) ?));
+      apply le_plus_l;apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*(pred n)*S (log b 2)
++(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2))) (14*n/log b n+28*n*S (log b 3)/pred (log b n)) (log b n) ?));
          [assumption
          |rewrite < plus_n_Sm in \vdash (? ? %);apply le_S_S;
           change in \vdash (? ? (? ? %)) with (1+3);
@@ -833,7 +833,7 @@ apply (trans_le ? ((2*S (log b (pred n))+2*n*S (log b 2)
           rewrite > assoc_plus in ⊢ (? ? (? % ?));
           rewrite > sym_plus in \vdash (? ? %);rewrite < assoc_plus in \vdash (? ? %);
           rewrite > sym_plus in \vdash (? ? (? % ?));apply le_plus
-            [apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*n*S (log b 2)) (2*S (log b (pred (sqrt n)))+2*sqrt n*S (log b 2)) (log b n) ?))
+            [apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*pred n*S (log b 2)) (2*S (log b (pred (sqrt n)))+2*pred (sqrt n)*S (log b 2)) (log b n) ?))
                [assumption
                |rewrite < plus_n_Sm;apply le_S_S;change in \vdash (? ? (? ? %)) with (1+1);
                 rewrite < assoc_plus in \vdash (? ? %);rewrite > assoc_plus in ⊢ (? ? (? (? % ?) ?));
@@ -863,48 +863,103 @@ apply (trans_le ? ((2*S (log b (pred n))+2*n*S (log b 2)
                            |elim daemon]]
                      |assumption]]]]]]]
 qed.
-                   
 
-      
-(*intros;apply lt_to_le;lapply (lt_div_S (((S (S (S (S O))))* log b (pred i)) + (S (S (S (S (S O)))))) i)
-   [apply (trans_le ? ? ? Hletin);apply le_times_l;apply le_S_S;
-    elim H1
-      [rewrite > log_SO;
-         [simplify;apply le_n
-         |assumption]
-      |
-    apply le_times_to_le_div2;
-      |*)
-       
-(*   
-theorem le_log_C2_sigma_p : \forall n,b. S O < b \to
-log b (C2 n) \leq 
-(sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x))) (\lambda x.S O)) +
-(sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x))) 
-   (\lambda p.(sigma_p (n+p) (\lambda i.leb p i) 
-       (\lambda i.S ((n+p)!/i*(S (log b 3)))))/(n+p)!)).
-intros;unfold C2;
-apply (trans_le ? (sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) (λx:nat.1)
-+sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x))
- (λi.log b (S (n/i)))))
-  [apply log_pi_p;assumption
-  |apply le_plus
-     [apply le_n
-     |apply le_sigma_p;intros;cut (S (n/i) = (n+i)/i)
-        [rewrite > Hcut;apply le_log_div_sigma_p 
-           [assumption
-           |apply prime_to_lt_O;apply primeb_true_to_prime;
-            elim (and_true ? ? H2);assumption
-           |apply le_plus_n
-           |apply le_n]
-        |lapply (prime_to_lt_O i (primeb_true_to_prime ? (andb_true_true ? ? H2))) as H3;
-         apply (div_mod_spec_to_eq (n+i) i (S (n/i)) (n \mod i) ? ((n+i) \mod i))
-           [constructor 1
-              [apply lt_mod_m_m;assumption
-              |simplify;rewrite > assoc_plus;rewrite < div_mod;
-                 [apply sym_plus
-                 |assumption]]
-           |apply div_mod_spec_div_mod;assumption]]]]
+lemma leq_sqrt_n : \forall n. sqrt n * sqrt n \leq n.
+intro;unfold sqrt;apply leb_true_to_le;apply f_max_true;apply (ex_intro ? ? O);
+split
+  [apply le_O_n
+  |simplify;reflexivity]
 qed.
-*)
 
+lemma le_sqrt_log_n : \forall n,b. 2 < b \to sqrt n * log b n \leq n.
+intros.
+apply (trans_le ? ? ? ? (leq_sqrt_n ?));
+apply le_times_r;unfold sqrt;
+apply f_m_to_le_max
+  [apply le_log_n_n;apply lt_to_le;assumption
+  |apply le_to_leb_true;elim (le_to_or_lt_eq ? ? (le_O_n n))
+     [apply (trans_le ? (exp b (log b n)))
+        [elim (log b n)
+           [apply le_O_n
+           |simplify in \vdash (? ? %);
+           elim (le_to_or_lt_eq ? ? (le_O_n n1))
+              [elim (le_to_or_lt_eq ? ? H3)
+                 [apply (trans_le ? (3*(n1*n1)));
+                    [simplify in \vdash (? % ?);rewrite > sym_times in \vdash (? % ?);
+                     simplify in \vdash (? % ?);
+                     simplify;rewrite > sym_plus;
+                     rewrite > plus_n_Sm;rewrite > sym_plus in \vdash (? (? % ?) ?);
+                     rewrite > assoc_plus;apply le_plus_r;
+                     rewrite < plus_n_Sm;
+                     rewrite < plus_n_O;
+                     apply lt_plus;rewrite > times_n_SO in \vdash (? % ?);
+                     apply lt_times_r1;assumption;
+                    |apply le_times
+                       [assumption
+                       |assumption]]
+                 |rewrite < H4;apply le_times
+                    [apply lt_to_le;assumption
+                    |apply lt_to_le;simplify;rewrite < times_n_SO;assumption]]
+             |rewrite < H3;simplify;rewrite < times_n_SO;do 2 apply lt_to_le;assumption]]
+        |simplify;apply le_exp_log;assumption]
+     |rewrite < H1;simplify;apply le_n]]
+qed.
+    
+(* Bertrand weak, lavori in corso
+          
+theorem bertrand_weak : \forall n. 9 \leq n \to prim n < prim (4*n).
+intros.
+apply (trans_le ? ? ? (le_S_S ? ? (le_prim_stima ? 2 ? ?)))
+  [apply le_n
+  |unfold sqrt;apply f_m_to_le_max
+     [do 6 apply lt_to_le;assumption
+     |apply le_to_leb_true;assumption]
+  |cut (pred ((4*n)/(S (log 2 (4*n)))) \leq prim (4*n))
+     [|apply le_S_S_to_le;rewrite < S_pred
+       [apply le_times_to_le_div2
+          [apply lt_O_S
+          |change in \vdash (? % (? (? (? %)) (? (? ? %)))) with (2*2*n);
+           rewrite > assoc_times in \vdash (? % (? (? (? %)) (? (? ? %))));
+           rewrite > sym_times in \vdash (? ? %);
+           apply le_priml;rewrite > (times_n_O O) in \vdash (? % ?);
+           apply lt_times;
+             [apply lt_O_S
+             |apply (trans_le ? ? ? ? H);apply le_S_S;apply le_O_n]]
+       |apply le_times_to_le_div;
+          [apply lt_O_S
+          |rewrite < times_n_SO;apply (trans_le ? (S (S (2 + (log 2 n)))))
+             [apply le_S_S;apply (log_times 2 4 n);apply le_S_S;apply le_n
+             |change in \vdash (? % ?) with (4 + log 2 n);
+              rewrite > S_pred in \vdash (? ? (? ? %));
+                [change in ⊢ (? ? (? ? %)) with (1 + pred n);
+                 rewrite > distr_times_plus;apply le_plus_r;elim H
+                   [simplify;do 3 apply le_S_S;apply le_O_n
+                   |apply (trans_le ? (log 2 (2*n1)))
+                      [apply le_log;
+                         [apply le_S_S;apply le_n
+                         |rewrite < times_SSO_n;
+                          change in \vdash (? % ?) with (1 + n1);
+                          apply le_plus_l;apply (trans_le ? ? ? ? H1);
+                          apply lt_O_S]
+                      |apply (trans_le ? (S (4*pred n1)))
+                         [rewrite > exp_n_SO in ⊢ (? (? ? (? % ?)) ?);
+                          rewrite > log_exp
+                            [change in \vdash (? ? %) with (1 + (4*pred n1));
+                             apply le_plus_r;
+                             assumption
+                            |apply le_S_S;apply le_n
+                            |apply (trans_le ? ? ? ? H1);apply le_S_S;apply le_O_n]
+                         |simplify in \vdash (? ? (? ? %));
+                          rewrite > minus_n_O in \vdash (? (? (? ? (? %))) ?);
+                          rewrite < eq_minus_S_pred;
+                          rewrite > distr_times_minus;
+                          change in \vdash (? % ?) with (1 + (4*n1 - 4));
+                          rewrite > eq_plus_minus_minus_minus
+                            [simplify;apply le_minus_m;
+                            |apply lt_O_S
+                            |rewrite > times_n_SO in \vdash (? % ?);
+                             apply le_times_r;apply (trans_le ? ? ? ? H1);
+                             apply lt_O_S]]]]
+                |apply (trans_le ? ? ? ? H);apply lt_O_S]]]]]
+  apply (trans_le ? ? ? ? Hcut);
+*)