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

[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 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