From 291771338278ef9c5b32e2f1660822b9246d7d0e Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 6 Jun 2008 10:21:15 +0000 Subject: [PATCH] Cleanup. --- helm/software/matita/library/nat/chebyshev.ma | 161 ++++++++++++------ 1 file changed, 110 insertions(+), 51 deletions(-) diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma index ff7db61cc..6ef8624e4 100644 --- a/helm/software/matita/library/nat/chebyshev.ma +++ b/helm/software/matita/library/nat/chebyshev.ma @@ -18,7 +18,7 @@ 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 @@ -152,7 +152,7 @@ apply nat_elim2;intros ] qed. -(* si dovrebbe poter migliorare *) +(* la prova potrebbe essere migliorata *) theorem le_prim_n3: \forall n. 15 \le n \to prim n \le pred (n/2). intros. @@ -331,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 @@ -544,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 ⊢ (? ? (? ? %)) @@ -655,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:?.? ? %) ?)) @@ -797,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 @@ -825,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))))) @@ -1009,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 @@ -1031,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. @@ -1047,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. @@ -1076,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 @@ -1118,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. @@ -1164,7 +1164,7 @@ 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 @@ -1275,7 +1275,8 @@ cut ((S(S O)) < (S ((S(S(S(S O))))*n))) ] ] qed. - + +(* not usefull theorem le_fact_A:\forall n.S O < n \to fact (2*n) \le exp (fact n) 2 * A (2*n). intros. @@ -1284,7 +1285,7 @@ rewrite > eq_fact_B apply le_B_A |assumption ] -qed. +qed. *) theorem lt_SO_to_le_B_exp: \forall n.S O < n \to B (2*n) \le exp 2 (pred (2*n)). @@ -1331,8 +1332,8 @@ apply (le_times_to_le (exp (fact n) (S(S O)))) ] qed. -theorem lt_SO_to_le_exp_B: \forall n. S O < n \to -exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n). +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. @@ -1350,7 +1351,7 @@ apply (le_times_to_le (exp (fact n) (S(S O)))) qed. theorem le_exp_B: \forall n. O < n \to -exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n). +exp 2 (2*n) \le 2 * n * B (2*n). intros. elim H [apply le_n @@ -1360,9 +1361,9 @@ elim H 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. @@ -1458,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. @@ -2084,6 +2085,64 @@ elim (decidable_le 9 m) ] 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 + ] + |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 + |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 le_exp_A2:\forall n. 1 < n \to exp 2 (n / 2) \le A n. +intros. +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 eq_sigma_pi_SO_n: \forall n. sigma_p n (\lambda i.true) (\lambda i.S O) = n. intro.elim n @@ -2126,13 +2185,13 @@ qed. (* the inequalities *) theorem le_exp_priml: \forall n. O < n \to -exp (S(S O)) ((S(S O))*n) \le exp ((S(S O))*n) (S(prim ((S(S O))*n))). +exp 2 (2*n) \le exp (2*n) (S(prim (2*n))). intros. -apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n)))))) +apply (trans_le ? (((2*n*(B (2*n)))))) [apply le_exp_B.assumption - |change in ⊢ (? ? %) with ((((S(S O))*n))*(((S(S O))*n))\sup (prim ((S(S O))*n))). + |change in ⊢ (? ? %) with (((2*n))*((2*n))\sup (prim (2*n))). apply le_times_r. - apply (trans_le ? (A ((S(S O))*n))) + apply (trans_le ? (A (2*n))) [apply le_B_A |apply le_Al ] -- 2.39.2