X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fneper.ma;fp=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fneper.ma;h=890d33c66043744e5be6df7db6b5cda72191ad44;hb=2abee6f6b5f1cf989224c64e6ab9091624a34248;hp=51f65ef4aefeab3967525d226409e3a8b1eb00dc;hpb=1f136ddf1cf133efbf10b72b8800e0f8a93b6f68;p=helm.git

diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma
index 51f65ef4a..890d33c66 100644
--- a/helm/software/matita/library/nat/neper.ma
+++ b/helm/software/matita/library/nat/neper.ma
@@ -18,6 +18,7 @@ include "nat/iteration2.ma".
 include "nat/div_and_mod_diseq.ma".
 include "nat/binomial.ma".
 include "nat/log.ma".
+include "nat/chebyshev.ma".
 
 theorem sigma_p_div_exp: \forall n,m.
 sigma_p n (\lambda i.true) (\lambda i.m/(exp (S(S O)) i)) \le 
@@ -355,6 +356,123 @@ elim b
        |apply monotonic_exp1;assumption]]]]
 qed.
 
+theorem le_exp_div:\forall n,m,q. O < m \to 
+exp (n/m) q \le (exp n q)/(exp m q).
+intros.
+apply le_times_to_le_div
+  [apply lt_O_exp.
+   assumption
+  |rewrite > times_exp.
+   rewrite < sym_times.
+   apply monotonic_exp1.
+   rewrite > (div_mod n m) in ⊢ (? ? %)
+    [apply le_plus_n_r
+    |assumption
+    ]
+  ]
+qed.
+
+theorem le_log_div_sigma_p: \forall a,b,n,p. S O < p \to
+O < a \to a \le b \to b \le n \to
+log p (b/a) \le
+(sigma_p b (\lambda i.leb a i) (\lambda i.S((n!/i)*S(log p (S(S(S O)))))))/n!.
+intros.
+apply le_times_to_le_div
+  [apply lt_O_fact
+  |apply (trans_le ? (log p (exp (b/a) n!)))
+    [apply log_exp2
+      [assumption
+      |apply le_times_to_le_div
+        [assumption
+        |rewrite < times_n_SO.
+         assumption
+        ]
+      ]
+    |apply (trans_le ? (log p ((exp b n!)/(exp a n!)))) 
+      [apply le_log
+        [assumption
+        |apply le_exp_div.assumption
+        ]
+      |apply (trans_le ? (log p (exp b n!) - log p (exp a n!)))
+        [apply log_div
+          [assumption
+          |apply lt_O_exp.
+           assumption
+          |apply monotonic_exp1.
+           assumption
+          ]
+        |apply le_log_exp_fact_sigma_p;assumption
+        ]
+      ]
+    ]
+  ]
+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 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 le_sigma_p.intros.
+apply le_log_div_sigma_p
+  [assumption
+  |apply prime_to_lt_O.
+   apply primeb_true_to_prime.
+   apply (andb_true_true ? ? H2)
+  |apply le_S_S_to_le.
+   assumption
+  |apply le_n
+  ]
+qed.
+
+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!).
+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 le_times_to_le_div
+    [apply lt_O_fact
+    |rewrite > distributive_times_plus_sigma_p.
+     rewrite < sym_times in ⊢ (? ? %).
+     rewrite > distributive_times_plus_sigma_p.
+     apply le_sigma_p.intros.
+     apply (trans_le ? ((n!*(sigma_p n (λj:nat.leb i j) (λi:nat.S (n!/i*S (log b (S(S(S O)))))))/n!)))
+      [apply le_times_div_div_times.
+       apply lt_O_fact
+      |rewrite > sym_times.
+       rewrite > lt_O_to_div_times
+        [rewrite > distributive_times_plus_sigma_p.
+         apply le_sigma_p.intros.
+         rewrite < times_n_Sm in ⊢ (? ? %).
+         rewrite > plus_n_SO.
+         rewrite > sym_plus.
+         apply le_plus
+          [apply le_S_S.apply le_O_n
+          |rewrite < sym_times.
+           apply le_n
+          ]
+        |apply lt_O_fact
+        ]
+      ]
+    ]
+  ]
+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!
+).
+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.
+*)
+
+
 (* theorem le_log_exp_Sn_log_exp_n: \forall n,m,a,p. O < m \to S O < p \to
 divides n m \to
 log p (exp n m) - log p (exp a m) \le