From 10f29fdd78ee089a9a94446207b543d33d6c851c Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 22 Jan 2008 10:41:43 +0000 Subject: [PATCH] Bertrand's conjecture (weak), some work in progress --- helm/software/matita/library/nat/chebyshev.ma | 145 +++++++++++++++ .../matita/library/nat/chebyshev_thm.ma | 175 ++++++++++++------ 2 files changed, 260 insertions(+), 60 deletions(-) diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma index 2a3695e8e..1f50b3212 100644 --- a/helm/software/matita/library/nat/chebyshev.ma +++ b/helm/software/matita/library/nat/chebyshev.ma @@ -1459,6 +1459,142 @@ elim H2 ] qed. +theorem le_A_exp4: \forall n. S O < n \to +A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * (pred n))). +intro. +apply (nat_elim1 n). +intros. +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))*(pred 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))*(pred 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. + rewrite < plus_n_O; + apply le_S_S_to_le; + rewrite > plus_n_Sm in \vdash (? ? %); + rewrite < S_pred; + [change in \vdash (? % ?) with ((S (pred a + pred a)) + m); + apply le_plus_l; + apply le_S_S_to_le; + rewrite < S_pred; + [rewrite > plus_n_Sm;rewrite > sym_plus; + rewrite > plus_n_Sm; + rewrite > H3;simplify in \vdash (? ? %); + rewrite < plus_n_O;rewrite < S_pred; + [apply le_n + |apply lt_to_le;assumption] + |apply lt_to_le;assumption] + |apply lt_to_le;assumption]] + |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. + 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 + ] + ] + |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))*a)))) + [apply le_times_r. + apply (trans_le ? ? ? (H (S a) ? ?)); + [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 + |simplify in ⊢ (? (? (? % ?) ?) ?); + apply le_times_r;apply le_exp; + [apply le_S;apply le_n + |apply le_times_r;simplify;apply le_n] + ] + |rewrite > sym_times. + rewrite > assoc_times. + rewrite < exp_plus_times. + rewrite > H3; + change in ⊢ (? ? (? (? % ?) ?)) with ((S (S O))*a); + rewrite < times_exp; + rewrite < sym_times in \vdash (? ? (? % ?)); + rewrite > assoc_times; + apply le_times_r; + rewrite < times_n_Sm in ⊢ (? (? ? (? ? %)) ?); + rewrite > sym_plus in \vdash (? (? ? %) ?); + rewrite > assoc_plus in \vdash (? (? ? %) ?); + rewrite > exp_plus_times;apply le_times_r; + rewrite < distr_times_plus in ⊢ (? (? ? %) ?); + simplify in ⊢ (? ? (? ? (? ? %)));rewrite < plus_n_O; + apply le_n + ] + ] + ] + |rewrite < H4 in H3.simplify in H3. + apply False_ind. + apply (lt_to_not_le ? ? H1). + rewrite > H3. + apply le_n + ] + ] +qed. + + theorem eq_sigma_pi_SO_n: \forall n. sigma_p n (\lambda i.true) (\lambda i.S O) = n. intro.elim n @@ -1488,6 +1624,15 @@ apply primeb_true_to_prime. assumption. qed. +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. + (* the inequalities *) theorem le_exp_priml: \forall n. O < n \to diff --git a/helm/software/matita/library/nat/chebyshev_thm.ma b/helm/software/matita/library/nat/chebyshev_thm.ma index c75594ab6..248c9e3c6 100644 --- a/helm/software/matita/library/nat/chebyshev_thm.ma +++ b/helm/software/matita/library/nat/chebyshev_thm.ma @@ -630,13 +630,13 @@ apply (trans_le ? (log b (A n) + (log b (C1 n * C2 n)) + 1)); qed. lemma le_log_A1 : \forall n,b. S O < b \to S O < n \to - log b (A n) \leq 2*(S (log b (pred n))) + (2*n)*(S (log b 2)) + 1. -intros.apply (trans_le ? (log b ((exp (pred n) 2)*(exp 2 (2*n))))) + log b (A n) \leq 2*(S (log b (pred n))) + (2*(pred n))*(S (log b 2)) + 1. +intros.apply (trans_le ? (log b ((exp (pred n) 2)*(exp 2 (2*(pred n)))))) [apply le_log [assumption - |simplify in ⊢ (? ? (? (? % ?) ?));apply le_A_exp3;assumption] - |rewrite < sym_plus;apply (trans_le ? (1 + ((log b (exp (pred n) 2)) + (log b (exp 2 (2*n)))))); - [change in \vdash (? ? %) with (S (log b ((pred n)\sup(2))+log b ((2)\sup(2*n)))); + |simplify in ⊢ (? ? (? (? % ?) ?));apply le_A_exp4;assumption] + |rewrite < sym_plus;apply (trans_le ? (1 + ((log b (exp (pred n) 2)) + (log b (exp 2 (2*(pred n))))))); + [change in \vdash (? ? %) with (S (log b ((pred n)\sup(2))+log b ((2)\sup(2*(pred n))))); apply log_times;assumption |apply le_plus_r;apply le_plus;apply log_exp1;assumption]] qed. @@ -721,13 +721,13 @@ qed. lemma le_prim_log_stima: \forall n,b. S O < b \to b < sqrt n \to (prim n)*(log b n) \leq - 2*S (log b (pred n))+2*n*S (log b 2) - +(2*S (log b (pred (sqrt n)))+2*sqrt n*S (log b 2)) + 2*S (log b (pred n))+2*(pred n)*S (log b 2) + +(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2)) +(14*n/log b n+28*n*S (log b 3)/pred (log b n)) +4. intros.cut (1 < n) - [apply (trans_le ? ((2*(S (log b (pred n))) + (2*n)*(S (log b 2)) + 1) + - (2*(S (log b (pred (sqrt n)))) + (2*(sqrt n))*(S (log b 2)) + 1) + + [apply (trans_le ? ((2*(S (log b (pred n))) + (2*(pred n))*(S (log b 2)) + 1) + + (2*(S (log b (pred (sqrt n)))) + (2*(pred (sqrt n)))*(S (log b 2)) + 1) + ((14*n/(log b n)) + ((28*n)*(S (log b (S (S (S O)))))/pred (log b n))) + 2)) [apply (trans_le ? ? ? (le_prim_log1 ? ? H ?)) [apply lt_to_le;assumption @@ -796,8 +796,8 @@ qed. lemma le_prim_stima: \forall n,b. S O < b \to b < sqrt n \to (prim n) \leq - 2*S (log b (pred n))/(log b n) + 2*n*S (log b 2)/(log b n) - +2*S (log b (pred (sqrt n)))/(log b n)+ 2*sqrt n*S (log b 2)/(log b n) + 2*S (log b (pred n))/(log b n) + 2*(pred n)*S (log b 2)/(log b n) + +2*S (log b (pred (sqrt n)))/(log b n)+ 2*(pred (sqrt n))*S (log b 2)/(log b n) + 14*n/(log b n * log b n) + 28*n*S (log b 3)/(pred (log b n) * log b n) +4/(log b n) + 6. intros; @@ -809,22 +809,22 @@ cut (O < log b n) |apply (trans_le ? (sqrt n)) [apply lt_to_le;assumption |apply le_sqrt_n_n]]] -apply (trans_le ? ((2*S (log b (pred n))+2*n*S (log b 2) - +(2*S (log b (pred (sqrt n)))+2*sqrt n*S (log b 2)) +apply (trans_le ? ((2*S (log b (pred n))+2*(pred n)*S (log b 2) + +(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2)) +(14*n/log b n+28*n*S (log b 3)/pred (log b n)) +4)/(log b n))) [apply le_times_to_le_div [assumption |rewrite > sym_times;apply le_prim_log_stima;assumption] - |apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*n*S (log b 2) -+(2*S (log b (pred (sqrt n)))+2*sqrt n*S (log b 2)) + |apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*(pred n)*S (log b 2) ++(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2)) +(14*n/log b n+28*n*S (log b 3)/pred (log b n))) 4 (log b n) ?)) [assumption |rewrite < plus_n_Sm;apply le_S_S;rewrite > assoc_plus in \vdash (? ? %); rewrite > sym_plus in \vdash (? ? (? ? %)); rewrite < assoc_plus in \vdash (? ? %); - apply le_plus_l;apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*n*S (log b 2) -+(2*S (log b (pred (sqrt n)))+2*sqrt n*S (log b 2))) (14*n/log b n+28*n*S (log b 3)/pred (log b n)) (log b n) ?)); + apply le_plus_l;apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*(pred n)*S (log b 2) ++(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2))) (14*n/log b n+28*n*S (log b 3)/pred (log b n)) (log b n) ?)); [assumption |rewrite < plus_n_Sm in \vdash (? ? %);apply le_S_S; change in \vdash (? ? (? ? %)) with (1+3); @@ -833,7 +833,7 @@ apply (trans_le ? ((2*S (log b (pred n))+2*n*S (log b 2) rewrite > assoc_plus in ⊢ (? ? (? % ?)); rewrite > sym_plus in \vdash (? ? %);rewrite < assoc_plus in \vdash (? ? %); rewrite > sym_plus in \vdash (? ? (? % ?));apply le_plus - [apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*n*S (log b 2)) (2*S (log b (pred (sqrt n)))+2*sqrt n*S (log b 2)) (log b n) ?)) + [apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*pred n*S (log b 2)) (2*S (log b (pred (sqrt n)))+2*pred (sqrt n)*S (log b 2)) (log b n) ?)) [assumption |rewrite < plus_n_Sm;apply le_S_S;change in \vdash (? ? (? ? %)) with (1+1); rewrite < assoc_plus in \vdash (? ? %);rewrite > assoc_plus in ⊢ (? ? (? (? % ?) ?)); @@ -863,48 +863,103 @@ apply (trans_le ? ((2*S (log b (pred n))+2*n*S (log b 2) |elim daemon]] |assumption]]]]]]] qed. - - -(*intros;apply lt_to_le;lapply (lt_div_S (((S (S (S (S O))))* log b (pred i)) + (S (S (S (S (S O)))))) i) - [apply (trans_le ? ? ? Hletin);apply le_times_l;apply le_S_S; - elim H1 - [rewrite > log_SO; - [simplify;apply le_n - |assumption] - | - apply le_times_to_le_div2; - |*) - -(* -theorem le_log_C2_sigma_p : \forall n,b. S O < b \to -log b (C2 n) \leq -(sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x))) (\lambda x.S O)) + -(sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x))) - (\lambda p.(sigma_p (n+p) (\lambda i.leb p i) - (\lambda i.S ((n+p)!/i*(S (log b 3)))))/(n+p)!)). -intros;unfold C2; -apply (trans_le ? (sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) (λx:nat.1) -+sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) - (λi.log b (S (n/i))))) - [apply log_pi_p;assumption - |apply le_plus - [apply le_n - |apply le_sigma_p;intros;cut (S (n/i) = (n+i)/i) - [rewrite > Hcut;apply le_log_div_sigma_p - [assumption - |apply prime_to_lt_O;apply primeb_true_to_prime; - elim (and_true ? ? H2);assumption - |apply le_plus_n - |apply le_n] - |lapply (prime_to_lt_O i (primeb_true_to_prime ? (andb_true_true ? ? H2))) as H3; - apply (div_mod_spec_to_eq (n+i) i (S (n/i)) (n \mod i) ? ((n+i) \mod i)) - [constructor 1 - [apply lt_mod_m_m;assumption - |simplify;rewrite > assoc_plus;rewrite < div_mod; - [apply sym_plus - |assumption]] - |apply div_mod_spec_div_mod;assumption]]]] +lemma leq_sqrt_n : \forall n. sqrt n * sqrt n \leq n. +intro;unfold sqrt;apply leb_true_to_le;apply f_max_true;apply (ex_intro ? ? O); +split + [apply le_O_n + |simplify;reflexivity] qed. -*) +lemma le_sqrt_log_n : \forall n,b. 2 < b \to sqrt n * log b n \leq n. +intros. +apply (trans_le ? ? ? ? (leq_sqrt_n ?)); +apply le_times_r;unfold sqrt; +apply f_m_to_le_max + [apply le_log_n_n;apply lt_to_le;assumption + |apply le_to_leb_true;elim (le_to_or_lt_eq ? ? (le_O_n n)) + [apply (trans_le ? (exp b (log b n))) + [elim (log b n) + [apply le_O_n + |simplify in \vdash (? ? %); + elim (le_to_or_lt_eq ? ? (le_O_n n1)) + [elim (le_to_or_lt_eq ? ? H3) + [apply (trans_le ? (3*(n1*n1))); + [simplify in \vdash (? % ?);rewrite > sym_times in \vdash (? % ?); + simplify in \vdash (? % ?); + simplify;rewrite > sym_plus; + rewrite > plus_n_Sm;rewrite > sym_plus in \vdash (? (? % ?) ?); + rewrite > assoc_plus;apply le_plus_r; + rewrite < plus_n_Sm; + rewrite < plus_n_O; + apply lt_plus;rewrite > times_n_SO in \vdash (? % ?); + apply lt_times_r1;assumption; + |apply le_times + [assumption + |assumption]] + |rewrite < H4;apply le_times + [apply lt_to_le;assumption + |apply lt_to_le;simplify;rewrite < times_n_SO;assumption]] + |rewrite < H3;simplify;rewrite < times_n_SO;do 2 apply lt_to_le;assumption]] + |simplify;apply le_exp_log;assumption] + |rewrite < H1;simplify;apply le_n]] +qed. + +(* Bertrand weak, lavori in corso + +theorem bertrand_weak : \forall n. 9 \leq n \to prim n < prim (4*n). +intros. +apply (trans_le ? ? ? (le_S_S ? ? (le_prim_stima ? 2 ? ?))) + [apply le_n + |unfold sqrt;apply f_m_to_le_max + [do 6 apply lt_to_le;assumption + |apply le_to_leb_true;assumption] + |cut (pred ((4*n)/(S (log 2 (4*n)))) \leq prim (4*n)) + [|apply le_S_S_to_le;rewrite < S_pred + [apply le_times_to_le_div2 + [apply lt_O_S + |change in \vdash (? % (? (? (? %)) (? (? ? %)))) with (2*2*n); + rewrite > assoc_times in \vdash (? % (? (? (? %)) (? (? ? %)))); + rewrite > sym_times in \vdash (? ? %); + apply le_priml;rewrite > (times_n_O O) in \vdash (? % ?); + apply lt_times; + [apply lt_O_S + |apply (trans_le ? ? ? ? H);apply le_S_S;apply le_O_n]] + |apply le_times_to_le_div; + [apply lt_O_S + |rewrite < times_n_SO;apply (trans_le ? (S (S (2 + (log 2 n))))) + [apply le_S_S;apply (log_times 2 4 n);apply le_S_S;apply le_n + |change in \vdash (? % ?) with (4 + log 2 n); + rewrite > S_pred in \vdash (? ? (? ? %)); + [change in ⊢ (? ? (? ? %)) with (1 + pred n); + rewrite > distr_times_plus;apply le_plus_r;elim H + [simplify;do 3 apply le_S_S;apply le_O_n + |apply (trans_le ? (log 2 (2*n1))) + [apply le_log; + [apply le_S_S;apply le_n + |rewrite < times_SSO_n; + change in \vdash (? % ?) with (1 + n1); + apply le_plus_l;apply (trans_le ? ? ? ? H1); + apply lt_O_S] + |apply (trans_le ? (S (4*pred n1))) + [rewrite > exp_n_SO in ⊢ (? (? ? (? % ?)) ?); + rewrite > log_exp + [change in \vdash (? ? %) with (1 + (4*pred n1)); + apply le_plus_r; + assumption + |apply le_S_S;apply le_n + |apply (trans_le ? ? ? ? H1);apply le_S_S;apply le_O_n] + |simplify in \vdash (? ? (? ? %)); + rewrite > minus_n_O in \vdash (? (? (? ? (? %))) ?); + rewrite < eq_minus_S_pred; + rewrite > distr_times_minus; + change in \vdash (? % ?) with (1 + (4*n1 - 4)); + rewrite > eq_plus_minus_minus_minus + [simplify;apply le_minus_m; + |apply lt_O_S + |rewrite > times_n_SO in \vdash (? % ?); + apply le_times_r;apply (trans_le ? ? ? ? H1); + apply lt_O_S]]]] + |apply (trans_le ? ? ? ? H);apply lt_O_S]]]]] + apply (trans_le ? ? ? ? Hcut); +*) -- 2.39.2