include "nat/sqrt.ma".
include "nat/chebyshev_teta.ma".
include "nat/chebyshev.ma".
+include "nat/o.ma".
+
+definition bertrand \def \lambda n.
+\exists p.n < p \land p \le 2*n \land (prime p).
definition not_bertrand \def \lambda n.
\forall p.n < p \to p \le 2*n \to \not (prime p).
+lemma not_not_bertrand_to_bertrand1: \forall n.
+\lnot (not_bertrand n) \to \forall x. n \le x \to x \le 2*n \to
+(\forall p.x < p \to p \le 2*n \to \not (prime p))
+\to \exists p.n < p \land p \le x \land (prime p).
+intros 4.elim H1
+ [apply False_ind.apply H.assumption
+ |apply (bool_elim ? (primeb (S n1)));intro
+ [apply (ex_intro ? ? (S n1)).
+ split
+ [split
+ [apply le_S_S.assumption
+ |apply le_n
+ ]
+ |apply primeb_true_to_prime.assumption
+ ]
+ |elim H3
+ [elim H7.clear H7.
+ elim H8.clear H8.
+ apply (ex_intro ? ? a).
+ split
+ [split
+ [assumption
+ |apply le_S.assumption
+ ]
+ |assumption
+ ]
+ |apply lt_to_le.assumption
+ |elim (le_to_or_lt_eq ? ? H7)
+ [apply H5;assumption
+ |rewrite < H9.
+ apply primeb_false_to_not_prime.
+ assumption
+ ]
+ ]
+ ]
+ ]
+qed.
+
+theorem not_not_bertrand_to_bertrand: \forall n.
+\lnot (not_bertrand n) \to bertrand n.
+unfold bertrand.intros.
+apply (not_not_bertrand_to_bertrand1 ? ? (2*n))
+ [assumption
+ |apply le_times_n.apply le_n_Sn
+ |apply le_n
+ |intros.apply False_ind.
+ apply (lt_to_not_le ? ? H1 H2)
+ ]
+qed.
+
(* not used
theorem divides_pi_p_to_divides: \forall p,n,b,g.prime p \to
divides p (pi_p n b g) \to \exists i. (i < n \and (b i = true \and
]
qed.
-(*
-theorem tech: \forall n. 2*(3*(S(log 2 (2*n)))/4) < sqrt (2*n) \to
-(sqrt(2*n)/2)*S(log 2 (2*n)) < 2*n / 3.
+theorem tech1: \forall a,b,c,d.O < b \to O < d \to
+(a/b)*(c/d) \le (a*c)/(b*d).
+intros.
+apply le_times_to_le_div
+ [rewrite > (times_n_O O).
+ apply lt_times;assumption
+ |rewrite > assoc_times.
+ rewrite < assoc_times in ⊢ (? (? ? %) ?).
+ rewrite < sym_times in ⊢ (? (? ? (? % ?)) ?).
+ rewrite > assoc_times.
+ rewrite < assoc_times.
+ apply le_times;
+ rewrite > sym_times;apply le_times_div_m_m;assumption
+ ]
+qed.
+
+theorem tech: \forall n. 2*(S(log 2 (2*n))) \le sqrt (2*n) \to
+(sqrt(2*n)/2)*S(log 2 (2*n)) \le 2*n / 4.
+intros.
+cut (4*(S(log 2 (2*n))) \le 2* sqrt(2*n))
+ [rewrite > sym_times.
+ apply le_times_to_le_div
+ [apply lt_O_S
+ |rewrite < assoc_times.
+ apply (trans_le ? (2*sqrt(2*n)*(sqrt (2*n)/2)))
+ [apply le_times_l.assumption
+ |apply (trans_le ? ((2*sqrt(2*n)*(sqrt(2*n))/2)))
+ [apply le_times_div_div_times.
+ apply lt_O_S
+ |rewrite > assoc_times.
+ rewrite > sym_times.
+ rewrite > lt_O_to_div_times.
+ apply leq_sqrt_n.
+ apply lt_O_S
+ ]
+ ]
+ ]
+ |change in ⊢ (? (? % ?) ?) with (2*2).
+ rewrite > assoc_times.
+ apply le_times_r.
+ assumption
+ ]
+qed.
+
+theorem lt_div_S_div: \forall n,m. O < m \to exp m 2 \le n \to
+n/(S m) < n/m.
+intros.
+apply lt_times_to_lt_div.
+apply (lt_to_le_to_lt ? (S(n/m)*m))
+ [apply lt_div_S.assumption
+ |rewrite > sym_times in ⊢ (? ? %). simplify.
+ rewrite > sym_times in ⊢ (? ? (? ? %)).
+ apply le_plus_l.
+ apply le_times_to_le_div
+ [assumption
+ |rewrite < exp_SSO.
+ assumption
+ ]
+ ]
+qed.
+
+theorem exp_plus_SSO: \forall a,b. exp (a+b) 2 = (exp a 2) + 2*a*b + (exp b 2).
+intros.
+rewrite > exp_SSO.
+rewrite > distr_times_plus.
+rewrite > times_plus_l.
+rewrite < exp_SSO.
+rewrite > assoc_plus.
+rewrite > assoc_plus.
+apply eq_f.
+rewrite > times_plus_l.
+rewrite < exp_SSO.
+rewrite < assoc_plus.
+rewrite < sym_times.
+rewrite > plus_n_O in ⊢ (? ? (? (? ? %) ?) ?).
+rewrite > assoc_times.
+apply eq_f2;reflexivity.
+qed.
+
+theorem tech3: \forall n. (exp 2 8) \le n \to 2*(S(log 2 (2*n))) \le sqrt (2*n).
intros.
- *)
+lapply (le_log 2 ? ? (le_n ?) H) as H1.
+rewrite > exp_n_SO in ⊢ (? (? ? (? (? ? (? % ?)))) ?).
+rewrite > log_exp
+ [rewrite > sym_plus.
+ rewrite > plus_n_Sm.
+ unfold sqrt.
+ apply f_m_to_le_max
+ [apply le_times_r.
+ apply (trans_le ? (2*log 2 n))
+ [rewrite < times_SSO_n.
+ apply le_plus_r.
+ apply (trans_le ? 8)
+ [apply leb_true_to_le.reflexivity
+ |rewrite < (eq_log_exp 2)
+ [assumption
+ |apply le_n
+ ]
+ ]
+ |apply (trans_le ? ? ? ? (le_exp_log 2 ? ? )).
+ apply le_times_SSO_n_exp_SSO_n.
+ apply (lt_to_le_to_lt ? ? ? ? H).
+ apply leb_true_to_le.reflexivity
+ ]
+ |apply le_to_leb_true.
+ rewrite > assoc_times.
+ apply le_times_r.
+ rewrite > sym_times.
+ rewrite > assoc_times.
+ rewrite < exp_SSO.
+ rewrite > exp_plus_SSO.
+ rewrite > distr_times_plus.
+ rewrite > distr_times_plus.
+ rewrite > assoc_plus.
+ apply (trans_le ? (4*exp (log 2 n) 2))
+ [change in ⊢ (? ? (? % ?)) with (2*2).
+ rewrite > assoc_times in ⊢ (? ? %).
+ rewrite < times_SSO_n in ⊢ (? ? %).
+ apply le_plus_r.
+ rewrite < times_SSO_n in ⊢ (? ? %).
+ apply le_plus
+ [rewrite > sym_times in ⊢ (? (? ? %) ?).
+ rewrite < assoc_times.
+ rewrite < assoc_times.
+ change in ⊢ (? (? % ?) ?) with 8.
+ rewrite > exp_SSO.
+ apply le_times_l.
+ (* strange things here *)
+ rewrite < (eq_log_exp 2)
+ [assumption
+ |apply le_n
+ ]
+ |apply (trans_le ? (log 2 n))
+ [change in ⊢ (? % ?) with 8.
+ rewrite < (eq_log_exp 2)
+ [assumption
+ |apply le_n
+ ]
+ |rewrite > exp_n_SO in ⊢ (? % ?).
+ apply le_exp
+ [apply lt_O_log
+ [apply (lt_to_le_to_lt ? ? ? ? H).
+ apply leb_true_to_le.reflexivity
+ |apply (lt_to_le_to_lt ? ? ? ? H).
+ apply leb_true_to_le.reflexivity
+ ]
+ |apply le_n_Sn
+ ]
+ ]
+ ]
+ |change in ⊢ (? (? % ?) ?) with (exp 2 2).
+ apply (trans_le ? ? ? ? (le_exp_log 2 ? ?))
+ [apply le_times_exp_n_SSO_exp_SSO_n
+ [apply le_n
+ |change in ⊢ (? % ?) with 8.
+ rewrite < (eq_log_exp 2)
+ [assumption
+ |apply le_n
+ ]
+ ]
+ |apply (lt_to_le_to_lt ? ? ? ? H).
+ apply leb_true_to_le.reflexivity
+ ]
+ ]
+ ]
+ |apply le_n
+ |apply (lt_to_le_to_lt ? ? ? ? H).
+ apply leb_true_to_le.reflexivity
+ ]
+qed.
+
+theorem le_to_bertrand:
+\forall n. (exp 2 8) \le n \to bertrand n.
+intros.
+apply not_not_bertrand_to_bertrand.unfold.intro.
+absurd (2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)))
+ [apply not_bertrand_to_le2
+ [apply (trans_le ? ? ? ? H).
+ apply le_exp
+ [apply lt_O_S
+ |apply le_n_Sn
+ ]
+ |assumption
+ ]
+ |apply lt_to_not_le.
+ apply (le_to_lt_to_lt ? ? ? ? (lt_div_S_div ? ? ? ?))
+ [apply tech.apply tech3.assumption
+ |apply lt_O_S
+ |apply (trans_le ? (2*exp 2 8))
+ [apply leb_true_to_le.reflexivity
+ |apply le_times_r.assumption
+ ]
+ ]
+ ]
+qed.
+
+(* test
+theorem mod_exp: eqb (mod (exp 2 8) 13) O = false.
+reflexivity.
+*)
projects / helm.git / blobdiff