X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fchebyshev.ma;h=6ef8624e4983922e9d8276633f72a6d0163d42fc;hb=c99a38b6539be1eb667cced1eed2db3fc75e3162;hp=c06675d0e2d3db98e1019496b3ed94887609fba5;hpb=fb3cf5acfd87741651c5e30ad1911a08e26f6c69;p=helm.git diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma index c06675d0e..6ef8624e4 100644 --- a/helm/software/matita/library/nat/chebyshev.ma +++ b/helm/software/matita/library/nat/chebyshev.ma @@ -12,16 +12,212 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/chebishev". - include "nat/log.ma". include "nat/pi_p.ma". include "nat/factorization.ma". include "nat/factorial2.ma". definition prim: nat \to nat \def -\lambda n. sigma_p (S n) primeb (\lambda p.(S O)). +\lambda n. sigma_p (S n) primeb (\lambda p.1). + +theorem le_prim_n: \forall n. prim n \le n. +intros.unfold prim. elim n + [apply le_n + |apply (bool_elim ? (primeb (S n1)));intro + [rewrite > true_to_sigma_p_Sn + [rewrite > sym_plus. + rewrite < plus_n_Sm. + rewrite < plus_n_O. + apply le_S_S.assumption + |assumption + ] + |rewrite > false_to_sigma_p_Sn + [apply le_S.assumption + |assumption + ] + ] + ] +qed. +theorem not_prime_times_SSO: \forall n. 1 < n \to \lnot prime (2*n). +intros.intro.elim H1. +absurd (2 = 2*n) + [apply H3 + [apply (witness ? ? n).reflexivity + |apply le_n + ] + |apply lt_to_not_eq. + rewrite > times_n_SO in ⊢ (? % ?). + apply lt_times_r. + assumption + ] +qed. + +theorem eq_prim_prim_pred: \forall n. 1 < n \to +(prim (2*n)) = (prim (pred (2*n))). +intros.unfold prim. +rewrite < S_pred + [rewrite > false_to_sigma_p_Sn + [reflexivity + |apply not_prime_to_primeb_false. + apply not_prime_times_SSO. + assumption + ] + |apply (trans_lt ? (2*1)) + [simplify.apply lt_O_S + |apply lt_times_r. + assumption + ] + ] +qed. + +theorem le_prim_n1: \forall n. 4 \le n \to prim (S(2*n)) \le n. +intros.unfold prim. elim H + [simplify.apply le_n + |cut (sigma_p (2*S n1) primeb (λp:nat.1) = sigma_p (S (2*S n1)) primeb (λp:nat.1)) + [apply (bool_elim ? (primeb (S(2*(S n1)))));intro + [rewrite > true_to_sigma_p_Sn + [rewrite > sym_plus. + rewrite < plus_n_Sm. + rewrite < plus_n_O. + apply le_S_S. + rewrite < Hcut. + rewrite > times_SSO. + assumption + |assumption + ] + |rewrite > false_to_sigma_p_Sn + [apply le_S. + rewrite < Hcut. + rewrite > times_SSO. + assumption + |assumption + ] + ] + |apply sym_eq.apply (eq_prim_prim_pred (S n1)). + apply le_S_S.apply (trans_le ? 4) + [apply leb_true_to_le.reflexivity + |assumption + ] + ] + ] +qed. + +(* usefull to kill a successor in bertrand *) +theorem le_prim_n2: \forall n. 7 \le n \to prim (S(2*n)) \le pred n. +intros.unfold prim. elim H + [apply leb_true_to_le.reflexivity. + |cut (sigma_p (2*S n1) primeb (λp:nat.1) = sigma_p (S (2*S n1)) primeb (λp:nat.1)) + [apply (bool_elim ? (primeb (S(2*(S n1)))));intro + [rewrite > true_to_sigma_p_Sn + [rewrite > sym_plus. + rewrite < plus_n_Sm. + rewrite < plus_n_O. + simplify in ⊢ (? ? %). + rewrite > S_pred in ⊢ (? ? %) + [apply le_S_S. + rewrite < Hcut. + rewrite > times_SSO. + assumption + |apply (ltn_to_ltO ? ? H1) + ] + |assumption + ] + |rewrite > false_to_sigma_p_Sn + [simplify in ⊢ (? ? %). + apply (trans_le ? ? ? ? (le_pred_n n1)). + rewrite < Hcut. + rewrite > times_SSO. + assumption + |assumption + ] + ] + |apply sym_eq.apply (eq_prim_prim_pred (S n1)). + apply le_S_S.apply (trans_le ? 4) + [apply leb_true_to_le.reflexivity + |apply (trans_le ? ? ? ? H1). + apply leb_true_to_le.reflexivity + ] + ] + ] +qed. + +(* da spostare *) +theorem le_pred: \forall n,m. n \le m \to pred n \le pred m. +apply nat_elim2;intros + [apply le_O_n + |apply False_ind.apply (le_to_not_lt ? ? H). + apply lt_O_S + |simplify.apply le_S_S_to_le.assumption + ] +qed. + +(* la prova potrebbe essere migliorata *) +theorem le_prim_n3: \forall n. 15 \le n \to +prim n \le pred (n/2). +intros. +elim (or_eq_eq_S (pred n)). +elim H1 + [cut (n = S (2*a)) + [rewrite > Hcut. + apply (trans_le ? (pred a)) + [apply le_prim_n2. + apply (le_times_to_le 2) + [apply le_n_Sn + |apply le_S_S_to_le. + rewrite < Hcut. + assumption + ] + |apply le_pred. + apply le_times_to_le_div + [apply lt_O_S + |apply le_n_Sn + ] + ] + |rewrite < H2. + apply S_pred. + apply (ltn_to_ltO ? ? H) + ] + |cut (n=2*(S a)) + [rewrite > Hcut. + rewrite > eq_prim_prim_pred + [rewrite > times_SSO in ⊢ (? % ?). + change in ⊢ (? (? %) ?) with (S (2*a)). + rewrite > sym_times in ⊢ (? ? (? (? % ?))). + rewrite > lt_O_to_div_times + [apply (trans_le ? (pred a)) + [apply le_prim_n2. + apply le_S_S_to_le. + apply (lt_times_to_lt 2) + [apply le_n_Sn + |apply le_S_S_to_le. + rewrite < Hcut. + apply le_S_S. + assumption + ] + |apply le_pred. + apply le_n_Sn + ] + |apply lt_O_S + ] + |apply le_S_S. + apply not_lt_to_le.intro. + apply (le_to_not_lt ? ? H). + rewrite > Hcut. + lapply (le_S_S_to_le ? ? H3) as H4. + apply (le_n_O_elim ? H4). + apply leb_true_to_le.reflexivity + ] + |rewrite > times_SSO. + rewrite > S_pred + [apply eq_f.assumption + |apply (ltn_to_ltO ? ? H) + ] + ] + ] +qed. + +(* This is chebishev psi function *) definition A: nat \to nat \def \lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)). @@ -79,6 +275,7 @@ elim (le_to_or_lt_eq ? ? (le_O_n n)) ] qed. +(* an equivalent formulation for psi *) definition A': nat \to nat \def \lambda n. pi_p (S n) primeb (\lambda p.(pi_p (log p n) (\lambda i.true) (\lambda i.p))). @@ -134,7 +331,7 @@ elim n ] ] qed. - + theorem lt_max_to_pi_p_primeb: \forall q,m. O < m \to max m (\lambda i.primeb i \land divides_b i m) < q \to m = pi_p q (\lambda i.primeb i \land divides_b i m) (\lambda p.exp p (ord m p)). intro.elim q @@ -327,7 +524,8 @@ intro.elim q ] ] qed. - + +(* factorization of n into primes *) theorem pi_p_primeb_divides_b: \forall n. O < n \to n = pi_p (S n) (\lambda i.primeb i \land divides_b i n) (\lambda p.exp p (ord n p)). intros. @@ -346,7 +544,7 @@ apply pi_p_primeb_divides_b. assumption. qed. -theorem le_ord_log: \forall n,p. O < n \to S O < p \to +theorem le_ord_log: \forall n,p. O < n \to 1 < p \to ord n p \le log p n. intros. rewrite > (exp_ord p) in ⊢ (? ? (? ? %)) @@ -457,7 +655,7 @@ qed. theorem eq_ord_sigma_p: \forall n,m,x. O < n \to prime x \to exp x m \le n \to n < exp x (S m) \to -ord n x=sigma_p m (λi:nat.divides_b (x\sup (S i)) n) (λx:nat.S O). +ord n x=sigma_p m (λi:nat.divides_b (x\sup (S i)) n) (λx:nat.1). intros. lapply (prime_to_lt_SO ? H1). rewrite > (exp_ord x n) in ⊢ (? ? ? (? ? (λi:?.? ? %) ?)) @@ -505,6 +703,7 @@ apply eq_pi_p1 ] qed. +(* the factorial function *) theorem eq_fact_pi_p:\forall n. fact n = pi_p (S n) (\lambda i.leb (S O) i) (\lambda i.i). intro.elim n @@ -590,6 +789,7 @@ apply (div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q)) ] qed. +(* still another characterization of the factorial *) theorem fact_pi_p: \forall n. fact n = pi_p (S n) primeb (\lambda p.(pi_p (log p n) @@ -597,20 +797,20 @@ pi_p (S n) primeb intros. rewrite > eq_fact_pi_p. apply (trans_eq ? ? - (pi_p (S n) (λi:nat.leb (S O) i) - (λn.pi_p (S n) primeb - (\lambda p.(pi_p (log p n) - (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p)))))) + (pi_p (S n) (λm:nat.leb (S O) m) + (λm.pi_p (S m) primeb + (\lambda p.(pi_p (log p m) + (\lambda i.divides_b (exp p (S i)) m) (\lambda i.p)))))) [apply eq_pi_p1;intros [reflexivity |apply pi_p_primeb1. apply leb_true_to_le.assumption ] |apply (trans_eq ? ? - (pi_p (S n) (λi:nat.leb (S O) i) - (λn:nat - .pi_p (S n) (\lambda p.primeb p\land leb p n) - (λp:nat.pi_p (log p n) (λi:nat.divides_b ((p)\sup(S i)) n) (λi:nat.p))))) + (pi_p (S n) (λm:nat.leb (S O) m) + (λm:nat + .pi_p (S m) (\lambda p.primeb p\land leb p m) + (λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p))))) [apply eq_pi_p1 [intros.reflexivity |intros.apply eq_pi_p1 @@ -625,7 +825,7 @@ apply (trans_eq ? ? ] ] |apply (trans_eq ? ? - (pi_p (S n) (λi:nat.leb (S O) i) + (pi_p (S n) (λm:nat.leb (S O) m) (λm:nat .pi_p (S n) (λp:nat.primeb p∧leb p m) (λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p))))) @@ -676,13 +876,6 @@ apply (trans_eq ? ? [apply prime_to_lt_SO. apply primeb_true_to_prime. assumption - |apply (lt_to_le_to_lt ? x) - [apply prime_to_lt_O. - apply primeb_true_to_prime. - assumption - |apply leb_true_to_le. - assumption - ] |apply le_S_S_to_le. assumption ] @@ -816,10 +1009,10 @@ intro.elim n | *) -theorem fact_pi_p2: \forall n. fact ((S(S O))*n) = -pi_p (S ((S(S O))*n)) primeb - (\lambda p.(pi_p (log p ((S(S O))*n)) - (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))*(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O)))))))). +theorem fact_pi_p2: \forall n. fact (2*n) = +pi_p (S (2*n)) primeb + (\lambda p.(pi_p (log p (2*n)) + (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i))))*(exp p (mod (2*n /(exp p (S i))) 2)))))). intros.rewrite > fact_pi_p. apply eq_pi_p1 [intros.reflexivity @@ -838,13 +1031,13 @@ apply eq_pi_p1 ] qed. -theorem fact_pi_p3: \forall n. fact ((S(S O))*n) = -pi_p (S ((S(S O))*n)) primeb - (\lambda p.(pi_p (log p ((S(S O))*n)) - (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))* -pi_p (S ((S(S O))*n)) primeb - (\lambda p.(pi_p (log p ((S(S O))*n)) - (\lambda i.true) (\lambda i.(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O))))))). +theorem fact_pi_p3: \forall n. fact (2*n) = +pi_p (S (2*n)) primeb + (\lambda p.(pi_p (log p (2*n)) + (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i))))))))* +pi_p (S (2*n)) primeb + (\lambda p.(pi_p (log p (2*n)) + (\lambda i.true) (\lambda i.(exp p (mod (2*n /(exp p (S i))) 2))))). intros. rewrite < times_pi_p. rewrite > fact_pi_p2. @@ -854,14 +1047,14 @@ apply eq_pi_p;intros ] qed. -theorem pi_p_primeb4: \forall n. S O < n \to -pi_p (S ((S(S O))*n)) primeb - (\lambda p.(pi_p (log p ((S(S O))*n)) - (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))) +theorem pi_p_primeb4: \forall n. 1 < n \to +pi_p (S (2*n)) primeb + (\lambda p.(pi_p (log p (2*n)) + (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i)))))))) = pi_p (S n) primeb - (\lambda p.(pi_p (log p (S(S O)*n)) - (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))). + (\lambda p.(pi_p (log p (2*n)) + (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i)))))))). intros. apply or_false_eq_SO_to_eq_pi_p [apply le_S_S. @@ -883,14 +1076,14 @@ apply or_false_eq_SO_to_eq_pi_p ] qed. -theorem pi_p_primeb5: \forall n. S O < n \to -pi_p (S ((S(S O))*n)) primeb +theorem pi_p_primeb5: \forall n. 1 < n \to +pi_p (S (2*n)) primeb (\lambda p.(pi_p (log p ((S(S O))*n)) - (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))) + (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i)))))))) = pi_p (S n) primeb (\lambda p.(pi_p (log p n) - (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))). + (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i)))))))). intros. rewrite > (pi_p_primeb4 ? H). apply eq_pi_p1;intros @@ -900,7 +1093,6 @@ apply eq_pi_p1;intros [apply prime_to_lt_SO. apply primeb_true_to_prime. assumption - |apply lt_to_le.assumption |apply le_times_n. apply lt_O_S ] @@ -926,11 +1118,11 @@ apply eq_pi_p1;intros qed. theorem exp_fact_SSO: \forall n. -exp (fact n) (S(S O)) +exp (fact n) 2 = pi_p (S n) primeb (\lambda p.(pi_p (log p n) - (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))). + (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i)))))))). intros. rewrite > fact_pi_p. rewrite < exp_pi_p. @@ -947,8 +1139,32 @@ pi_p (S n) primeb (\lambda p.(pi_p (log p n) (\lambda i.true) (\lambda i.(exp p (mod (n /(exp p (S i))) (S(S O))))))). +theorem B_SSSO: B 3 = 6. +reflexivity. +qed. + +theorem B_SSSSO: B 4 = 6. +reflexivity. +qed. + +theorem B_SSSSSO: B 5 = 30. +reflexivity. +qed. + +theorem B_SSSSSSO: B 6 = 20. +reflexivity. +qed. + +theorem B_SSSSSSSO: B 7 = 140. +reflexivity. +qed. + +theorem B_SSSSSSSSO: B 8 = 70. +reflexivity. +qed. + theorem eq_fact_B:\forall n.S O < n \to -fact ((S(S O))*n) = exp (fact n) (S(S O)) * B((S(S O))*n). +fact (2*n) = exp (fact n) 2 * B(2*n). intros. unfold B. rewrite > fact_pi_p3. apply eq_f2 @@ -978,18 +1194,101 @@ apply le_exp ] qed. +theorem le_B_A4: \forall n. O < n \to (S(S O))* B ((S(S(S(S O))))*n) \le A ((S(S(S(S O))))*n). +intros.unfold B. +rewrite > eq_A_A'. +unfold A'. +cut ((S(S O)) < (S ((S(S(S(S O))))*n))) + [cut (O (pi_p_gi ? ? (S(S O))) + [rewrite > (pi_p_gi ? ? (S(S O))) in ⊢ (? ? %) + [rewrite < assoc_times. + apply le_times + [rewrite > (pi_p_gi ? ? O) + [rewrite > (pi_p_gi ? ? O) in ⊢ (? ? %) + [rewrite < assoc_times. + apply le_times + [rewrite < exp_n_SO. + change in ⊢ (? (? ? (? ? (? (? (? % ?) ?) ?))) ?) + with ((S(S O))*(S(S O))). + rewrite > assoc_times. + rewrite > sym_times in ⊢ (? (? ? (? ? (? (? % ?) ?))) ?). + rewrite > lt_O_to_div_times + [rewrite > divides_to_mod_O + [apply le_n + |apply lt_O_S + |apply (witness ? ? n).reflexivity + ] + |apply lt_O_S + ] + |apply le_pi_p.intros. + rewrite > exp_n_SO in ⊢ (? ? %). + apply le_exp + [apply lt_O_S + |apply le_S_S_to_le. + apply lt_mod_m_m. + apply lt_O_S + ] + ] + |assumption + |reflexivity + ] + |assumption + |reflexivity + ] + |apply le_pi_p.intros. + apply le_pi_p.intros. + rewrite > exp_n_SO in ⊢ (? ? %). + apply le_exp + [apply prime_to_lt_O. + apply primeb_true_to_prime. + apply (andb_true_true ? ? H2) + |apply le_S_S_to_le. + apply lt_mod_m_m. + apply lt_O_S + ] + ] + |assumption + |reflexivity + ] + |assumption + |reflexivity + ] + |apply lt_O_log + [rewrite > (times_n_O (S(S(S(S O))))) in ⊢ (? % ?). + apply lt_times_r1 + [apply lt_O_S + |assumption + ] + |rewrite > times_n_SO in ⊢ (? % ?). + apply le_times + [apply le_S.apply le_S.apply le_n + |assumption + ] + ] + ] + |apply le_S_S. + rewrite > times_n_SO in ⊢ (? % ?). + apply le_times + [apply le_S.apply le_n_Sn + |assumption + ] + ] +qed. + +(* not usefull theorem le_fact_A:\forall n.S O < n \to -fact ((S(S O))*n) \le exp (fact n) (S(S O)) * A ((S(S O))*n). +fact (2*n) \le exp (fact n) 2 * A (2*n). intros. rewrite > eq_fact_B [apply le_times_r. apply le_B_A |assumption ] -qed. +qed. *) theorem lt_SO_to_le_B_exp: \forall n.S O < n \to -B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n). +B (2*n) \le exp 2 (pred (2*n)). intros. apply (le_times_to_le (exp (fact n) (S(S O)))) [apply lt_O_exp. @@ -1005,21 +1304,66 @@ apply (le_times_to_le (exp (fact n) (S(S O)))) qed. theorem le_B_exp: \forall n. -B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n). +B (2*n) \le exp 2 (pred (2*n)). intro.cases n [apply le_n |cases n1 - [simplify.apply le_S.apply le_S.apply le_n + [simplify.apply le_n |apply lt_SO_to_le_B_exp. apply le_S_S.apply lt_O_S. ] ] qed. +theorem lt_SSSSO_to_le_B_exp: \forall n.4 < n \to +B (2*n) \le exp 2 ((2*n)-2). +intros. +apply (le_times_to_le (exp (fact n) (S(S O)))) + [apply lt_O_exp. + apply lt_O_fact + |rewrite < eq_fact_B + [rewrite < sym_times in ⊢ (? ? %). + rewrite > exp_SSO. + rewrite < assoc_times. + apply lt_SSSSO_to_fact.assumption + |apply lt_to_le.apply lt_to_le. + apply lt_to_le.assumption + ] + ] +qed. + +theorem lt_SO_to_le_exp_B: \forall n. 1 < n \to +exp 2 (2*n) \le 2 * n * B (2*n). +intros. +apply (le_times_to_le (exp (fact n) (S(S O)))) + [apply lt_O_exp. + apply lt_O_fact + |rewrite < assoc_times in ⊢ (? ? %). + rewrite > sym_times in ⊢ (? ? (? % ?)). + rewrite > assoc_times in ⊢ (? ? %). + rewrite < eq_fact_B + [rewrite < sym_times. + apply fact3. + apply lt_to_le.assumption + |assumption + ] + ] +qed. + +theorem le_exp_B: \forall n. O < n \to +exp 2 (2*n) \le 2 * n * B (2*n). +intros. +elim H + [apply le_n + |apply lt_SO_to_le_exp_B. + apply le_S_S.assumption + ] +qed. + theorem eq_A_SSO_n: \forall n.O < n \to -A((S(S O))*n) = - pi_p (S ((S(S O))*n)) primeb - (\lambda p.(pi_p (log p ((S(S O))*n) ) +A(2*n) = + pi_p (S (2*n)) primeb + (\lambda p.(pi_p (log p (2*n) ) (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i)))))))) *A n. intro. @@ -1088,7 +1432,6 @@ cut ( [apply prime_to_lt_SO. apply primeb_true_to_prime. assumption - |assumption |simplify. apply le_plus_n_r ] @@ -1116,7 +1459,7 @@ cut ( qed. theorem le_A_BA1: \forall n. O < n \to -A((S(S O))*n) \le B((S(S O))*n)*A n. +A(2*n) \le B(2*n)*A n. intros. rewrite > eq_A_SSO_n [apply le_times_l. @@ -1142,8 +1485,7 @@ rewrite > eq_A_SSO_n assumption |cut (i\sup(S i1)≤(S(S O))*n) [apply div_mod_spec_intro - [alias id "lt_plus_to_lt_minus" = "cic:/matita/nat/map_iter_p.ma/lt_plus_to_lt_minus.con". - apply lt_plus_to_lt_minus + [apply lt_plus_to_lt_minus [assumption |simplify in ⊢ (? % ?). rewrite < plus_n_O. @@ -1190,521 +1532,792 @@ intros.cases n qed. theorem le_A_exp: \forall n. -A((S(S O))*n) \le (exp (S(S O)) ((S(S O)*n)))*A n. +A(2*n) \le (exp 2 (pred (2*n)))*A n. intro. -apply (trans_le ? (B((S(S O))*n)*A n)) +apply (trans_le ? (B(2*n)*A n)) [apply le_A_BA |apply le_times_l. apply le_B_exp ] qed. -(* da spostare *) -theorem times_exp: \forall n,m,p.exp n p * exp m p = exp (n*m) p. -intros.elim p - [reflexivity - |simplify.autobatch +theorem lt_SSSSO_to_le_A_exp: \forall n. 4 < n \to +A(2*n) \le exp 2 ((2*n)-2)*A n. +intros. +apply (trans_le ? (B(2*n)*A n)) + [apply le_A_BA + |apply le_times_l. + apply lt_SSSSO_to_le_B_exp.assumption ] qed. -theorem le_exp_log: \forall p,n. O < n \to -exp p ( -log n) \le n. -intros. -apply leb_true_to_le. -unfold log. -apply (f_max_true (\lambda x.leb (exp p x) n)). -apply (ex_intro ? ? O). -split - [apply le_O_n - |apply le_to_leb_true.simplify.assumption +theorem times_SSO_pred: \forall n. 2*(pred n) \le pred (2*n). +intro.cases n + [apply le_n + |simplify.apply le_plus_r. + apply le_n_Sn ] qed. -theorem lt_log_n_n: \forall n. O < n \to log n < n. +theorem le_S_times_SSO: \forall n. O < n \to S n \le 2*n. intros. -cut (log n \le n) - [elim (le_to_or_lt_eq ? ? Hcut) +elim H + [apply le_n + |rewrite > times_SSO. + apply le_S_S. + apply (trans_le ? (2*n1)) [assumption - |absurd (exp (S(S O)) n \le n) - [rewrite < H1 in ⊢ (? (? ? %) ?). - apply le_exp_log. + |apply le_n_Sn + ] + ] +qed. + +theorem le_A_exp1: \forall n. +A(exp 2 n) \le (exp 2 ((2*(exp 2 n)-(S(S n))))). +intro.elim n + [simplify.apply le_n + |change in ⊢ (? % ?) with (A(2*(exp 2 n1))). + apply (trans_le ? ((exp 2 (pred(2*(exp (S(S O)) n1))))*A (exp (S(S O)) n1))) + [apply le_A_exp + |apply (trans_le ? ((2)\sup(pred (2*(2)\sup(n1)))*(2)\sup(2*(2)\sup(n1)-S (S n1)))) + [apply le_times_r. assumption - |apply lt_to_not_le. - apply lt_m_exp_nm. - apply le_n + |rewrite < exp_plus_times. + apply le_exp + [apply lt_O_S + |cut (S(S n1) \le 2*(exp 2 n1)) + [apply le_S_S_to_le. + change in ⊢ (? % ?) with (S(pred (2*(2)\sup(n1)))+(2*(2)\sup(n1)-S (S n1))). + rewrite < S_pred + [rewrite > eq_minus_S_pred in ⊢ (? ? %). + rewrite < S_pred + [rewrite < eq_minus_plus_plus_minus + [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?). + apply le_n + |assumption + ] + |apply lt_to_lt_O_minus. + apply (lt_to_le_to_lt ? (2*(S(S n1)))) + [rewrite > times_n_SO in ⊢ (? % ?). + rewrite > sym_times. + apply lt_times_l1 + [apply lt_O_S + |apply le_n + ] + |apply le_times_r. + assumption + ] + ] + |unfold.rewrite > times_n_SO in ⊢ (? % ?). + apply le_times + [apply le_n_Sn + |apply lt_O_exp. + apply lt_O_S + ] + ] + |elim n1 + [apply le_n + |apply (trans_le ? (2*(S(S n2)))) + [apply le_S_times_SSO. + apply lt_O_S + |apply le_times_r. + assumption + ] + ] + ] + ] ] ] - |unfold log.apply le_max_n ] qed. -theorem le_log_n_n: \forall n. log n \le n. -intro. -cases n +theorem monotonic_A: monotonic nat le A. +unfold.intros. +elim H [apply le_n - |apply lt_to_le. - apply lt_log_n_n. - apply lt_O_S + |apply (trans_le ? (A n1)) + [assumption + |unfold A. + cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1)) + ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1)))) + [apply (bool_elim ? (primeb (S n1)));intro + [rewrite > (true_to_pi_p_Sn ? ? ? H3). + rewrite > times_n_SO in ⊢ (? % ?). + rewrite > sym_times. + apply le_times + [apply lt_O_exp.apply lt_O_S + |assumption + ] + |rewrite > (false_to_pi_p_Sn ? ? ? H3). + assumption + ] + |apply le_pi_p.intros. + apply le_exp + [apply prime_to_lt_O. + apply primeb_true_to_prime. + assumption + |apply le_log + [apply prime_to_lt_SO. + apply primeb_true_to_prime. + assumption + |apply le_S.apply le_n + ] + ] + ] + ] ] qed. -theorem lt_exp_log: \forall n. n < exp (S(S O)) (S (log n)). -intro.cases n - [simplify.apply le_S.apply le_n - |apply not_le_to_lt. - apply leb_false_to_not_le. - apply (lt_max_to_false ? (S n1) (S (log (S n1)))) - [apply le_S_S.apply le_n - |apply lt_log_n_n.apply lt_O_S +(* +theorem le_A_exp2: \forall n. O < n \to +A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)). +intros. +apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n))))) + [apply monotonic_A. + apply lt_to_le. + apply lt_exp_log. + apply le_n + |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n))))))) + [apply le_A_exp1 + |apply le_exp + [apply lt_O_S + |rewrite > assoc_times.apply le_times_r. + change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n). + apply le_times_r. + apply le_exp_log. + assumption + ] ] ] qed. +*) -theorem f_false_to_le_max: \forall f,n,p. (∃i:nat.i≤n∧f i=true) \to -(\forall m. p < m \to f m = false) -\to max n f \le p. -intros. -apply not_lt_to_le.intro. -apply not_eq_true_false. -rewrite < (H1 ? H2). -apply sym_eq. -apply f_max_true. -assumption. +(* example *) +theorem A_SO: A (S O) = S O. +reflexivity. +qed. + +theorem A_SSO: A (S(S O)) = S (S O). +reflexivity. +qed. + +theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))). +reflexivity. +qed. + +theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))). +reflexivity. qed. -theorem log_times1: \forall n,m. O < n \to O < m \to -log (n*m) \le S(log n+log m). +(* +(* a better result *) +theorem le_A_exp3: \forall n. S O < n \to +A(n) \le exp (pred n) (2*(exp 2 (2 * n)). +intro. +apply (nat_elim1 n). intros. -unfold in ⊢ (? (% ?) ?). -apply f_false_to_le_max - [apply (ex_intro ? ? O). - split - [apply le_O_n - |apply le_to_leb_true. +elim (or_eq_eq_S m). +elim H2 + [elim (le_to_or_lt_eq (S O) a) + [rewrite > H3 in ⊢ (? % ?). + apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a)) + [apply le_A_exp + |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)* + ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a)))) + [apply le_times_r. + apply H + [rewrite > H3. + rewrite > times_n_SO in ⊢ (? % ?). + rewrite > sym_times. + apply lt_times_l1 + [apply lt_to_le.assumption + |apply le_n + ] + |assumption + ] + |rewrite > sym_times. + rewrite > assoc_times. + rewrite < exp_plus_times. + apply (trans_le ? + (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m))) + [rewrite > assoc_times. + apply le_times_r. + rewrite < exp_plus_times. + apply le_exp + [apply lt_O_S + |rewrite < H3. + simplify. + rewrite < plus_n_O. + apply le_S.apply le_S. + apply le_n + ] + |apply le_times_l. + rewrite > times_exp. + apply monotonic_exp1. + rewrite > H3. + rewrite > sym_times. + cases a + [apply le_n + |simplify. + rewrite < plus_n_Sm. + apply le_S. + apply le_n + ] + ] + ] + ] + |rewrite < H4 in H3. + simplify in H3. + rewrite > H3. simplify. - rewrite > times_n_SO. - apply le_times;assumption + apply le_S_S.apply le_S_S.apply le_O_n + |apply not_lt_to_le.intro. + apply (lt_to_not_le ? ? H1). + rewrite > H3. + apply (le_n_O_elim a) + [apply le_S_S_to_le.assumption + |apply le_O_n + ] ] - |intros. - apply lt_to_leb_false. - apply (lt_to_le_to_lt ? ((exp (S(S O)) (S(log n)))*(exp (S(S O)) (S(log m))))) - [apply lt_times;apply lt_exp_log - |rewrite < exp_plus_times. - apply le_exp - [apply lt_O_S - |simplify. - rewrite < plus_n_Sm. - assumption + |elim (le_to_or_lt_eq O a (le_O_n ?)) + [apply (trans_le ? (A ((S(S O))*(S a)))) + [apply monotonic_A. + rewrite > H3. + rewrite > times_SSO. + apply le_n_Sn + |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a))) + [apply le_A_exp + |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)* + (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a))))) + [apply le_times_r. + apply H + [rewrite > H3. + apply le_S_S. + simplify. + rewrite > plus_n_SO. + apply le_plus_r. + rewrite < plus_n_O. + assumption + |apply le_S_S.assumption + ] + |rewrite > sym_times. + rewrite > assoc_times. + rewrite < exp_plus_times. + apply (trans_le ? + (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m))) + [rewrite > assoc_times. + apply le_times_r. + rewrite < exp_plus_times. + apply le_exp + [apply lt_O_S + |rewrite > times_SSO. + rewrite < H3. + simplify. + rewrite < plus_n_Sm. + rewrite < plus_n_O. + apply le_n + ] + |apply le_times_l. + rewrite > times_exp. + apply monotonic_exp1. + rewrite > H3. + rewrite > sym_times. + apply le_n + ] + ] + ] ] + |rewrite < H4 in H3.simplify in H3. + apply False_ind. + apply (lt_to_not_le ? ? H1). + rewrite > H3. + apply le_ ] ] qed. - -theorem log_times: \forall n,m.log (n*m) \le S(log n+log m). +*) + +theorem le_A_exp4: \forall n. S O < n \to +A(n) \le (pred n)*exp 2 ((2 * n) -3). +intro. +apply (nat_elim1 n). intros. -cases n - [apply le_O_n - |cases m - [rewrite < times_n_O. - apply le_O_n - |apply log_times1;apply lt_O_S +elim (or_eq_eq_S m). +elim H2 + [elim (le_to_or_lt_eq (S O) a) + [rewrite > H3 in ⊢ (? % ?). + apply (trans_le ? (exp 2 (pred(2*a))*A a)) + [apply le_A_exp + |apply (trans_le ? (2\sup(pred(2*a))*((pred a)*2\sup((2*a)-3)))) + [apply le_times_r. + apply H + [rewrite > H3. + rewrite > times_n_SO in ⊢ (? % ?). + rewrite > sym_times. + apply lt_times_l1 + [apply lt_to_le.assumption + |apply le_n + ] + |assumption + ] + |rewrite < H3. + rewrite < assoc_times. + rewrite > sym_times in ⊢ (? (? % ?) ?). + rewrite > assoc_times. + apply le_times + [rewrite > H3. + elim a[apply le_n|simplify.apply le_plus_n_r] + |rewrite < exp_plus_times. + apply le_exp + [apply lt_O_S + |apply (trans_le ? (m+(m-3))) + [apply le_plus_l. + cases m[apply le_n|apply le_n_Sn] + |simplify.rewrite < plus_n_O. + rewrite > eq_minus_plus_plus_minus + [apply le_n + |rewrite > H3. + apply (trans_le ? (2*2)) + [simplify.apply (le_n_Sn 3) + |apply le_times_r.assumption + ] + ] + ] + ] + ] + ] + ] + |rewrite > H3.rewrite < H4.simplify. + apply le_S_S.apply lt_O_S + |apply not_lt_to_le.intro. + apply (lt_to_not_le ? ? H1). + rewrite > H3. + apply (le_n_O_elim a) + [apply le_S_S_to_le.assumption + |apply le_O_n + ] + ] + |elim (le_to_or_lt_eq O a (le_O_n ?)) + [apply (trans_le ? (A ((S(S O))*(S a)))) + [apply monotonic_A. + rewrite > H3. + rewrite > times_SSO. + apply le_n_Sn + |apply (trans_le ? ((exp 2 (pred(2*(S a))))*A (S a))) + [apply le_A_exp + |apply (trans_le ? ((2\sup(pred (2*S a)))*(a*(exp 2 ((2*(S a))-3))))) + [apply le_times_r. + apply H + [rewrite > H3. + apply le_S_S. + apply le_S_times_SSO. + assumption + |apply le_S_S.assumption + ] + |rewrite > H3. + change in ⊢ (? ? (? % ?)) with (2*a). + rewrite > times_SSO. + change in ⊢ (? (? (? ? %) ?) ?) with (S(2*a)). + rewrite > minus_Sn_m + [change in ⊢ (? (? ? (? ? %)) ?) with (2*(exp 2 (S(2*a)-3))). + rewrite < assoc_times in ⊢ (? (? ? %) ?). + rewrite < assoc_times. + rewrite > sym_times in ⊢ (? (? % ?) ?). + rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?). + rewrite > assoc_times. + apply le_times_r. + rewrite < exp_plus_times. + apply le_exp + [apply lt_O_S + |rewrite < eq_minus_plus_plus_minus + [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?). + apply le_n + |apply le_S_S. + apply O_lt_const_to_le_times_const. + assumption + ] + ] + |apply le_S_S. + apply O_lt_const_to_le_times_const. + assumption + ] + ] + ] + ] + |rewrite < H4 in H3.simplify in H3. + apply False_ind. + apply (lt_to_not_le ? ? H1). + rewrite > H3. + apply le_n ] ] qed. -theorem log_exp: \forall n,m.O < m \to -log ((exp (S(S O)) n)*m)=n+log m. +theorem le_n_SSSSSSSSO_to_le_A_exp: +\forall n. n \le 8 \to A(n) \le exp 2 ((2 * n) -3). +intro.cases n + [intro.apply le_n + |cases n1 + [intro.apply le_n + |cases n2 + [intro.apply le_n + |cases n3 + [intro.apply leb_true_to_le.reflexivity + |cases n4 + [intro.apply leb_true_to_le.reflexivity + |cases n5 + [intro.apply leb_true_to_le.reflexivity + |cases n6 + [intro.apply leb_true_to_le.reflexivity + |cases n7 + [intro.apply leb_true_to_le.reflexivity + |cases n8 + [intro.apply leb_true_to_le.reflexivity + |intro.apply False_ind. + apply (lt_to_not_le ? ? H). + apply leb_true_to_le.reflexivity + ] + ] + ] + ] + ] + ] + ] + ] + ] +qed. + +theorem le_A_exp5: \forall n. A(n) \le exp 2 ((2 * n) -3). +intro. +apply (nat_elim1 n). intros. -unfold log in ⊢ (? ? (% ?) ?). -apply max_spec_to_max. -unfold max_spec. -split - [split - [elim n - [simplify. - rewrite < plus_n_O. - apply le_log_n_n - |simplify. - rewrite < plus_n_O. - rewrite > times_plus_l. - apply (trans_le ? (S((S(S O))\sup(n1)*m))) - [apply le_S_S.assumption - |apply (lt_O_n_elim ((S(S O))\sup(n1)*m)) - [rewrite > (times_n_O O) in ⊢ (? % ?). - apply lt_times - [apply lt_O_exp. - apply lt_O_S - |assumption +elim (decidable_le 9 m) + [elim (or_eq_eq_S m). + elim H2 + [rewrite > H3 in ⊢ (? % ?). + apply (trans_le ? (exp 2 (pred(2*a))*A a)) + [apply le_A_exp + |apply (trans_le ? (2\sup(pred(2*a))*(2\sup((2*a)-3)))) + [apply le_times_r. + apply H. + rewrite > H3. + apply lt_m_nm + [apply (trans_lt ? 4) + [apply lt_O_S + |apply (lt_times_to_lt 2) + [apply lt_O_S + |rewrite < H3.assumption + ] + ] + |apply le_n + ] + |rewrite < H3. + rewrite < exp_plus_times. + apply le_exp + [apply lt_O_S + |simplify.rewrite < plus_n_O. + rewrite > eq_minus_plus_plus_minus + [apply le_plus_l. + apply le_pred_n + |apply (trans_le ? 9) + [apply leb_true_to_le. reflexivity + |assumption + ] + ] + ] + ] + ] + |apply (trans_le ? (A (2*(S a)))) + [apply monotonic_A. + rewrite > H3. + rewrite > times_SSO. + apply le_n_Sn + |apply (trans_le ? ((exp 2 ((2*(S a))-2))*A (S a))) + [apply lt_SSSSO_to_le_A_exp. + apply le_S_S. + apply (le_times_to_le 2) + [apply le_n_Sn. + |apply le_S_S_to_le.rewrite < H3.assumption + ] + |apply (trans_le ? ((2\sup((2*S a)-2))*(exp 2 ((2*(S a))-3)))) + [apply le_times_r. + apply H. + rewrite > H3. + apply le_S_S. + apply lt_m_nm + [apply (lt_to_le_to_lt ? 4) + [apply lt_O_S + |apply (le_times_to_le 2) + [apply lt_O_S + |apply le_S_S_to_le. + rewrite < H3.assumption + ] + ] + |apply le_n + ] + |rewrite > times_SSO. + rewrite < H3. + rewrite < exp_plus_times. + apply le_exp + [apply lt_O_S + |cases m + [apply le_n + |cases n1 + [apply le_n + |simplify. + rewrite < minus_n_O. + rewrite < plus_n_O. + rewrite < plus_n_Sm. + simplify.rewrite < minus_n_O. + rewrite < plus_n_Sm. + apply le_n + ] + ] ] - |intro.simplify.apply le_S_S. - apply le_plus_n ] ] ] - |simplify. - apply le_to_leb_true. - rewrite > exp_plus_times. - apply le_times_r. - apply le_exp_log. - assumption ] - |intros. - simplify. - apply lt_to_leb_false. - apply (lt_to_le_to_lt ? ((exp (S(S O)) n)*(exp (S(S O)) (S(log m))))) - [apply lt_times_r1 - [apply lt_O_exp.apply lt_O_S - |apply lt_exp_log. + |apply le_n_SSSSSSSSO_to_le_A_exp. + apply le_S_S_to_le. + apply not_le_to_lt. + assumption + ] +qed. + +theorem le_exp_Al:\forall n. O < n \to exp 2 n \le A (2 * n). +intros. +apply (trans_le ? ((exp 2 (2*n))/(2*n))) + [apply le_times_to_le_div + [rewrite > (times_n_O O) in ⊢ (? % ?). + apply lt_times + [apply lt_O_S + |assumption ] - |rewrite < exp_plus_times. - apply le_exp + |simplify in ⊢ (? ? (? ? %)). + rewrite < plus_n_O. + rewrite > exp_plus_times. + apply le_times_l. + alias id "le_times_SSO_n_exp_SSO_n" = "cic:/matita/nat/o/le_times_SSO_n_exp_SSO_n.con". + apply le_times_SSO_n_exp_SSO_n + ] + |apply le_times_to_le_div2 + [rewrite > (times_n_O O) in ⊢ (? % ?). + apply lt_times [apply lt_O_S - |rewrite < plus_n_Sm. + |assumption + ] + |apply (trans_le ? ((B (2*n)*(2*n)))) + [rewrite < sym_times in ⊢ (? ? %). + apply le_exp_B. assumption + |apply le_times_l. + apply le_B_A ] ] ] qed. -theorem log_SSO: \forall n. O < n \to -log ((S(S O))*n) = S (log n). +theorem le_exp_A2:\forall n. 1 < n \to exp 2 (n / 2) \le A n. intros. -change with (log ((exp (S(S O)) (S O))*n)=S (log n)). -rewrite > log_exp.reflexivity.assumption. -qed. - -theorem or_eq_S: \forall n.\exists m. -(n = (S(S O))*m) \lor (n = S((S(S O))*m)). -intro. -elim n - [apply (ex_intro ? ? O).left.apply times_n_O - |elim H.elim H1 - [apply (ex_intro ? ? a).right.apply eq_f.assumption - |apply (ex_intro ? ? (S a)).left. - rewrite > H2.simplify. - rewrite < plus_n_O. - rewrite < plus_n_Sm. - reflexivity +apply (trans_le ? (A(n/2*2))) + [rewrite > sym_times. + apply le_exp_Al. + elim (le_to_or_lt_eq ? ? (le_O_n (n/2))) + [assumption + |apply False_ind. + apply (lt_to_not_le ? ? H). + rewrite > (div_mod n 2) + [rewrite < H1. + change in ⊢ (? % ?) with (n\mod 2). + apply le_S_S_to_le. + apply lt_mod_m_m. + apply lt_O_S + |apply lt_O_S + ] ] + |apply monotonic_A. + rewrite > (div_mod n 2) in ⊢ (? ? %). + apply le_plus_n_r. + apply lt_O_S ] qed. -theorem lt_O_to_or_eq_S: \forall n.O < n \to \exists m.m < n \land -((n = (S(S O))*m) \lor (n = S((S(S O))*m))). -intros. -elim (or_eq_S n). -elim H1 - [apply (ex_intro ? ? a).split - [rewrite > H2. - rewrite > times_n_SO in ⊢ (? % ?). - rewrite > sym_times. - apply lt_times_l1 - [apply (divides_to_lt_O a n ? ?) - [assumption - |apply (witness a n (S (S O))). - rewrite > sym_times. - assumption - ] - |apply le_n - ] - |left.assumption - ] - |apply (ex_intro ? ? a).split - [rewrite > H2. - apply (le_to_lt_to_lt ? ((S(S O))*a)) - [rewrite > times_n_SO in ⊢ (? % ?). - rewrite > sym_times. - apply le_times_l. - apply le_n_Sn - |apply le_n - ] - |right.assumption +theorem eq_sigma_pi_SO_n: \forall n. +sigma_p n (\lambda i.true) (\lambda i.S O) = n. +intro.elim n + [reflexivity + |rewrite > true_to_sigma_p_Sn + [rewrite > H.reflexivity + |reflexivity ] ] qed. -theorem factS: \forall n. fact (S n) = (S n)*(fact n). -intro.simplify.reflexivity. +theorem leA_prim: \forall n. +exp n (prim n) \le A n * pi_p (S n) primeb (λp:nat.p). +intro. +unfold prim. +rewrite < (exp_sigma_p (S n) n primeb). +unfold A. +rewrite < times_pi_p. +apply le_pi_p. +intros. +rewrite > sym_times. +change in ⊢ (? ? %) with (exp i (S (log i n))). +apply lt_to_le. +apply lt_exp_log. +apply prime_to_lt_SO. +apply primeb_true_to_prime. +assumption. qed. -theorem exp_S: \forall n,m. exp m (S n) = m*exp m n. -intros.reflexivity. + +theorem le_prim_log : \forall n,b.S O < b \to +log b (A n) \leq prim n * (S (log b n)). +intros;apply (trans_le ? ? ? ? (log_exp1 ? ? ? ?)) + [apply le_log + [assumption + |apply le_Al] + |assumption] qed. -lemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)). -intro.simplify.rewrite < plus_n_Sm.reflexivity. + +(* the inequalities *) +theorem le_exp_priml: \forall n. O < n \to +exp 2 (2*n) \le exp (2*n) (S(prim (2*n))). +intros. +apply (trans_le ? (((2*n*(B (2*n)))))) + [apply le_exp_B.assumption + |change in ⊢ (? ? %) with (((2*n))*((2*n))\sup (prim (2*n))). + apply le_times_r. + apply (trans_le ? (A (2*n))) + [apply le_B_A + |apply le_Al + ] + ] qed. -theorem fact1: \forall n. -fact ((S(S O))*n) \le (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n). -intro.elim n - [rewrite < times_n_O.apply le_n - |rewrite > times_SSO. - rewrite > factS. - rewrite > factS. +theorem le_exp_prim4l: \forall n. O < n \to +exp 2 (S(4*n)) \le exp (4*n) (S(prim (4*n))). +intros. +apply (trans_le ? (2*(4*n*(B (4*n))))) + [change in ⊢ (? % ?) with (2*(exp 2 (4*n))). + apply le_times_r. + cut (4*n = 2*(2*n)) + [rewrite > Hcut. + apply le_exp_B. + apply lt_to_le.unfold. + rewrite > times_n_SO in ⊢ (? % ?). + apply le_times_r.assumption + |rewrite < assoc_times. + reflexivity + ] + |change in ⊢ (? ? %) with ((4*n)*(4*n)\sup (prim (4*n))). rewrite < assoc_times. - rewrite > factS. - apply (trans_le ? (((S(S O))*(S n1))*((S(S O))*(S n1))*(fact (((S(S O))*n1))))) - [apply le_times_l. - rewrite > times_SSO. - apply le_times_r. - apply le_n_Sn - |rewrite > assoc_times. - rewrite > assoc_times. - rewrite > assoc_times in ⊢ (? ? %). - rewrite > exp_S. - rewrite > assoc_times in ⊢ (? ? %). - apply le_times_r. - rewrite < assoc_times. - rewrite < assoc_times. - rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?). - rewrite > assoc_times. - rewrite > assoc_times. - rewrite > exp_S. - rewrite > assoc_times in ⊢ (? ? %). - apply le_times_r. - rewrite > sym_times in ⊢ (? ? %). - rewrite > assoc_times in ⊢ (? ? %). - rewrite > assoc_times in ⊢ (? ? %). - apply le_times_r. - rewrite < assoc_times in ⊢ (? ? %). - rewrite < assoc_times in ⊢ (? ? %). - rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)). - rewrite > assoc_times in ⊢ (? ? %). - rewrite > assoc_times in ⊢ (? ? %). - apply le_times_r. - rewrite > sym_times in ⊢ (? ? (? ? %)). - rewrite > sym_times in ⊢ (? ? %). - assumption + rewrite > sym_times in ⊢ (? (? % ?) ?). + rewrite > assoc_times. + apply le_times_r. + apply (trans_le ? (A (4*n))) + [apply le_B_A4.assumption + |apply le_Al ] ] qed. -theorem monotonic_log: monotonic nat le log. -unfold monotonic.intros. -elim (le_to_or_lt_eq ? ? H) 0 - [cases x;intro - [apply le_O_n - |apply lt_S_to_le. - apply (lt_exp_to_lt (S(S O))) +theorem le_priml: \forall n. O < n \to +2*n \le (S (log 2 (2*n)))*S(prim (2*n)). +intros. +rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?) + [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n))))))) + [apply le_log [apply le_n - |apply (le_to_lt_to_lt ? (S n)) - [apply le_exp_log. - apply lt_O_S - |apply (trans_lt ? y) - [assumption - |apply lt_exp_log - ] - ] + |apply le_exp_priml.assumption ] + |rewrite > sym_times in ⊢ (? ? %). + apply log_exp1. + apply le_n ] - |intro.rewrite < H1.apply le_n + |apply le_n ] qed. -theorem lt_O_fact: \forall n. O < fact n. -intro.elim n - [simplify.apply lt_O_S - |rewrite > factS. - rewrite > (times_n_O O). - apply lt_times - [apply lt_O_S - |assumption - ] +theorem le_exp_primr: \forall n. +exp n (prim n) \le exp 2 (2*(2*n-3)). +intros. +apply (trans_le ? (exp (A n) 2)) + [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))). + rewrite < times_n_SO. + apply leA_r2 + |rewrite > sym_times. + rewrite < exp_exp_times. + apply monotonic_exp1. + apply le_A_exp5 ] qed. -theorem fact2: \forall n.O < n \to -(exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n) < fact (S((S(S O))*n)). -intros.elim H - [simplify.apply le_S.apply le_n - |rewrite > times_SSO. - rewrite > factS. - rewrite > factS. - rewrite < assoc_times. - rewrite > factS. - rewrite < times_SSO in ⊢ (? ? %). - apply (trans_lt ? (((S(S O))*S n1)*((S(S O))*S n1*(S ((S(S O))*n1))!))) - [rewrite > assoc_times in ⊢ (? ? %). - rewrite > exp_S. - rewrite > assoc_times. - rewrite > assoc_times. - rewrite > assoc_times. - apply lt_times_r. - rewrite > exp_S. - rewrite > assoc_times. - rewrite > sym_times in ⊢ (? ? %). - rewrite > assoc_times in ⊢ (? ? %). - rewrite > assoc_times in ⊢ (? ? %). - apply lt_times_r. - rewrite > sym_times. - rewrite > assoc_times. - rewrite > assoc_times. - apply lt_times_r. - rewrite < assoc_times. - rewrite < assoc_times. - rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?). - rewrite > assoc_times. - rewrite > assoc_times. - rewrite > sym_times in ⊢ (? ? %). - apply lt_times_r. - rewrite < assoc_times. - rewrite < sym_times. - rewrite < assoc_times. - assumption - |apply lt_times_l1 - [rewrite > (times_n_O O) in ⊢ (? % ?). - apply lt_times - [rewrite > (times_n_O O) in ⊢ (? % ?). - apply lt_times - [apply lt_O_S - |apply lt_O_S - ] - |apply lt_O_fact +(* bounds *) +theorem le_primr: \forall n. 1 < n \to prim n \le 2*(2*n-3)/log 2 n. +intros. +apply le_times_to_le_div + [apply lt_O_log + [apply lt_to_le.assumption + |assumption + ] + |apply (trans_le ? (log 2 (exp n (prim n)))) + [rewrite > sym_times. + apply log_exp2 + [apply le_n + |apply lt_to_le.assumption + ] + |rewrite < (eq_log_exp 2) in ⊢ (? ? %) + [apply le_log + [apply le_n + |apply le_exp_primr ] |apply le_n ] ] ] qed. - -theorem lt_O_log: \forall n. S O < n \to O < log n. -intros.elim H - [simplify.apply lt_O_S - |apply (lt_to_le_to_lt ? (log n1)) - [assumption - |apply monotonic_log. - apply le_n_Sn + +theorem le_priml1: \forall n. O < n \to +2*n/((log 2 n)+2) - 1 \le prim (2*n). +intros. +apply le_plus_to_minus. +apply le_times_to_le_div2 + [rewrite > sym_plus. + simplify.apply lt_O_S + |rewrite > sym_times in ⊢ (? ? %). + rewrite < plus_n_Sm. + rewrite < plus_n_Sm in ⊢ (? ? (? ? %)). + rewrite < plus_n_O. + rewrite < sym_plus. + rewrite < log_exp + [simplify in ⊢ (? ? (? (? (? ? (? % ?))) ?)). + apply le_priml. + assumption + |apply le_n + |assumption ] ] qed. -theorem log_fact_SSSO: log (fact (S(S(S O)))) = S (S O). -reflexivity. -qed. - -lemma exp_SSO_SSO: exp (S(S O)) (S(S O)) = S(S(S(S O))). -reflexivity. -qed. (* -theorem log_fact_SSSSO: log (fact (S(S(S(S O))))) = S(S(S(S O))). -reflexivity. -qed. -*) -theorem log_fact_SSSSSO: log (fact (S(S(S(S(S O)))))) = S(S(S(S O))). -reflexivity. -qed. - -theorem bof_bof: \forall n.(S(S(S(S O)))) < n \to -n \le (S(S(S(S(S(S(S(S O)))))))) \to log (fact n) < n*log n - n. +theorem prim_SSSSSSO: \forall n.30\le n \to O < prim (8*n) - prim n. intros. -elim H - [rewrite > factS in ⊢ (? (? %) ?). - rewrite > factS in ⊢ (? (? (? ? %)) ?). - rewrite < assoc_times in ⊢ (? (? %) ?). - rewrite < sym_times in ⊢ (? (? (? % ?)) ?). - rewrite > assoc_times in ⊢ (? (? %) ?). - change with (exp (S(S O)) (S(S O))) in ⊢ (? (? (? % ?)) ?). - -theorem bof: \forall n.(S(S(S(S O))))) < n \to log (fact n) < n*log n - n. -intro.apply (nat_elim1 n). -intros. -elim (lt_O_to_or_eq_S m) - [elim H2.clear H2. - elim H4.clear H4. - rewrite > H2. - apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a)))) - [apply monotonic_log. - apply fact1 - |rewrite > assoc_times in ⊢ (? (? %) ?). - rewrite > log_exp. - apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!))) - [apply le_plus_r. - apply log_times - |rewrite > plus_n_Sm. - rewrite > log_SSO. - rewrite < times_n_Sm. - apply (le_to_lt_to_lt ? ((S(S O))*a+(log a!+(a*log a-a)))) - [apply le_plus_r. - apply le_plus_r. - apply H.assumption - |apply (lt_to_le_to_lt ? ((S(S O))*a+((a*log a-a)+(a*log a-a)))) - [apply lt_plus_r. - apply lt_plus_l. - apply H. - assumption. - |rewrite > times_SSO_n. - rewrite > distr_times_minus. - rewrite > sym_plus. - rewrite > plus_minus - [rewrite > sym_plus. - rewrite < assoc_times. - apply le_n - |rewrite < assoc_times. - rewrite > times_n_SO in ⊢ (? % ?). - apply le_times - [apply le_n - |apply lt_O_log. - apply (lt_times_n_to_lt_r (S(S O))) - [apply lt_O_S - |rewrite < times_n_SO. - rewrite < H2. - assumption - ] - ] - ] - ] - - . - ] - | - rewrite < eq_plus_minus_minus_plus. - - rewrite > assoc_plus. - apply lt_plus_r. - rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?). - change with - (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)). - apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a)))) - [apply le_S_S. - apply lt_plus_r. - apply lt_times_r. - apply H. - assumption - | - -theorem stirling: \forall n,k.k \le n \to -log (fact n) < n*log n - n + k*log n. -intro. -apply (nat_elim1 n). -intros. -elim (lt_O_to_or_eq_S m) - [elim H2.clear H2. - elim H4.clear H4. - rewrite > H2. - apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a)))) - [apply monotonic_log. - apply fact1 - |rewrite > assoc_times in ⊢ (? (? %) ?). - rewrite > log_exp. - apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!))) - [apply le_plus_r. - apply log_times - |rewrite < plus_n_Sm. - rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?). - change with - (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)). - apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a)))) - [apply le_S_S. - apply lt_plus_r. - apply lt_times_r. - apply H. - assumption - | - - [ - - a*log a-a+k*log a - -*) \ No newline at end of file +apply lt_to_lt_O_minus. +change in ⊢ (? ? (? (? % ?))) with (2*4). +rewrite > assoc_times. +apply (le_to_lt_to_lt ? (2*(2*n-3)/log 2 n)) + [apply le_primr.apply (trans_lt ? ? ? ? H). + apply leb_true_to_le.reflexivity + |apply (lt_to_le_to_lt ? (2*(4*n)/((log 2 (4*n))+2) - 1)) + [elim H + [ +normalize in ⊢ (%);simplify. + |apply le_priml1. +*) + + +