A few more lemmas.

diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma
index fa935be03784040f76892ff02fb0628b6e2ee687..2a3695e8e99c401322e4491248d62c6442c4d7ef 100644 (file)
--- a/helm/software/matita/library/nat/chebyshev.ma
+++ b/helm/software/matita/library/nat/chebyshev.ma
@@ -22,6 +22,7 @@ include "nat/factorial2.ma".
 definition prim: nat \to nat \def
 \lambda n. sigma_p (S n) primeb (\lambda p.(S O)).
 
+(* This is chebishev psi funcion *)
 definition A: nat \to nat \def
 \lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)).
 
@@ -79,6 +80,7 @@ elim (le_to_or_lt_eq ? ? (le_O_n n))
   ]
 qed.
 
+(* an equivalent formulation for psi *)
 definition A': nat \to nat \def
 \lambda n. pi_p (S n) primeb 
   (\lambda p.(pi_p (log p n) (\lambda i.true) (\lambda i.p))).
@@ -327,7 +329,8 @@ intro.elim q
     ]
   ]
 qed.
-    
+
+(* factorization of n into primes *)
 theorem pi_p_primeb_divides_b: \forall n. O < n \to 
 n = pi_p (S n) (\lambda i.primeb i \land divides_b i n) (\lambda p.exp p (ord n p)).
 intros.
@@ -505,6 +508,7 @@ apply eq_pi_p1
   ]
 qed.
 
+(* the factorial function *)
 theorem eq_fact_pi_p:\forall n. fact n = 
 pi_p (S n) (\lambda i.leb (S O) i) (\lambda i.i).
 intro.elim n
@@ -590,6 +594,7 @@ apply (div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q))
   ]
 qed.              
 
+(* still another characterization of the factorial *)
 theorem fact_pi_p: \forall n. fact n =
 pi_p (S n) primeb 
   (\lambda p.(pi_p (log p n) 
@@ -1161,8 +1166,7 @@ rewrite > eq_A_SSO_n
            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
+              [apply lt_plus_to_lt_minus
                 [assumption
                 |simplify in ⊢ (? % ?).
                  rewrite < plus_n_O.

diff --git a/helm/software/matita/library/nat/iteration2.ma b/helm/software/matita/library/nat/iteration2.ma
index c5236ff4a6f8678907c1143bf47ffd18d5c1dcf5..6dbbfd572a2ac824de1d69bff781d06eb18009cc 100644 (file)
--- a/helm/software/matita/library/nat/iteration2.ma
+++ b/helm/software/matita/library/nat/iteration2.ma
@@ -107,6 +107,84 @@ apply (false_to_eq_iter_p_gen);
   assumption.
 qed.
 
+theorem or_false_to_eq_sigma_p:
+\forall n,m:nat.\forall p:nat \to bool.
+\forall g: nat \to nat. 
+n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = O)
+\to sigma_p m p g = sigma_p n p g.
+intros.
+unfold sigma_p.
+apply or_false_eq_baseA_to_eq_iter_p_gen
+  [intros.reflexivity
+  |assumption
+  |assumption
+  ]
+qed.
+
+theorem bool_to_nat_to_eq_sigma_p:
+\forall n:nat.\forall p1,p2:nat \to bool.
+\forall g1,g2: nat \to nat. 
+(\forall i:nat. 
+bool_to_nat (p1 i)*(g1 i) = bool_to_nat (p2 i)*(g2 i)) 
+\to sigma_p n p1 g1 = sigma_p n p2 g2.
+intros.elim n
+  [reflexivity
+  |generalize in match (H n1).
+   apply (bool_elim ? (p1 n1));intro
+    [apply (bool_elim ? (p2 n1));intros
+      [rewrite > true_to_sigma_p_Sn
+        [rewrite > true_to_sigma_p_Sn
+          [apply eq_f2
+            [simplify in H4.
+             rewrite > plus_n_O.
+             rewrite > plus_n_O in ⊢ (? ? ? %).
+             assumption
+            |assumption
+            ]
+          |assumption
+          ]
+        |assumption
+        ]
+      |rewrite > true_to_sigma_p_Sn
+        [rewrite > false_to_sigma_p_Sn
+          [change in ⊢ (? ? ? %) with (O + sigma_p n1 p2 g2).
+           apply eq_f2
+            [simplify in H4.
+             rewrite > plus_n_O.
+             assumption
+            |assumption
+            ]
+          |assumption
+          ]
+        |assumption
+        ]
+      ]
+    |apply (bool_elim ? (p2 n1));intros
+      [rewrite > false_to_sigma_p_Sn
+        [rewrite > true_to_sigma_p_Sn
+          [change in ⊢ (? ? % ?) with (O + sigma_p n1 p1 g1).
+           apply eq_f2
+            [simplify in H4.
+             rewrite < plus_n_O in H4.
+             assumption
+            |assumption
+            ]
+          |assumption
+          ]
+        |assumption
+        ]
+      |rewrite > false_to_sigma_p_Sn
+        [rewrite > false_to_sigma_p_Sn
+          [assumption
+          |assumption
+          ]
+        |assumption
+        ]
+      ]
+    ]
+  ]
+qed.
+            
 theorem sigma_p2 : 
 \forall n,m:nat.
 \forall p1,p2:nat \to bool.
@@ -240,6 +318,90 @@ elim n
   ]
 qed.
 
+(* a slightly more general result *)
+theorem le_sigma_p1: 
+\forall n:nat. \forall p1,p2:nat \to bool. \forall g1,g2:nat \to nat.
+(\forall i. i < n \to 
+bool_to_nat (p1 i)*(g1 i) \le bool_to_nat (p2 i)*g2 i) \to 
+sigma_p n p1 g1 \le sigma_p n p2 g2.
+intros.
+generalize in match H.
+elim n
+  [apply le_n.
+  |apply (bool_elim ? (p1 n1));intros
+    [apply (bool_elim ? (p2 n1));intros
+      [rewrite > true_to_sigma_p_Sn
+        [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
+          [apply le_plus
+            [lapply (H2 n1) as H5
+              [rewrite > H3 in H5.
+               rewrite > H4 in H5.
+               simplify in H5.
+               rewrite < plus_n_O in H5.
+               rewrite < plus_n_O in H5.
+               assumption
+              |apply le_S_S.apply le_n
+              ]
+            |apply H1.intros.
+             apply H2.apply le_S.assumption
+            ]
+          |assumption
+          ]
+        |assumption
+        ]
+      |rewrite > true_to_sigma_p_Sn
+        [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
+          [change in ⊢ (? ? %) with (O + sigma_p n1 p2 g2).
+           apply le_plus
+            [lapply (H2 n1) as H5
+              [rewrite > H3 in H5.
+               rewrite > H4 in H5.
+               simplify in H5.
+               rewrite < plus_n_O in H5.
+               assumption
+              |apply le_S_S.apply le_n
+              ]
+            |apply H1.intros.
+             apply H2.apply le_S.assumption
+            ]
+          |assumption
+          ]
+        |assumption
+        ]
+      ]
+    |apply (bool_elim ? (p2 n1));intros
+      [rewrite > false_to_sigma_p_Sn
+        [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
+          [change in ⊢ (? % ?) with (O + sigma_p n1 p1 g1).
+           apply le_plus
+            [lapply (H2 n1) as H5
+              [rewrite > H3 in H5.
+               rewrite > H4 in H5.
+               simplify in H5.
+               rewrite < plus_n_O in H5.
+               assumption
+              |apply le_S_S.apply le_n
+              ]
+            |apply H1.intros.
+             apply H2.apply le_S.assumption
+            ]
+          |assumption
+          ]
+        |assumption
+        ]
+      |rewrite > false_to_sigma_p_Sn
+        [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
+          [apply H1.intros.
+           apply H2.apply le_S.assumption
+          |assumption
+          ]
+        |assumption
+        ]
+      ]
+    ]
+  ]
+qed.    
+
 theorem lt_sigma_p: 
 \forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat.
 (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to
@@ -539,7 +701,6 @@ rewrite > sym_times.
 apply eq_sigma_p_sigma_p_times1.
 qed.
 
-
 theorem sigma_p_times:\forall n,m:nat. 
 \forall f,f1,f2:nat \to bool.
 \forall g:nat \to nat \to nat. 
@@ -801,4 +962,21 @@ apply(iter_p_gen_2_eq nat O plus ? ? ? g h11 h12 h21 h22 n1 m1 n2 m2 p11 p21 p12
 | assumption
 | assumption
 ]
+qed.
+
+theorem sigma_p_sigma_p: 
+\forall g: nat \to nat \to nat.
+\forall n,m.
+\forall p11,p21:nat \to bool.
+\forall p12,p22:nat \to nat \to bool.
+(\forall x,y. x < n \to y < m \to 
+ (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
+sigma_p n p11 (\lambda x:nat.sigma_p m (p12 x) (\lambda y. g x y)) =
+sigma_p m p21 (\lambda y:nat.sigma_p n (p22 y) (\lambda x. g x y)).
+intros.
+unfold sigma_p.unfold sigma_p.
+apply (iter_p_gen_iter_p_gen ? ? ? sym_plus assoc_plus)
+  [intros.apply sym_eq.apply plus_n_O.
+  |assumption
+  ]
 qed.
\ No newline at end of file

diff --git a/helm/software/matita/library/nat/map_iter_p.ma b/helm/software/matita/library/nat/map_iter_p.ma
index ca5031f22148098d6588c8da04ce1011c0aa8fd8..080f9a45fb883fc573d8945af970b0216c4d726c 100644 (file)
--- a/helm/software/matita/library/nat/map_iter_p.ma
+++ b/helm/software/matita/library/nat/map_iter_p.ma
@@ -578,48 +578,6 @@ elim n
   ]
 qed.
 
-(* tutti d spostare *)
-theorem lt_minus_to_lt_plus:
-\forall n,m,p. n - m < p \to n < m + p.
-intros 2.
-apply (nat_elim2 ? ? ? ? n m)
-  [simplify.intros.autobatch.
-  |intros 2.rewrite < minus_n_O.
-   intro.assumption
-  |intros.
-   simplify.
-   cut (n1 < m1+p)
-    [autobatch
-    |apply H.
-     apply H1
-    ]
-  ]
-qed.
-
-theorem lt_plus_to_lt_minus:
-\forall n,m,p. m \le n \to n < m + p \to n - m < p.
-intros 2.
-apply (nat_elim2 ? ? ? ? n m)
-  [simplify.intros 3.
-   apply (le_n_O_elim ? H).
-   simplify.intros.assumption
-  |simplify.intros.assumption.
-  |intros.
-   simplify.
-   apply H
-    [apply le_S_S_to_le.assumption
-    |apply le_S_S_to_le.apply H2
-    ]
-  ]
-qed. 
-
-theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n).
-intros.
-apply sym_eq.
-apply plus_to_minus.
-autobatch.
-qed.
-
 theorem eq_map_iter_p_transpose2: \forall p.\forall f.associative nat f \to
 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le n \to
 (p (S n) = true) \to (p k) = true 

diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma
index 11585f2065706c33ba70901cd3944c4261ad775c..339e2262c72de402a1d29187e8a41907658038b7 100644 (file)
--- a/helm/software/matita/library/nat/minus.ma
+++ b/helm/software/matita/library/nat/minus.ma
@@ -296,6 +296,47 @@ apply (lt_minus_to_plus O  a b).
 assumption.
 qed.
 
+theorem lt_minus_to_lt_plus:
+\forall n,m,p. n - m < p \to n < m + p.
+intros 2.
+apply (nat_elim2 ? ? ? ? n m)
+  [simplify.intros.autobatch.
+  |intros 2.rewrite < minus_n_O.
+   intro.assumption
+  |intros.
+   simplify.
+   cut (n1 < m1+p)
+    [autobatch
+    |apply H.
+     apply H1
+    ]
+  ]
+qed.
+
+theorem lt_plus_to_lt_minus:
+\forall n,m,p. m \le n \to n < m + p \to n - m < p.
+intros 2.
+apply (nat_elim2 ? ? ? ? n m)
+  [simplify.intros 3.
+   apply (le_n_O_elim ? H).
+   simplify.intros.assumption
+  |simplify.intros.assumption.
+  |intros.
+   simplify.
+   apply H
+    [apply le_S_S_to_le.assumption
+    |apply le_S_S_to_le.apply H2
+    ]
+  ]
+qed. 
+
+theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n).
+intros.
+apply sym_eq.
+apply plus_to_minus.
+autobatch.
+qed.
+
 theorem distributive_times_minus: distributive nat times minus.
 unfold distributive.
 intros.

diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma
index 890d33c66043744e5be6df7db6b5cda72191ad44..df70accbc50dbbaad6cbe3ef920ecb0767b972f5 100644 (file)
--- a/helm/software/matita/library/nat/neper.ma
+++ b/helm/software/matita/library/nat/neper.ma
@@ -408,7 +408,7 @@ apply le_times_to_le_div
   ]
 qed.
       
-theorem sigma_p_log_div: \forall n,b. S O < b \to
+theorem sigma_p_log_div1: \forall n,b. S O < b \to
 sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
 \le sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)*S(log b (S(S(S O)))))))/n!
 ).
@@ -425,14 +425,14 @@ apply le_log_div_sigma_p
   ]
 qed.
 
-theorem sigma_p_log_div1: \forall n,b. S O < b \to
+theorem sigma_p_log_div2: \forall n,b. S O < b \to
 sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
 \le 
 (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)))))*S(log b (S(S(S O))))/n!).
 intros.
 apply (trans_le ? (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)*S(log b (S(S(S O)))))))/n!
 )))
-  [apply sigma_P_log_div.assumption
+  [apply sigma_p_log_div1.assumption
   |apply le_times_to_le_div
     [apply lt_O_fact
     |rewrite > distributive_times_plus_sigma_p.
@@ -460,18 +460,76 @@ apply (trans_le ? (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\
     ]
   ]
 qed.
-     
-(*     
+
 theorem sigma_p_log_div: \forall n,b. S O < b \to
 sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
-\le (sigma_p (S n) (\lambda i.leb (S n) (i*i)) (\lambda i.(prim i)*n!/i))*S(log b (S(S(S O)))/n!
-).
+\le (sigma_p n (\lambda i.leb (S n) (i*i)) (\lambda i.(prim i)*S(n!/i)))*S(log b (S(S(S O))))/n!
+.
 intros.
 apply (trans_le ? (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)))))*S(log b (S(S(S O))))/n!))
-  [apply sigma_p_log_div1
-  |unfold prim.
-*)
-
+  [apply sigma_p_log_div2.assumption
+  |apply monotonic_div
+    [apply lt_O_fact
+    |apply le_times_l.
+     unfold prim.
+     cut
+     (sigma_p (S n) (λp:nat.primeb p∧leb (S n) (p*p))
+      (λp:nat.sigma_p n (λi:nat.leb p i) (λi:nat.S (n!/i)))
+     = sigma_p n (λi:nat.leb (S n) (i*i))
+       (λi:nat.sigma_p (S n) (\lambda p.primeb p \land leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i))))
+      [rewrite > Hcut.
+       apply le_sigma_p.intros.
+       rewrite < sym_times.
+       rewrite > distributive_times_plus_sigma_p.
+       rewrite < times_n_SO.
+       cut 
+        (sigma_p (S n) (λp:nat.primeb p∧leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i))
+         = sigma_p (S i) (\lambda p.primeb p \land leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i)))
+        [rewrite > Hcut1.
+         apply le_sigma_p1.intros.
+         rewrite < andb_sym.
+         rewrite < andb_sym in ⊢ (? (? (? (? ? %)) ?) ?).
+         apply (bool_elim  ? (leb i1 i));intros
+          [apply (bool_elim  ? (leb (S n) (i1*i1)));intros
+            [apply le_n
+            |apply le_O_n
+            ]
+          |apply le_O_n
+          ]
+        |apply or_false_to_eq_sigma_p
+          [apply le_S.assumption
+          |intros.
+           left.rewrite > (lt_to_leb_false i1 i)
+            [rewrite > andb_sym.reflexivity
+            |assumption
+            ]
+          ]
+        ]
+      |apply sigma_p_sigma_p.intros.
+       apply (bool_elim ? (leb x y));intros
+        [apply (bool_elim ? (leb (S n) (x*x)));intros
+          [rewrite > le_to_leb_true in ⊢ (? ? ? (? % ?))
+            [reflexivity
+            |apply (trans_le ? (x*x))
+              [apply leb_true_to_le.assumption
+              |apply le_times;apply leb_true_to_le;assumption
+              ]
+            ]
+          |rewrite < andb_sym in ⊢ (? ? (? % ?) ?).
+           rewrite < andb_sym in ⊢ (? ? ? (? ? (? % ?))).
+           rewrite < andb_sym in ⊢ (? ? ? %).
+           reflexivity
+          ]
+        |rewrite < andb_sym.
+         rewrite > andb_assoc in ⊢ (? ? ? %).
+         rewrite < andb_sym in ⊢ (? ? ? (? % ?)).
+         reflexivity
+        ]
+      ]
+    ]
+  ]
+qed.
+         
 
 (* theorem le_log_exp_Sn_log_exp_n: \forall n,m,a,p. O < m \to S O < p \to
 divides n m \to