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

diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma
index f980d4458..a7b473ec0 100644
--- a/helm/software/matita/library/nat/chebyshev.ma
+++ b/helm/software/matita/library/nat/chebyshev.ma
@@ -988,7 +988,7 @@ rewrite > eq_fact_B
   ]
 qed.
 
-theorem le_B_exp: \forall n.S O < n \to
+theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
 intros.
 apply (le_times_to_le (exp (fact n) (S(S O))))
@@ -1004,171 +1004,471 @@ apply (le_times_to_le (exp (fact n) (S(S O))))
   ]
 qed.
 
-theorem le_A_SSO_A: \forall n.
-A((S(S O))*n) \le 
- pi_p (S ((S(S O))*n)) primeb (λp:nat.p)*A n.
-unfold A.intros.
-cut (pi_p (S n) primeb (λp:nat.(exp p (log p n))) = pi_p (S ((S(S O))*n)) primeb (λp:nat.(p)\sup(log p n)))
+theorem le_B_exp: \forall n.
+B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
+intro.cases n
+  [apply le_n
+  |cases n1
+    [simplify.apply le_S.apply le_S.apply le_n
+    |apply lt_SO_to_le_B_exp.
+     apply le_S_S.apply lt_O_S.
+    ]
+  ]
+qed.
+
+theorem eq_A_SSO_n: \forall n.O < n \to
+A((S(S O))*n) =
+ pi_p (S ((S(S O))*n)) primeb 
+  (\lambda p.(pi_p (log p ((S(S O))*n) )   
+    (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
+ *A n.
+intro.
+rewrite > eq_A_A'.rewrite > eq_A_A'.
+unfold A'.intros.
+cut (
+ pi_p (S n) primeb (λp:nat.pi_p (log p n) (λi:nat.true) (λi:nat.p))
+ = pi_p (S ((S(S O))*n)) primeb
+    (λp:nat.pi_p (log p ((S(S O))*n)) (λi:nat.true) (λi:nat.(p)\sup(bool_to_nat (\lnot (leb (S n) (exp p (S i))))))))
   [rewrite > Hcut.
    rewrite < times_pi_p.
-   apply le_pi_p.intros.
-   lapply (prime_to_lt_SO ? (primeb_true_to_prime ? H1)) as H2.
-   change with (i\sup(log i ((S(S O))*n))≤i\sup(S(log i n))).
-   apply le_exp
-    [apply lt_to_le.assumption
-    |apply (trans_le ? (log i (i*n)))
-      [apply le_log
-        [assumption
-        |apply not_le_to_lt.intro.
-         apply (lt_to_not_le ? ? H).  
-         apply (trans_le ? (S O)) 
-          [apply le_S_S.assumption
-          |apply lt_to_le.assumption
-          ] 
-        |apply le_times_l.
-         assumption
+   apply eq_pi_p1;intros
+    [reflexivity
+    |rewrite < times_pi_p.
+     apply eq_pi_p;intros
+      [reflexivity
+      |apply (bool_elim ? (leb (S n) (exp x (S x1))));intro
+        [simplify.rewrite < times_n_SO.apply times_n_SO
+        |simplify.rewrite < plus_n_O.apply times_n_SO
         ]
-      |rewrite > exp_n_SO in ⊢ (? (? ? (? % ?)) ?).
-       rewrite > log_exp
-        [apply le_n
-        |assumption
-        |apply not_le_to_lt.intro.
-         apply (lt_to_not_le ? ? H). 
-         apply (le_n_O_elim ? H3).
-         apply lt_to_le.
-         assumption
-        ] 
       ]
     ]
-  |apply sym_eq.
-   apply or_false_eq_SO_to_eq_pi_p
-    [apply le_S_S.
-     apply le_times_n.
-     apply lt_O_S
-    |intros.right.
-     change with (exp i (log i n) = (exp i O)).
-     apply eq_f.
-     apply antisymmetric_le
-      [cut (O < n)
-        [apply le_S_S_to_le.
-         apply (lt_exp_to_lt i)
-          [apply (le_to_lt_to_lt ? n);assumption
-          |apply (le_to_lt_to_lt ? n)
-            [apply le_exp_log.
+  |apply (trans_eq ? ? (pi_p (S n) primeb 
+    (\lambda p:nat.pi_p (log p n) (\lambda i:nat.true) (\lambda i:nat.(p)\sup(bool_to_nat (¬leb (S n) (exp p (S i))))))))
+    [apply eq_pi_p1;intros
+      [reflexivity
+      |apply eq_pi_p1;intros
+        [reflexivity
+        |rewrite > lt_to_leb_false
+          [simplify.apply times_n_SO
+          |apply le_S_S.
+           apply (trans_le ? (exp x (log x n)))
+            [apply le_exp
+              [apply prime_to_lt_O.
+               apply primeb_true_to_prime.
+               assumption
+              |assumption
+              ]
+            |apply le_exp_log.
              assumption
-            |rewrite < exp_n_SO.
+            ]
+          ]
+        ]
+      ]
+    |apply (trans_eq ? ? 
+      (pi_p (S ((S(S O))*n)) primeb
+       (λp:nat.pi_p (log p n) (λi:nat.true)
+        (λi:nat.(p)\sup(bool_to_nat (¬leb (S n) ((p)\sup(S i))))))))
+      [apply sym_eq.
+       apply or_false_eq_SO_to_eq_pi_p
+        [apply le_S_S.
+         simplify.
+         apply le_plus_n_r
+        |intros.right.
+         rewrite > lt_to_log_O
+          [reflexivity
+          |assumption
+          |assumption
+          ]
+        ]
+      |apply eq_pi_p1;intros
+        [reflexivity
+        |apply sym_eq.
+         apply or_false_eq_SO_to_eq_pi_p
+          [apply le_log
+            [apply prime_to_lt_SO.
+             apply primeb_true_to_prime.
              assumption
+            |assumption
+            |simplify.
+             apply le_plus_n_r
+            ]
+          |intros.right.
+           rewrite > le_to_leb_true
+            [simplify.reflexivity
+            |apply (lt_to_le_to_lt ? (exp x (S (log x n))))
+              [apply lt_exp_log.
+               apply prime_to_lt_SO.
+               apply primeb_true_to_prime.
+               assumption
+              |apply le_exp
+                [apply prime_to_lt_O.
+                 apply primeb_true_to_prime.
+                 assumption
+                |apply le_S_S.assumption
+                ]
+              ]
             ]
           ]
-        |apply not_le_to_lt.intro.
-         apply (lt_to_not_le ? ? H1).
-         generalize in match H.
-         apply (le_n_O_elim ? H2).
-         intro.assumption
         ]
-      |apply le_O_n
       ]
     ]
   ]
 qed.
-    
-(* so far so good 
-
-theorem le_A_BA: \forall n. 
+               
+theorem le_A_BA1: \forall n. O < n \to 
 A((S(S O))*n) \le B((S(S O))*n)*A n.
-(*
-  [simplify.reflexivity
-  |rewrite > times_SSO.
-   rewrite > times_SSO.
-   unfold A.
-apply (trans_le ? ((pi_p (S ((S(S O))*n)) primeb (λp:nat.p))*A n))
-  [apply le_A_SSO_A
-  |apply le_times_l.
+intros.
+rewrite > eq_A_SSO_n
+  [apply le_times_l.
    unfold B.
    apply le_pi_p.intros.
-*)
-intro.unfold A.unfold B.
-cut (pi_p (S n) primeb (λp:nat.(exp p (log p n))) = pi_p (S ((S(S O))*n)) primeb (λp:nat.(p)\sup(log p n)))
-  [rewrite > Hcut.
-   rewrite < times_pi_p.
    apply le_pi_p.intros.
-   apply le_trans i.
-   
-
-   change with (i\sup(log i ((S(S O))*n))≤i\sup(S(log i n))).
    apply le_exp
     [apply prime_to_lt_O.
      apply primeb_true_to_prime.
      assumption
-    |apply (trans_le ? (log i (i*n)))
-      [apply le_log
-        [apply prime_to_lt_SO.
-         apply primeb_true_to_prime.
-         assumption
-        |apply not_le_to_lt.intro.
-         apply (lt_to_not_le ? ? H).  
-         apply (trans_le ? (S O)) 
-          [apply le_S_S.assumption
-          |apply prime_to_lt_O.
+    |apply (bool_elim ? (leb (S n) (exp i (S i1))));intro
+      [simplify in ⊢ (? % ?).
+       cut ((S(S O))*n/i\sup(S i1) = S O)
+        [rewrite > Hcut.apply le_n
+        |apply (div_mod_spec_to_eq 
+          ((S(S O))*n) (exp i (S i1)) 
+           ? (mod ((S(S O))*n) (exp i (S i1))) 
+           ? (minus ((S(S O))*n) (exp i (S i1))) )
+          [apply div_mod_spec_div_mod.
+           apply lt_O_exp.
+           apply prime_to_lt_O.
            apply primeb_true_to_prime.
-           assumption 
-          ] 
-        |apply le_times_l.
-         apply prime_to_lt_SO.
-         apply primeb_true_to_prime.
-         assumption
+           assumption
+          |cut (i\sup(S i1)≤(S(S O))*n)
+            [apply div_mod_spec_intro
+              [alias id "lt_plus_to_lt_minus" = "cic:/matita/nat/map_iter_p.ma/lt_plus_to_lt_minus.con".
+               apply lt_plus_to_lt_minus
+                [assumption
+                |simplify in ⊢ (? % ?).
+                 rewrite < plus_n_O.
+                 apply lt_plus
+                  [apply leb_true_to_le.assumption
+                  |apply leb_true_to_le.assumption
+                  ]
+                ]
+              |rewrite > sym_plus.
+               rewrite > sym_times in ⊢ (? ? ? (? ? %)).
+               rewrite < times_n_SO.
+               apply plus_minus_m_m.
+               assumption
+              ]
+            |apply (trans_le ? (exp i (log i ((S(S O))*n))))
+              [apply le_exp
+                [apply prime_to_lt_O.
+                 apply primeb_true_to_prime.
+                 assumption
+                |assumption
+                ]
+              |apply le_exp_log.
+               rewrite > (times_n_O O) in ⊢ (? % ?).
+               apply lt_times 
+                [apply lt_O_S
+                |assumption
+                ]
+              ]
+            ]
+          ]
         ]
-      |rewrite > exp_n_SO in ⊢ (? (? ? (? % ?)) ?).
-       rewrite > log_exp
-        [apply le_n
-        |apply prime_to_lt_SO.
-         apply primeb_true_to_prime.
+      |apply le_O_n
+      ]
+    ]
+  |assumption
+  ]
+qed.
+
+theorem le_A_BA: \forall n. A((S(S O))*n) \le B((S(S O))*n)*A n.
+intros.cases n
+  [apply le_n
+  |apply le_A_BA1.apply lt_O_S
+  ]
+qed.
+
+theorem le_A_exp: \forall n.
+A((S(S O))*n) \le (exp (S(S O)) ((S(S O)*n)))*A n.
+intro.
+apply (trans_le ? (B((S(S O))*n)*A n))
+  [apply le_A_BA
+  |apply le_times_l.
+   apply le_B_exp
+  ]
+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 not_le_to_lt.intro.
-         apply (lt_to_not_le ? ? H). 
-         apply (le_n_O_elim ? H2).
-         apply prime_to_lt_O.
+        ]
+      |apply le_pi_p.intros.
+       apply le_exp
+        [apply prime_to_lt_O.
          apply primeb_true_to_prime.
          assumption
-        ] 
-      ]
-    ]
-  |apply sym_eq.
-   apply or_false_eq_SO_to_eq_pi_p
-    [apply le_S_S.
-     apply le_times_n.
-     apply lt_O_S
-    |intros.right.
-     change with (exp i (log i n) = (exp i O)).
-     apply eq_f.
-     apply antisymmetric_le
-      [cut (O < n)
-        [apply le_S_S_to_le.
-         apply (lt_exp_to_lt i)
-          [apply (le_to_lt_to_lt ? n);assumption
-          |apply (le_to_lt_to_lt ? n)
-            [apply le_exp_log.
+        |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
-            |rewrite < exp_n_SO.
+            |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
+            ]
           ]
-        |apply not_le_to_lt.intro.
-         apply (lt_to_not_le ? ? H1).
-         generalize in match H.
-         apply (le_n_O_elim ? H2).
-         intro.assumption
         ]
+      ]
+    |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.
 
 
-unfold A.unfold B.
-rewrite > eq_A_A'.rewrite > eq_A_A'.
-unfold A'.unfold B.
 
 (* da spostare *)
 theorem times_exp: \forall n,m,p.exp n p * exp m p = exp (n*m) p.
@@ -1678,3 +1978,4 @@ elim (lt_O_to_or_eq_S m)
        
        a*log a-a+k*log a
        
+*)
\ No newline at end of file