(* *)
(**************************************************************************)
-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).
assumption
|apply lt_exp_Sn_n_SSSO
]
- |apply (O_lt_times_to_O_lt ? n2).
+ |apply (O_lt_times_to_O_lt ? n1).
rewrite < H2.
assumption
]
|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
|(*già usata 2 volte: fattorizzare*)
elim n
[simplify;apply le_n
- |apply (bool_elim ? (p n1));intro
+ |apply (bool_elim ? (p n2));intro
[rewrite > true_to_pi_p_Sn
[rewrite > (times_n_O O);apply lt_times
- [elim (H n1);assumption
+ [elim (H n2);assumption
|assumption]
|assumption]
|rewrite > false_to_pi_p_Sn;assumption]]]
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
[rewrite > exp_plus_times;
unfold bc;
elim (bc2 n x)
- [rewrite > H3;cut (x!*n2 = pi_p x (\lambda i.true) (\lambda i.(n - i)))
+ [rewrite > H3;cut (x!*n1 = 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!)
[apply divides_SO_n
|elim x
[simplify;apply divides_SO_n
- |change in \vdash (? % ?) with (n*(exp n n1));
+ |change in \vdash (? % ?) with (n*(exp n n2));
rewrite > true_to_pi_p_Sn
[apply divides_times;assumption
|reflexivity]]]
|apply lt_O_fact
- |apply (witness ? ? n2);symmetry;assumption]]
+ |apply (witness ? ? n1);symmetry;assumption]]
|rewrite > divides_times_to_eq;
[apply eq_f2
[reflexivity
|elim x
[simplify;reflexivity
- |change in \vdash (? ? % ?) with (a*(exp a n1));
+ |change in \vdash (? ? % ?) with (a*(exp a n2));
rewrite > true_to_pi_p_Sn
[apply eq_f2
[reflexivity
|assumption]
|reflexivity]]]
|apply lt_O_fact
- |apply (witness ? ? n2);symmetry;assumption]]
+ |apply (witness ? ? n1);symmetry;assumption]]
|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 < H3;generalize in match H2;elim x
+ rewrite < H3;generalize in match H2; elim x
[rewrite < minus_n_O;simplify;rewrite < times_n_SO;reflexivity
|rewrite < fact_minus in H4;
[rewrite > true_to_pi_p_Sn
|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]
[elim H2;rewrite > H3;rewrite < times_exp;rewrite > sym_times in ⊢ (? ? (? (? ? ? (λ_:?.? ? %)) ?) ?);
rewrite > sym_times in ⊢ (? ? ? (? ? ? (λ_:?.? (? (? ? %) ?) ?)));
transitivity (sigma_p (S n) (λx:nat.true)
-(λk:nat.(exp n n)*(bc n k*(n)\sup(n-k)*(n2)\sup(n)))/exp n n)
+(λk:nat.(exp n n)*(bc n k*(n)\sup(n-k)*(n1)\sup(n)))/exp n n)
[apply eq_f2
[apply eq_sigma_p;intros;
[reflexivity
|rewrite < assoc_times;rewrite > sym_times;reflexivity]
|reflexivity]
- |rewrite < (distributive_times_plus_sigma_p ? ? ? (\lambda k.bc n k*(exp n (n-k))*(exp n2 n)));
+ |rewrite < (distributive_times_plus_sigma_p ? ? ? (\lambda k.bc n k*(exp n (n-k))*(exp n1 n)));
transitivity (sigma_p (S n) (λx:nat.true)
- (λk:nat.bc n k*(n2)\sup(n)*(n)\sup(n-k)))
+ (λk:nat.bc n k*(n1)\sup(n)*(n)\sup(n-k)))
[rewrite > (S_pred (exp n n))
[rewrite > div_times;apply eq_sigma_p;intros
[reflexivity
rewrite > sym_times;apply divides_times
[apply divides_SO_n
|elim (bc2 n i);
- [apply (witness ? ? n2);
+ [apply (witness ? ? n1);
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)!))
[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
apply divides_times
[apply divides_SO_n
|elim (bc2 (S n) i);
- [apply (witness ? ? n2);
+ [apply (witness ? ? n1);
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)!))
[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
projects / helm.git / blobdiff