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
|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