include "nat/iteration2.ma".
include "nat/div_and_mod_diseq.ma".
include "nat/binomial.ma".
include "nat/log.ma".
include "nat/chebyshev.ma".
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
((S(S O))*m*(exp (S(S O)) n) - (S(S O))*m)/(exp (S(S O)) n).
theorem sigma_p_div_exp: \forall n,m.
sigma_p n (\lambda i.true) (\lambda i.m/(exp (S(S O)) i)) \le
((S(S O))*m*(exp (S(S O)) n) - (S(S O))*m)/(exp (S(S O)) n).
rewrite < (eq_plus_minus_minus_minus n x x);
[rewrite > exp_plus_times;
rewrite > sym_times;rewrite > sym_times in \vdash (? ? (? ? %) ?);
rewrite < (eq_plus_minus_minus_minus n x x);
[rewrite > exp_plus_times;
rewrite > sym_times;rewrite > sym_times in \vdash (? ? (? ? %) ?);
- rewrite > assoc_times;rewrite > sym_times in ⊢ (? ? (? (? (? ? %) ?) ?) ?);
- rewrite < eq_div_div_times
+ rewrite > assoc_times;
+ rewrite < sym_times in ⊢ (? ? (? (? (? % ?) ?) ?) ?);
+ rewrite < lt_to_lt_to_eq_div_div_times_times;
[rewrite > Hcut;rewrite < assoc_times;
cut (pi_p x (λi:nat.true) (λi:nat.n-i)/x!*(a)\sup(x)
= pi_p x (λi:nat.true) (λi:nat.(n-i))*pi_p x (\lambda i.true) (\lambda i.a)/x!)
[rewrite > Hcut;rewrite < assoc_times;
cut (pi_p x (λi:nat.true) (λi:nat.n-i)/x!*(a)\sup(x)
= pi_p x (λi:nat.true) (λi:nat.(n-i))*pi_p x (\lambda i.true) (\lambda i.a)/x!)
|apply lt_O_fact
|apply lt_O_fact]
|apply (inj_times_r (pred ((n-x)!)));
rewrite < (S_pred ((n-x)!))
[rewrite < assoc_times;rewrite < sym_times in \vdash (? ? (? % ?) ?);
|apply lt_O_fact
|apply lt_O_fact]
|apply (inj_times_r (pred ((n-x)!)));
rewrite < (S_pred ((n-x)!))
[rewrite < assoc_times;rewrite < sym_times in \vdash (? ? (? % ?) ?);
[rewrite < minus_n_O;simplify;rewrite < times_n_SO;reflexivity
|rewrite < fact_minus in H4;
[rewrite > true_to_pi_p_Sn
[rewrite < minus_n_O;simplify;rewrite < times_n_SO;reflexivity
|rewrite < fact_minus in H4;
[rewrite > true_to_pi_p_Sn
(\lambda k.(exp a (n-k))*(pi_p k (\lambda y.true) (\lambda i.a - (a*i/n)))/k!)/(exp a n).
intros;transitivity ((exp a n)*(exp (S n) n)/(exp n n)/(exp a n))
[rewrite > eq_div_div_div_times
(\lambda k.(exp a (n-k))*(pi_p k (\lambda y.true) (\lambda i.a - (a*i/n)))/k!)/(exp a n).
intros;transitivity ((exp a n)*(exp (S n) n)/(exp n n)/(exp a n))
[rewrite > eq_div_div_div_times
[elim H2;rewrite > H3;rewrite < times_exp;rewrite > sym_times in ⊢ (? ? (? (? ? ? (λ_:?.? ? %)) ?) ?);
rewrite > sym_times in ⊢ (? ? ? (? ? ? (λ_:?.? (? (? ? %) ?) ?)));
transitivity (sigma_p (S n) (λx:nat.true)
[elim H2;rewrite > H3;rewrite < times_exp;rewrite > sym_times in ⊢ (? ? (? (? ? ? (λ_:?.? ? %)) ?) ?);
rewrite > sym_times in ⊢ (? ? ? (? ? ? (λ_:?.? (? (? ? %) ?) ?)));
transitivity (sigma_p (S n) (λx:nat.true)
cut (pi_p i (\lambda y.true) (\lambda i.n-i) = (n!/(n-i)!))
[rewrite > Hcut1;rewrite > H3;rewrite > sym_times in ⊢ (? ? (? (? % ?) ?) ?);
rewrite > (S_pred ((n-i)!))
cut (pi_p i (\lambda y.true) (\lambda i.n-i) = (n!/(n-i)!))
[rewrite > Hcut1;rewrite > H3;rewrite > sym_times in ⊢ (? ? (? (? % ?) ?) ?);
rewrite > (S_pred ((n-i)!))
cut (pi_p i (\lambda y.true) (\lambda i.S n-i) = ((S n)!/(S n-i)!))
[rewrite > Hcut1;rewrite > H3;rewrite > sym_times in ⊢ (? ? (? (? % ?) ?) ?);
rewrite > (S_pred ((S n-i)!))
cut (pi_p i (\lambda y.true) (\lambda i.S n-i) = ((S n)!/(S n-i)!))
[rewrite > Hcut1;rewrite > H3;rewrite > sym_times in ⊢ (? ? (? (? % ?) ?) ?);
rewrite > (S_pred ((S n-i)!))