X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fchebyshev.ma;h=a7b473ec031b98325e41873374eb1355d9b2f3ba;hb=a1f4ef3daaeed7a3121a40afe55f321565669da8;hp=c06675d0e2d3db98e1019496b3ed94887609fba5;hpb=fb3cf5acfd87741651c5e30ad1911a08e26f6c69;p=helm.git

diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma
index c06675d0e..a7b473ec0 100644
--- a/helm/software/matita/library/nat/chebyshev.ma
+++ b/helm/software/matita/library/nat/chebyshev.ma
@@ -1199,6 +1199,277 @@ apply (trans_le ? (B((S(S O))*n)*A n))
   ]
 qed.
 
+theorem le_A_exp1: \forall n.
+A(exp (S(S O)) n) \le (exp (S(S O)) ((S(S O))*(exp (S(S O)) n))).
+intro.elim n
+  [simplify.apply le_S_S.apply le_O_n
+  |change with (A ((S(S O))*((S(S O)))\sup n1)≤ ((S(S O)))\sup((S(S O))*((S(S O))\sup(S n1)))).
+   apply (trans_le ? ((exp (S(S O)) ((S(S O)*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
+    [apply le_A_exp
+    |apply (trans_le ? ((S(S O))\sup((S(S O))*((S(S O)))\sup(n1))*(S(S O))\sup((S(S O))*((S(S O)))\sup(n1))))
+      [apply le_times_r.
+       assumption
+      |rewrite < exp_plus_times.
+       simplify.rewrite < plus_n_O in ⊢ (? ? (? ? (? ? %))).
+       apply le_n
+      ]
+    ]
+  ]
+qed.  
+
+theorem monotonic_A: monotonic nat le A.
+unfold.intros.
+elim H
+  [apply le_n
+  |apply (trans_le ? (A n1))
+    [assumption
+    |unfold A.
+     cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1))
+          ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1))))
+      [apply (bool_elim ? (primeb (S n1)));intro
+        [rewrite > (true_to_pi_p_Sn ? ? ? H3).
+         rewrite > times_n_SO in ⊢ (? % ?).
+         rewrite > sym_times.
+         apply le_times
+          [apply lt_O_exp.apply lt_O_S
+          |assumption
+          ]
+        |rewrite > (false_to_pi_p_Sn ? ? ? H3).
+         assumption
+        ]
+      |apply le_pi_p.intros.
+       apply le_exp
+        [apply prime_to_lt_O.
+         apply primeb_true_to_prime.
+         assumption
+        |apply le_log
+          [apply prime_to_lt_SO.
+           apply primeb_true_to_prime.
+           assumption
+          |apply (lt_to_le_to_lt ? i)
+            [apply prime_to_lt_O.
+             apply primeb_true_to_prime.
+             assumption
+            |apply le_S_S_to_le.
+             assumption
+            ]
+          |apply le_S.apply le_n
+          ]
+        ]
+      ]
+    ]
+  ]
+qed.
+ 
+theorem le_A_exp2: \forall n. O < n \to
+A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
+intros.
+apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
+  [apply monotonic_A.
+   apply lt_to_le.
+   apply lt_exp_log.
+   apply le_n
+  |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
+    [apply le_A_exp1
+    |apply le_exp
+      [apply lt_O_S
+      |rewrite > assoc_times.apply le_times_r.
+       change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
+       apply le_times_r.
+       apply le_exp_log.
+       assumption
+      ]
+    ]
+  ]
+qed.
+
+(* example *)
+theorem A_SO: A (S O) = S O.
+reflexivity.
+qed.
+
+theorem A_SSO: A (S(S O)) = S (S O).
+reflexivity.
+qed.
+
+theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
+reflexivity.
+qed.
+
+theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
+reflexivity.
+qed.
+
+(* da spostare *)
+theorem or_eq_eq_S: \forall n.\exists m. 
+n = (S(S O))*m \lor n = S ((S(S O))*m).
+intro.elim n
+  [apply (ex_intro ? ? O).
+   left.reflexivity
+  |elim H.elim H1
+    [apply (ex_intro ? ? a).
+     right.apply eq_f.assumption
+    |apply (ex_intro ? ? (S a)).
+     left.rewrite > H2.
+     apply sym_eq.
+     apply times_SSO
+    ]
+  ]
+qed.
+
+theorem times_exp: 
+\forall n,m,p. exp n p * exp m p = exp (n*m) p.
+intros.elim p
+  [simplify.reflexivity
+  |simplify.
+   rewrite > assoc_times.
+   rewrite < assoc_times in ⊢ (? ? (? ? %) ?).
+   rewrite < sym_times in ⊢ (? ? (? ? (? % ?)) ?).
+   rewrite > assoc_times in ⊢ (? ? (? ? %) ?).
+   rewrite < assoc_times.
+   rewrite < H.
+   reflexivity
+  ]
+qed.
+
+theorem monotonic_exp1: \forall n.
+monotonic nat le (\lambda x.(exp x n)).
+unfold monotonic. intros.
+simplify.elim n
+  [apply le_n
+  |simplify.
+   apply le_times;assumption
+  ]
+qed.
+
+(* a better result *)
+theorem le_A_exp3: \forall n. S O < n \to
+A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * 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))*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))*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.
+             apply le_n
+            ]
+          |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))*(S a)))))
+          [apply le_times_r.
+           apply H
+            [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
+            ]
+          |rewrite > sym_times.
+           rewrite > assoc_times.
+           rewrite < exp_plus_times.
+           apply (trans_le ? 
+            (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
+            [rewrite > assoc_times.
+             apply le_times_r.
+             rewrite < exp_plus_times.
+             apply le_exp
+              [apply lt_O_S
+              |rewrite > times_SSO.
+               rewrite < H3.
+               simplify.
+               rewrite < plus_n_Sm.
+               rewrite < plus_n_O.
+               apply le_n
+              ]
+            |apply le_times_l.
+             rewrite > times_exp.
+             apply monotonic_exp1.
+             rewrite > H3.
+             rewrite > sym_times.
+             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.
+
+
+
 (* da spostare *)
 theorem times_exp: \forall n,m,p.exp n p * exp m p = exp (n*m) p.
 intros.elim p