A few more lemmas.

[helm.git] / helm / software / matita / library / nat / neper.ma

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