(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/chebyshev_thm/".
-
include "nat/neper.ma".
definition C \def \lambda n.pi_p (S n) primeb
[apply (bool_elim ? (leb ((S n1)*(S n1)) m))
[intro;rewrite > true_to_pi_p_Sn in \vdash (? ? ? (? % ?))
[rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? ? %))
- [rewrite > H1;rewrite > H2;rewrite < assoc_times;reflexivity
+ [rewrite > H1;rewrite < assoc_times;reflexivity
|rewrite > H;lapply (leb_true_to_le ? ? H2);
lapply (le_to_not_lt ? ? Hletin);
apply (bool_elim ? (leb (S m) (S n1 * S n1)))
|rewrite > andb_sym;apply le_O_n]
|apply sigma_p_log_div;assumption]]]]
qed.
+(*
lemma le_prim_n_stima : \forall n,b. S O < b \to b \leq n \to
prim n \leq (S (((S (S (S (S O))))*(S (log b (pred n)))) +
|assumption]]
qed.
-lemma eq_div_div_times : \forall x,y,z.O < z \to O < y \to x/y = (z*x)/(z*y).
-intros.rewrite > (div_mod x y) in \vdash (? ? ? %);
- [rewrite > distr_times_plus;rewrite > sym_times;rewrite > assoc_times;
- rewrite > sym_times in ⊢ (? ? ? (? (? (? ? %) ?) ?));
- rewrite > div_plus_times
- [reflexivity
- |generalize in match H;cases z;intros
- [elim (not_le_Sn_O ? H2)
- |apply lt_times_r;apply lt_mod_m_m;assumption]]
- |assumption]
-qed.
-
alias num (instance 0) = "natural number".
lemma le_sigma_p_lemma1 : \forall n,b. S O < b \to b*b < n \to
(sigma_p n (\lambda x.leb (S n) (x*x))
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.
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
|apply (trans_le ? ? ? H);apply lt_to_le;apply (trans_le ? ? ? H1);
apply le_sqrt_n_n]
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 eq_div_div_div_times: \forall a,b,c. O < b \to O < c \to a/b/c = a/(b*c).
+intros.rewrite > (div_mod a (b*c)) in \vdash (? ? % ?)
+ [rewrite > (div_mod (a \mod (b*c)) b)
+ [rewrite < assoc_plus;
+ rewrite > sym_times in ⊢ (? ? (? (? (? (? (? ? %) ?) ?) ?) ?) ?);
+ rewrite < assoc_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?);
+ rewrite > sym_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?);
+ rewrite > sym_times in ⊢ (? ? (? (? (? (? ? %) ?) ?) ?) ?);
+ rewrite < distr_times_plus;rewrite < sym_times in ⊢ (? ? (? (? (? % ?) ?) ?) ?);
+ rewrite > (div_plus_times b)
+ [rewrite > (div_plus_times c)
+ [reflexivity
+ |apply lt_times_to_lt_div;rewrite > sym_times in \vdash (? ? %);
+ apply lt_mod_m_m;unfold lt;rewrite > times_n_SO;apply le_times;assumption]
+ |apply lt_mod_m_m;assumption]
+ |assumption]
+ |unfold lt;rewrite > times_n_SO;apply le_times;assumption]
+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*(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;
+cut (O < log b n)
+ [|apply lt_O_log;
+ [apply lt_to_le;apply (trans_le ? ? ? H);apply (trans_le ? (sqrt n))
+ [apply lt_to_le;assumption
+ |apply le_sqrt_n_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*(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*(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*(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);
+ rewrite < assoc_plus in \vdash (? ? %);
+ rewrite > assoc_plus in ⊢ (? ? (? (? % ?) ?));
+ 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*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 ⊢ (? ? (? (? % ?) ?));
+ rewrite > assoc_plus in ⊢ (? ? (? % ?));
+ rewrite > sym_plus in \vdash (? ? %);
+ rewrite < assoc_plus in \vdash (? ? %);
+ rewrite > sym_plus in \vdash (? ? (? % ?));
+ apply le_plus
+ [rewrite < plus_n_Sm;rewrite < plus_n_O;apply le_div_plus_S;
+ assumption
+ |rewrite < plus_n_Sm;rewrite < plus_n_O;apply le_div_plus_S;
+ assumption]]
+ |rewrite < plus_n_Sm;rewrite < plus_n_O;apply (trans_le ? ? ? (le_div_plus_S ? ? ? ?));
+ [assumption
+ |apply le_S_S;apply le_plus
+ [rewrite > eq_div_div_div_times;
+ [apply le_n
+ |*:assumption]
+ |rewrite > eq_div_div_div_times
+ [apply le_n
+ |rewrite > minus_n_O in \vdash (? ? (? %));
+ rewrite < eq_minus_S_pred;apply lt_to_lt_O_minus;
+ apply (trans_le ? (log b (sqrt n * sqrt n)))
+ [elim daemon;
+ |apply le_log;
+ [assumption
+ |elim daemon]]
+ |assumption]]]]]]]
qed.
-*)
+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);
+*)
+*)
\ No newline at end of file