From 52cfc3c337a48d52e9d2a8e4e761fa933f161103 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 5 Feb 2008 15:10:20 +0000 Subject: [PATCH] lower bound for neper's constant --- helm/software/matita/library/nat/neper.ma | 551 +++++++++++++++++++++- 1 file changed, 549 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma index 9378bd8de..bad55bc49 100644 --- a/helm/software/matita/library/nat/neper.ma +++ b/helm/software/matita/library/nat/neper.ma @@ -606,8 +606,555 @@ apply (trans_le ? (sigma_p (S n) apply le_log; [assumption |simplify;rewrite < times_n_SO;assumption]]] -qed. +qed. + +lemma neper_sigma_p1 : \forall n,a.n \divides a \to +exp (a * S n) n = +sigma_p (S n) (\lambda x.true) (\lambda k.(bc n k)*(exp n (n-k))*(exp a n)). +intros;rewrite < times_exp;rewrite > exp_S_sigma_p; +rewrite > distributive_times_plus_sigma_p; +apply eq_sigma_p;intros; + [reflexivity + |rewrite > sym_times;reflexivity;] +qed. + +lemma eq_exp_pi_p : \forall a,n.(exp a n) = pi_p n (\lambda x.true) (\lambda x.a). +intros;elim n + [simplify;reflexivity + |change in \vdash (? ? % ?) with (a*exp a n1);rewrite > true_to_pi_p_Sn + [apply eq_f2 + [reflexivity + |assumption] + |reflexivity]] +qed. +lemma eq_fact_pi_p : \forall n.n! = pi_p n (\lambda x.true) (\lambda x.S x). +intros;elim n + [simplify;reflexivity + |rewrite > true_to_pi_p_Sn + [change in \vdash (? ? % ?) with (S n1*n1!);apply eq_f2 + [reflexivity + |assumption] + |reflexivity]] +qed. + +lemma divides_pi_p : \forall m,n,p,f.m \leq n \to pi_p m p f \divides pi_p n p f. +intros;elim H + [apply divides_n_n + |apply (bool_elim ? (p n1));intro + [rewrite > true_to_pi_p_Sn + [rewrite > sym_times;rewrite > times_n_SO;apply divides_times + [assumption + |apply divides_SO_n] + |assumption] + |rewrite > false_to_pi_p_Sn;assumption]] +qed. + +lemma divides_fact_fact : \forall m,n.m \leq n \to m! \divides n!. +intros;do 2 rewrite > eq_fact_pi_p;apply divides_pi_p;assumption. +qed. + +lemma divides_times_to_eq : \forall a,b,c.O < c \to c \divides a \to a*b/c = a/c*b. +intros;elim H1;rewrite > H2;cases H;rewrite > assoc_times;do 2 rewrite > div_times; +reflexivity; +qed. + +lemma divides_pi_p_to_eq : \forall k,p,f,g.(\forall x.p x = true \to O < g x \land (g x \divides f x)) \to +pi_p k p f/pi_p k p g = pi_p k p (\lambda x.(f x)/(g x)). +intros; +cut (\forall k1.(pi_p k1 p g \divides pi_p k1 p f)) + [|intro;elim k1 + [simplify;apply divides_n_n + |apply (bool_elim ? (p n));intro; + [rewrite > true_to_pi_p_Sn + [rewrite > true_to_pi_p_Sn + [elim (H n) + [elim H4;elim H1;rewrite > H5;rewrite > H6; + rewrite < assoc_times;rewrite > assoc_times in ⊢ (? ? (? % ?)); + rewrite > sym_times in ⊢ (? ? (? (? ? %) ?)); + rewrite > assoc_times;rewrite > assoc_times; + apply divides_times + [apply divides_n_n + |rewrite > times_n_SO in \vdash (? % ?);apply divides_times + [apply divides_n_n + |apply divides_SO_n]] + |assumption] + |assumption] + |assumption] + |rewrite > false_to_pi_p_Sn + [rewrite > false_to_pi_p_Sn + [assumption + |assumption] + |assumption]]]] +elim k + [simplify;reflexivity + |apply (bool_elim ? (p n)) + [intro;rewrite > true_to_pi_p_Sn; + [rewrite > true_to_pi_p_Sn; + [rewrite > true_to_pi_p_Sn; + [elim (H n); + [elim H4;rewrite > H5;rewrite < eq_div_div_div_times; + [cases H3 + [rewrite > assoc_times;do 2 rewrite > div_times; + elim (Hcut n);rewrite > H6;rewrite < assoc_times; + rewrite < sym_times in \vdash (? ? (? (? % ?) ?) ?); + cut (O < pi_p n p g) + [rewrite < H1;rewrite > H6;cases Hcut1; + rewrite > assoc_times;do 2 rewrite > div_times;reflexivity + |elim n + [simplify;apply le_n + |apply (bool_elim ? (p n3));intro + [rewrite > true_to_pi_p_Sn + [rewrite > (times_n_O O);apply lt_times + [elim (H n3);assumption + |assumption] + |assumption] + |rewrite > false_to_pi_p_Sn;assumption]]] + |rewrite > assoc_times;do 2 rewrite > div_times; + elim (Hcut n);rewrite > H7;rewrite < assoc_times; + rewrite < sym_times in \vdash (? ? (? (? % ?) ?) ?); + cut (O < pi_p n p g) + [rewrite < H1;rewrite > H7;cases Hcut1; + rewrite > assoc_times;do 2 rewrite > div_times;reflexivity + |elim n + [simplify;apply le_n + |apply (bool_elim ? (p n3));intro + [rewrite > true_to_pi_p_Sn + [rewrite > (times_n_O O);apply lt_times + [elim (H n3);assumption + |assumption] + |assumption] + |rewrite > false_to_pi_p_Sn;assumption]]]] + |assumption + |(*già usata 2 volte: fattorizzare*) + elim n + [simplify;apply le_n + |apply (bool_elim ? (p n1));intro + [rewrite > true_to_pi_p_Sn + [rewrite > (times_n_O O);apply lt_times + [elim (H n1);assumption + |assumption] + |assumption] + |rewrite > false_to_pi_p_Sn;assumption]]] + |assumption] + |assumption] + |assumption] + |assumption] + |intro;rewrite > (false_to_pi_p_Sn ? ? ? H2); + rewrite > (false_to_pi_p_Sn ? ? ? H2);rewrite > (false_to_pi_p_Sn ? ? ? H2); + assumption]] +qed. + +lemma divides_times_to_divides_div : \forall a,b,c.O < b \to + a*b \divides c \to a \divides c/b. +intros;elim H1;rewrite > H2;rewrite > sym_times in \vdash (? ? (? (? % ?) ?)); +rewrite > assoc_times;cases H;rewrite > div_times;rewrite > times_n_SO in \vdash (? % ?); +apply divides_times + [1,3:apply divides_n_n + |*:apply divides_SO_n] +qed. + +lemma neper_sigma_p2 : \forall n,a.O < n \to n \divides a \to +sigma_p (S n) (\lambda x.true) (\lambda k.((bc n k)*(exp a n)*(exp n (n-k)))/(exp n n)) += sigma_p (S n) (\lambda x.true) +(\lambda k.(exp a (n-k))*(pi_p k (\lambda y.true) (\lambda i.a - (a*i/n)))/k!). +intros;apply eq_sigma_p;intros; + [reflexivity + |transitivity (bc n x*exp a n/exp n x) + [rewrite > minus_n_O in ⊢ (? ? (? ? (? ? %)) ?); + rewrite > (minus_n_n x); + 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; + [reflexivity + |*:apply lt_O_exp;assumption] + |apply le_n + |apply le_S_S_to_le;assumption] + |rewrite > minus_n_O in ⊢ (? ? (? (? ? (? ? %)) ?) ?); + rewrite > (minus_n_n x); + rewrite < (eq_plus_minus_minus_minus n x x); + [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 > sym_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?); + rewrite > assoc_times;rewrite > sym_times in ⊢ (? ? (? (? (? ? %) ?) ?) ?); + rewrite < eq_div_div_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 > Hcut1;rewrite < times_pi_p; + rewrite > divides_times_to_eq in \vdash (? ? % ?); + [rewrite > eq_div_div_div_times; + [rewrite > sym_times in ⊢ (? ? (? (? ? %) ?) ?); + rewrite < eq_div_div_div_times; + [cut (exp n x = pi_p x (\lambda i.true) (\lambda i.n)) + [rewrite > Hcut2;rewrite > divides_pi_p_to_eq + [rewrite > sym_times in \vdash (? ? ? %); + rewrite > divides_times_to_eq in \vdash (? ? ? %); + [apply eq_f2 + [apply eq_f2 + [apply eq_pi_p;intros + [reflexivity + |rewrite > sym_times; + rewrite > distr_times_minus;elim H1; + rewrite > H5;(* in ⊢ (? ? (? (? ? (? % ?)) ?) ?);*) + rewrite > sym_times;rewrite > assoc_times; + rewrite < distr_times_minus; + generalize in match H;cases n;intros + [elim (not_le_Sn_O ? H6) + |do 2 rewrite > div_times;reflexivity]] + |reflexivity] + |reflexivity] + |apply lt_O_fact + |cut (pi_p x (λy:nat.true) (λi:nat.a-a*i/n) = (exp a x)/(exp n x)*(n!/(n-x)!)) + [rewrite > Hcut3;rewrite > times_n_SO; + rewrite > sym_times;apply divides_times + [apply divides_SO_n; + |apply divides_times_to_divides_div; + [apply lt_O_fact + |apply bc2;apply le_S_S_to_le;assumption]] + |cut (pi_p x (\lambda y.true) (\lambda i. a - a*i/n) = + pi_p x (\lambda y.true) (\lambda i. a*(n-i)/n)) + [rewrite > Hcut3; + rewrite < (divides_pi_p_to_eq ? ? (\lambda i.(a*(n-i))) (\lambda i.n)) + [rewrite > (times_pi_p ? ? (\lambda i.a) (\lambda i.(n-i))); + rewrite > divides_times_to_eq; + [apply eq_f2 + [apply eq_f2;rewrite < eq_exp_pi_p;reflexivity + |rewrite < Hcut;rewrite > H3; + rewrite < sym_times in ⊢ (? ? ? (? (? % ?) ?)); + rewrite > (S_pred ((n-x)!)); + [rewrite > assoc_times; + rewrite > div_times;reflexivity + |apply lt_O_fact]] + |unfold lt;cut (1 = pi_p x (\lambda y.true) (\lambda y.1)) + [rewrite > Hcut4;apply le_pi_p;intros;assumption + |elim x + [simplify;reflexivity + |rewrite > true_to_pi_p_Sn; + [rewrite < H4;reflexivity + |reflexivity]]] + |elim x + [simplify;apply divides_SO_n + |rewrite > true_to_pi_p_Sn + [rewrite > true_to_pi_p_Sn + [apply divides_times;assumption + |reflexivity] + |reflexivity]]] + |intros;split + [assumption + |rewrite > times_n_SO;apply divides_times + [assumption + |apply divides_SO_n]]] + |apply eq_pi_p;intros; + [reflexivity + |elim H1;rewrite > H5;rewrite > (S_pred n); + [rewrite > assoc_times; + rewrite > assoc_times; + rewrite > div_times; + rewrite > div_times; + rewrite > distr_times_minus; + rewrite > sym_times; + reflexivity + |assumption]]]]] + |intros;split + [assumption + |rewrite > sym_times;rewrite > times_n_SO; + apply divides_times + [assumption + |apply divides_SO_n]]] + |rewrite < eq_exp_pi_p;reflexivity] + |apply lt_O_exp;assumption + |apply lt_O_fact] + |apply lt_O_fact + |apply lt_O_exp;assumption] + |apply lt_O_exp;assumption + |rewrite > (times_pi_p ? ? (\lambda x.(n-x)) (\lambda x.a)); + rewrite > divides_times_to_eq + [rewrite > times_n_SO;rewrite > sym_times;apply divides_times + [apply divides_SO_n + |elim x + [simplify;apply divides_SO_n + |change in \vdash (? % ?) with (n*(exp n n1)); + rewrite > true_to_pi_p_Sn + [apply divides_times;assumption + |reflexivity]]] + |apply lt_O_fact + |apply (witness ? ? n2);symmetry;assumption]] + |rewrite > divides_times_to_eq; + [apply eq_f2 + [reflexivity + |elim x + [simplify;reflexivity + |change in \vdash (? ? % ?) with (a*(exp a n1)); + rewrite > true_to_pi_p_Sn + [apply eq_f2 + [reflexivity + |assumption] + |reflexivity]]] + |apply lt_O_fact + |apply (witness ? ? n2);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 < minus_n_O;simplify;rewrite < times_n_SO;reflexivity + |rewrite < fact_minus in H4; + [rewrite > true_to_pi_p_Sn + [rewrite < assoc_times;rewrite > sym_times in \vdash (? ? ? (? % ?)); + apply H4;apply lt_to_le;assumption + |reflexivity] + |apply le_S_S_to_le;assumption]] + |apply lt_O_fact]] + |apply le_S_S_to_le;assumption] + |apply le_n + |apply le_S_S_to_le;assumption]]] +qed. + +lemma divides_sigma_p_to_eq : \forall k,p,f,b.O < b \to + (\forall x.p x = true \to b \divides f x) \to + (sigma_p k p f)/b = sigma_p k p (\lambda x. (f x)/b). +intros;cut (\forall k1.b \divides sigma_p k1 p f) + [|intro;elim k1 + [simplify;apply (witness ? ? O);rewrite < times_n_O;reflexivity + |apply (bool_elim ? (p n));intro + [rewrite > true_to_sigma_p_Sn; + [elim (H1 n); + [elim H2;rewrite > H4;rewrite > H5;rewrite < distr_times_plus; + rewrite > times_n_SO in \vdash (? % ?);apply divides_times + [apply divides_n_n + |apply divides_SO_n] + |assumption] + |assumption] + |rewrite > false_to_sigma_p_Sn;assumption]]] +elim k + [cases H;simplify;reflexivity + |apply (bool_elim ? (p n));intro + [rewrite > true_to_sigma_p_Sn + [rewrite > true_to_sigma_p_Sn + [elim (H1 n); + [elim (Hcut n);rewrite > H4;rewrite > H5;rewrite < distr_times_plus; + rewrite < H2;rewrite > H5;cases H;do 3 rewrite > div_times; + reflexivity + |assumption] + |assumption] + |assumption] + |do 2 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) = +sigma_p (S n) (\lambda x.true) +(\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; + [reflexivity + |apply lt_O_exp;assumption + |apply lt_O_exp;assumption] + |apply lt_O_exp;assumption + |apply lt_O_exp;assumption] + |apply eq_f2; + [rewrite > times_exp;rewrite > neper_sigma_p1 + [transitivity (sigma_p (S n) (λx:nat.true) (λk:nat.bc n k*(a)\sup(n)*(exp n (n-k))/(exp n n))) + [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) + [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))); + transitivity (sigma_p (S n) (λx:nat.true) + (λk:nat.bc n k*(n2)\sup(n)*(n)\sup(n-k))) + [rewrite > (S_pred (exp n n)) + [rewrite > div_times;apply eq_sigma_p;intros + [reflexivity + |rewrite > sym_times;rewrite > sym_times in ⊢ (? ? ? (? % ?)); + rewrite > assoc_times in \vdash (? ? ? %);reflexivity] + |apply lt_O_exp;assumption] + |apply eq_sigma_p;intros + [reflexivity + |rewrite < assoc_times;rewrite > assoc_times in \vdash (? ? ? %); + rewrite > sym_times in \vdash (? ? ? (? (? ? %) ?)); + rewrite < assoc_times;rewrite > sym_times in \vdash (? ? ? %); + rewrite > (S_pred (exp n n)) + [rewrite > div_times;reflexivity + |apply lt_O_exp;assumption]]]] + |rewrite > neper_sigma_p2; + [reflexivity + |assumption + |assumption]] + |assumption] + |reflexivity]] +qed. + +theorem neper_monotonic : \forall n. O < n \to +(exp (S n) n)/(exp n n) \leq (exp (S (S n)) (S n))/(exp (S n) (S n)). +intros;rewrite > (neper_sigma_p3 (n*S n) n) + [rewrite > (neper_sigma_p3 (n*S n) (S n)) + [change in ⊢ (? ? (? ? %)) with ((n * S n)*(exp (n * S n) n)); + rewrite < eq_div_div_div_times + [apply monotonic_div; + [apply lt_O_exp;rewrite > (times_n_O O);apply lt_times + [assumption + |apply lt_O_S] + |apply le_times_to_le_div + [rewrite > (times_n_O O);apply lt_times + [assumption + |apply lt_O_S] + |rewrite > distributive_times_plus_sigma_p; + apply (trans_le ? (sigma_p (S n) (λx:nat.true) + (λk:nat.((n*S n))\sup(S n-k)*pi_p k (λy:nat.true) (λi:nat.n*S n-n*S n*i/S n)/k!))) + [apply le_sigma_p;intros;rewrite > sym_times in ⊢ (? (? ? %) ?); + rewrite > sym_times in \vdash (? ? (? % ?)); + rewrite > divides_times_to_eq in \vdash (? ? %) + [rewrite > divides_times_to_eq in \vdash (? % ?) + [rewrite > sym_times in \vdash (? (? ? %) ?); + rewrite < assoc_times; + rewrite > sym_times in \vdash (? ? %); + rewrite > minus_Sn_m; + [apply le_times_r;apply monotonic_div + [apply lt_O_fact + |apply le_pi_p;intros;apply monotonic_le_minus_r; + rewrite > assoc_times in \vdash (? % ?); + rewrite > sym_times in \vdash (? % ?); + rewrite > assoc_times in \vdash (? % ?); + rewrite > div_times; + rewrite > (S_pred n) in \vdash (? ? %); + [rewrite > assoc_times;rewrite > div_times; + rewrite < S_pred + [rewrite > sym_times;apply le_times_l;apply le_S;apply le_n + |assumption] + |assumption]] + |apply le_S_S_to_le;assumption] + |apply lt_O_fact + |cut (pi_p i (λy:nat.true) (λi:nat.n*S n-n*S n*i/n) = + pi_p i (\lambda y.true) (\lambda i.S n) * + pi_p i (\lambda y.true) (\lambda i.(n-i))) + [rewrite > Hcut;rewrite > times_n_SO; + rewrite > sym_times;apply divides_times + [apply divides_SO_n + |elim (bc2 n i); + [apply (witness ? ? n2); + 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 > assoc_times;rewrite > div_times; + reflexivity + |apply lt_O_fact] + |generalize in match H1;elim i + [rewrite < minus_n_O;rewrite > div_n_n; + [reflexivity + |apply lt_O_fact] + |rewrite > true_to_pi_p_Sn + [rewrite > H4 + [rewrite > sym_times;rewrite < divides_times_to_eq + [rewrite < fact_minus + [rewrite > sym_times; + rewrite < eq_div_div_times + [reflexivity + |apply lt_to_lt_O_minus;apply le_S_S_to_le; + assumption + |apply lt_O_fact;] + |apply le_S_S_to_le;assumption] + |apply lt_O_fact + |apply divides_fact_fact; + apply le_plus_to_minus; + rewrite > plus_n_O in \vdash (? % ?); + apply le_plus_r;apply le_O_n] + |apply lt_to_le;assumption] + |reflexivity]]] + |apply le_S_S_to_le;assumption]] + |rewrite < times_pi_p;apply eq_pi_p;intros; + [reflexivity + |rewrite > distr_times_minus;rewrite > assoc_times; + rewrite > (S_pred n) in \vdash (? ? (? ? (? (? % ?) %)) ?) + [rewrite > div_times;rewrite > sym_times;reflexivity + |assumption]]]] + |apply lt_O_fact + |cut (pi_p i (λy:nat.true) (λi:nat.n*S n-n*S n*i/S n) = + pi_p i (\lambda y.true) (\lambda i.n) * + pi_p i (\lambda y.true) (\lambda i.(S n-i))) + [rewrite > Hcut;rewrite > times_n_SO;rewrite > sym_times; + apply divides_times + [apply divides_SO_n + |elim (bc2 (S n) i); + [apply (witness ? ? n2); + 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 > assoc_times;rewrite > div_times; + reflexivity + |apply lt_O_fact] + |generalize in match H1;elim i + [rewrite < minus_n_O;rewrite > div_n_n; + [reflexivity + |apply lt_O_fact] + |rewrite > true_to_pi_p_Sn + [rewrite > H4 + [rewrite > sym_times;rewrite < divides_times_to_eq + [rewrite < fact_minus + [rewrite > sym_times; + rewrite < eq_div_div_times + [reflexivity + |apply lt_to_lt_O_minus;apply lt_to_le; + assumption + |apply lt_O_fact] + |apply lt_to_le;assumption] + |apply lt_O_fact + |apply divides_fact_fact; + apply le_plus_to_minus; + rewrite > plus_n_O in \vdash (? % ?); + apply le_plus_r;apply le_O_n] + |apply lt_to_le;assumption] + |reflexivity]]] + |apply lt_to_le;assumption]] + |rewrite < times_pi_p;apply eq_pi_p;intros; + [reflexivity + |rewrite > distr_times_minus;rewrite > sym_times in \vdash (? ? (? ? (? (? % ?) ?)) ?); + rewrite > assoc_times;rewrite > div_times;reflexivity]]] + |rewrite > true_to_sigma_p_Sn in \vdash (? ? %) + [rewrite > sym_plus;rewrite > plus_n_O in \vdash (? % ?); + apply le_plus_r;apply le_O_n + |reflexivity]]]] + |rewrite > (times_n_O O);apply lt_times + [assumption + |apply lt_O_S] + |apply lt_O_exp;rewrite > (times_n_O O);apply lt_times + [assumption + |apply lt_O_S]] + |rewrite > (times_n_O O);apply lt_times + [assumption + |apply lt_O_S] + |apply lt_O_S + |apply (witness ? ? n);apply sym_times] + |rewrite > (times_n_O O);apply lt_times + [assumption + |apply lt_O_S] + |assumption + |apply (witness ? ? (S n));reflexivity] +qed. + +theorem le_SSO_neper : \forall n.O < n \to (2 \leq (exp (S n) n)/(exp n n)). +intros;elim H + [simplify;apply le_n + |apply (trans_le ? ? ? H2);apply neper_monotonic;assumption] +qed. + +theorem le_SSO_exp_neper : \forall n.O < n \to 2*(exp n n) \leq exp (S n) n. +intros;apply (trans_le ? ((exp (S n) n)/(exp n n)*(exp n n))) + [apply le_times_l;apply le_SSO_neper;assumption + |rewrite > sym_times;apply (trans_le ? ? ? (le_times_div_div_times ? ? ? ?)) + [apply lt_O_exp;assumption + |cases (lt_O_exp ? n H);rewrite > div_times;apply le_n]] +qed. + (* 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 @@ -744,4 +1291,4 @@ apply (lt_to_le_to_lt ? (sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k) ] ] qed. -*) \ No newline at end of file +*) -- 2.39.2