(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/neper".
-
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).
|apply le_log
[assumption
|cut (O = exp O n!)
- [rewrite > Hcut;apply monotonic_exp1;constructor 2;
+ [apply monotonic_exp1;constructor 2;
apply leb_true_to_le;assumption
|elim n
[reflexivity
rewrite < (eq_plus_minus_minus_minus n x x);
[rewrite > exp_plus_times;
rewrite > sym_times;rewrite > sym_times in \vdash (? ? (? ? %) ?);
- rewrite < eq_div_div_times;
+ rewrite < sym_times;
+ rewrite < sym_times in ⊢ (? ? (? ? %) ?);
+ rewrite < lt_to_lt_to_eq_div_div_times_times;
[reflexivity
|*:apply lt_O_exp;assumption]
|apply le_n
elim (bc2 n x)
[rewrite > H3;cut (x!*n2 = pi_p x (\lambda i.true) (\lambda i.(n - i)))
[rewrite > sym_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?);
- 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!)
|assumption]
|assumption]
|assumption]
- |do 2 rewrite > false_to_sigma_p_Sn;assumption]]
+ |do 2 try rewrite > false_to_sigma_p_Sn;assumption]]
qed.
lemma neper_sigma_p3 : \forall a,n.O < a \to O < n \to n \divides a \to (exp (S n) n)/(exp n n) =
(\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
- [rewrite > sym_times in \vdash (? ? ? (? ? %));rewrite < eq_div_div_times;
+ [rewrite < sym_times; rewrite < lt_to_lt_to_eq_div_div_times_times;
[reflexivity
|apply lt_O_exp;assumption
|apply lt_O_exp;assumption]
[rewrite > H4
[rewrite > sym_times;rewrite < divides_times_to_eq
[rewrite < fact_minus
- [rewrite > sym_times;
- rewrite < eq_div_div_times
+ [rewrite > sym_times in ⊢ (? ? (? ? %) ?);
+ rewrite < lt_to_lt_to_eq_div_div_times_times;
[reflexivity
|apply lt_to_lt_O_minus;apply le_S_S_to_le;
assumption
[rewrite > H4
[rewrite > sym_times;rewrite < divides_times_to_eq
[rewrite < fact_minus
- [rewrite > sym_times;
- rewrite < eq_div_div_times
+ [rewrite > sym_times in ⊢ (? ? (? ? %) ?);
+ rewrite < lt_to_lt_to_eq_div_div_times_times;
[reflexivity
|apply lt_to_lt_O_minus;apply lt_to_le;
assumption