--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / Matita is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+include "nat/sqrt.ma".
+include "nat/chebyshev_teta.ma".
+include "nat/chebyshev.ma".
+
+definition not_bertrand \def \lambda n.
+\forall p.n < p \to p \le 2*n \to \not (prime p).
+
+(* 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
+divides p (g i))).
+intros 2.elim n
+ [simplify in H1.
+ apply False_ind.
+ apply (le_to_not_lt p 1)
+ [apply divides_to_le
+ [apply le_n
+ |assumption
+ ]
+ |elim H.assumption
+ ]
+ |apply (bool_elim ? (b n1));intro
+ [rewrite > (true_to_pi_p_Sn ? ? ? H3) in H2.
+ elim (divides_times_to_divides ? ? ? H1 H2)
+ [apply (ex_intro ? ? n1).
+ split
+ [apply le_n
+ |split;assumption
+ ]
+ |elim (H ? ? H1 H4).
+ elim H5.
+ apply (ex_intro ? ? a).
+ split
+ [apply lt_to_le.apply le_S_S.assumption
+ |assumption
+ ]
+ ]
+ |rewrite > (false_to_pi_p_Sn ? ? ? H3) in H2.
+ elim (H ? ? H1 H2).
+ elim H4.
+ apply (ex_intro ? ? a).
+ split
+ [apply lt_to_le.apply le_S_S.assumption
+ |assumption
+ ]
+ ]
+ ]
+qed.
+
+theorem divides_B: \forall n,p.prime p \to p \divides (B n) \to
+p \le n \land \exists i.mod (n /(exp p (S i))) 2 \neq O.
+intros.
+unfold B in H1.
+elim (divides_pi_p_to_divides ? ? ? ? H H1).
+elim H2.clear H2.
+elim H4.clear H4.
+elim (divides_pi_p_to_divides ? ? ? ? H H5).clear H5.
+elim H4.clear H4.
+elim H6.clear H6.
+cut (p = a)
+ [split
+ [rewrite > Hcut.apply le_S_S_to_le.assumption
+ |apply (ex_intro ? ? a1).
+ rewrite > Hcut.
+ intro.
+ change in H7:(? ? %) with (exp a ((n/(exp a (S a1))) \mod 2)).
+ rewrite > H6 in H7.
+ simplify in H7.
+ absurd (p \le 1)
+ [apply divides_to_le[apply lt_O_S|assumption]
+ |apply lt_to_not_le.elim H.assumption
+ ]
+ ]
+ |apply (divides_exp_to_eq ? ? ? H ? H7).
+ apply primeb_true_to_prime.
+ assumption
+ ]
+qed.
+*)
+
+definition k \def \lambda n,p.
+sigma_p (log p n) (λi:nat.true) (λi:nat.((n/(exp p (S i))\mod 2))).
+
+theorem le_k: \forall n,p. k n p \le log p n.
+intros.unfold k.elim (log p n)
+ [apply le_n
+ |rewrite > true_to_sigma_p_Sn
+ [rewrite > plus_n_SO.
+ rewrite > sym_plus in ⊢ (? ? %).
+ apply le_plus
+ [apply le_S_S_to_le.
+ apply lt_mod_m_m.
+ apply lt_O_S
+ |assumption
+ ]
+ |reflexivity
+ ]
+ ]
+qed.
+
+definition B1 \def
+\lambda n. pi_p (S n) primeb (\lambda p.(exp p (k n p))).
+
+theorem eq_B_B1: \forall n. B n = B1 n.
+intros.unfold B.unfold B1.
+apply eq_pi_p
+ [intros.reflexivity
+ |intros.unfold k.
+ apply exp_sigma_p1
+ ]
+qed.
+
+definition B_split1 \def \lambda n.
+pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb (k n p) 1)* (k n p)))).
+
+definition B_split2 \def \lambda n.
+pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb 2 (k n p))* (k n p)))).
+
+theorem eq_B1_times_B_split1_B_split2: \forall n.
+B1 n = B_split1 n * B_split2 n.
+intro.unfold B1.unfold B_split1.unfold B_split2.
+rewrite < times_pi_p.
+apply eq_pi_p
+ [intros.reflexivity
+ |intros.apply (bool_elim ? (leb (k n x) 1));intro
+ [rewrite > (lt_to_leb_false 2 (k n x))
+ [simplify.rewrite < plus_n_O.
+ rewrite < times_n_SO.reflexivity
+ |apply le_S_S.apply leb_true_to_le.assumption
+ ]
+ |rewrite > (le_to_leb_true 2 (k n x))
+ [simplify.rewrite < plus_n_O.
+ rewrite < plus_n_O.reflexivity
+ |apply not_le_to_lt.apply leb_false_to_not_le.assumption
+ ]
+ ]
+ ]
+qed.
+
+lemma lt_div_to_times: \forall n,m,q. O < q \to n/q < m \to n < q*m.
+intros.
+cut (O < m) as H2
+ [apply not_le_to_lt.
+ intro.apply (lt_to_not_le ? ? H1).
+ apply le_times_to_le_div;assumption
+ |apply (ltn_to_ltO ? ? H1)
+ ]
+qed.
+
+lemma lt_to_div_O:\forall n,m. n < m \to n / m = O.
+intros.
+apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n)
+ [apply div_mod_spec_div_mod.
+ apply (ltn_to_ltO ? ? H)
+ |apply div_mod_spec_intro
+ [assumption
+ |reflexivity
+ ]
+ ]
+qed.
+
+(* the value of n could be smaller *)
+lemma k1: \forall n,p. 18 \le n \to p \le n \to 2*n/ 3 < p\to k (2*n) p = O.
+intros.unfold k.
+elim (log p (2*n))
+ [reflexivity
+ |rewrite > true_to_sigma_p_Sn
+ [rewrite > H3.
+ rewrite < plus_n_O.
+ cases n1
+ [rewrite < exp_n_SO.
+ cut (2*n/p = 2) as H4
+ [rewrite > H4.reflexivity
+ |apply lt_to_le_times_to_lt_S_to_div
+ [apply (ltn_to_ltO ? ? H2)
+ |rewrite < sym_times.
+ apply le_times_r.
+ assumption
+ |rewrite > sym_times in ⊢ (? ? %).
+ apply lt_div_to_times
+ [apply lt_O_S
+ |assumption
+ ]
+ ]
+ ]
+ |cut (2*n/(p)\sup(S (S n2)) = O) as H4
+ [rewrite > H4.reflexivity
+ |apply lt_to_div_O.
+ apply (le_to_lt_to_lt ? (exp ((2*n)/3) 2))
+ [apply (le_times_to_le (exp 3 2))
+ [apply leb_true_to_le.reflexivity
+ |rewrite > sym_times in ⊢ (? ? %).
+ rewrite > times_exp.
+ apply (trans_le ? (exp n 2))
+ [rewrite < assoc_times.
+ rewrite > exp_SSO in ⊢ (? ? %).
+ apply le_times_l.
+ assumption
+ |apply monotonic_exp1.
+ apply (le_plus_to_le 3).
+ change in ⊢ (? ? %) with ((S(2*n/3))*3).
+ apply (trans_le ? (2*n))
+ [simplify in ⊢ (? ? %).
+ rewrite < plus_n_O.
+ apply le_plus_l.
+ apply (trans_le ? 18 ? ? H).
+ apply leb_true_to_le.reflexivity
+ |apply lt_to_le.
+ apply lt_div_S.
+ apply lt_O_S
+ ]
+ ]
+ ]
+ |apply (lt_to_le_to_lt ? (exp p 2))
+ [apply lt_exp1
+ [apply lt_O_S
+ |assumption
+ ]
+ |apply le_exp
+ [apply (ltn_to_ltO ? ? H2)
+ |apply le_S_S.apply le_S_S.apply le_O_n
+ ]
+ ]
+ ]
+ ]
+ ]
+ |reflexivity
+ ]
+ ]
+qed.
+
+theorem le_B_split1_teta:\forall n.18 \le n \to not_bertrand n \to
+B_split1 (2*n) \le teta (2 * n / 3).
+intros.unfold B_split1.unfold teta.
+apply (trans_le ? (pi_p (S (2*n)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
+ [apply le_pi_p.intros.
+ apply le_exp
+ [apply prime_to_lt_O.apply primeb_true_to_prime.assumption
+ |apply (bool_elim ? (leb (k (2*n) i) 1));intro
+ [elim (le_to_or_lt_eq ? ? (leb_true_to_le ? ? H4))
+ [lapply (le_S_S_to_le ? ? H5) as H6.
+ apply (le_n_O_elim ? H6).
+ rewrite < times_n_O.
+ apply le_n
+ |rewrite > (eq_to_eqb_true ? ? H5).
+ rewrite > H5.apply le_n
+ ]
+ |apply le_O_n
+ ]
+ ]
+ |apply (trans_le ? (pi_p (S (2*n/3)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
+ [apply (eq_ind ? ? ? (le_n ?)).
+ apply or_false_eq_SO_to_eq_pi_p
+ [apply le_S_S.
+ apply le_times_to_le_div2
+ [apply lt_O_S
+ |rewrite > sym_times in ⊢ (? ? %).
+ apply le_times_n.
+ apply leb_true_to_le.reflexivity
+ ]
+ |intros.
+ unfold not_bertrand in H1.
+ elim (decidable_le (S n) i)
+ [left.
+ apply not_prime_to_primeb_false.
+ apply H1
+ [assumption
+ |apply le_S_S_to_le.assumption
+ ]
+ |right.
+ rewrite > k1
+ [reflexivity
+ |assumption
+ |apply le_S_S_to_le.
+ apply not_le_to_lt.assumption
+ |assumption
+ ]
+ ]
+ ]
+ |apply le_pi_p.intros.
+ elim (eqb (k (2*n) i) 1)
+ [rewrite < exp_n_SO.apply le_n
+ |simplify.apply prime_to_lt_O.
+ apply primeb_true_to_prime.
+ assumption
+ ]
+ ]
+ ]
+qed.
+
+theorem le_B_split2_exp: \forall n. exp 2 7 \le n \to
+B_split2 (2*n) \le exp (2*n) (pred(sqrt(2*n)/2)).
+intros.unfold B_split2.
+cut (O < n)
+ [apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb
+ (λp:nat.(p)\sup(bool_to_nat (leb 2 (k (2*n) p))*k (2*n) p))))
+ [apply (eq_ind ? ? ? (le_n ?)).
+ apply or_false_eq_SO_to_eq_pi_p
+ [apply le_S_S.
+ apply le_sqrt_n_n
+ |intros.
+ apply (bool_elim ? (leb 2 (k (2*n) i)));intro
+ [apply False_ind.
+ apply (lt_to_not_le ? ? H1).unfold sqrt.
+ apply f_m_to_le_max
+ [apply le_S_S_to_le.assumption
+ |apply le_to_leb_true.
+ rewrite < exp_SSO.
+ apply not_lt_to_le.intro.
+ apply (le_to_not_lt 2 (log i (2*n)))
+ [apply (trans_le ? (k (2*n) i))
+ [apply leb_true_to_le.assumption
+ |apply le_k
+ ]
+ |apply le_S_S.unfold log.apply f_false_to_le_max
+ [apply (ex_intro ? ? O).split
+ [apply le_O_n
+ |apply le_to_leb_true.simplify.
+ apply (trans_le ? n)
+ [assumption.
+ |apply le_plus_n_r
+ ]
+ ]
+ |intros.apply lt_to_leb_false.
+ apply (lt_to_le_to_lt ? (exp i 2))
+ [assumption
+ |apply le_exp
+ [apply (ltn_to_ltO ? ? H1)
+ |assumption
+ ]
+ ]
+ ]
+ ]
+ ]
+ |right.reflexivity
+ ]
+ ]
+ |apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb (λp:nat.2*n)))
+ [apply le_pi_p.intros.
+ apply (trans_le ? (exp i (log i (2*n))))
+ [apply le_exp
+ [apply prime_to_lt_O.
+ apply primeb_true_to_prime.
+ assumption
+ |apply (bool_elim ? (leb 2 (k (2*n) i)));intro
+ [simplify in ⊢ (? (? % ?) ?).
+ rewrite > sym_times.
+ rewrite < times_n_SO.
+ apply le_k
+ |apply le_O_n
+ ]
+ ]
+ |apply le_exp_log.
+ rewrite > (times_n_O O) in ⊢ (? % ?).
+ apply lt_times
+ [apply lt_O_S
+ |assumption
+ ]
+ ]
+ |apply (trans_le ? (exp (2*n) (prim(sqrt (2*n)))))
+ [unfold prim.
+ apply (eq_ind ? ? ? (le_n ?)).
+ apply exp_sigma_p
+ |apply le_exp
+ [rewrite > (times_n_O O) in ⊢ (? % ?).
+ apply lt_times
+ [apply lt_O_S
+ |assumption
+ ]
+ |apply le_prim_n3.
+ unfold sqrt.
+ apply f_m_to_le_max
+ [apply (trans_le ? (2*(exp 2 7)))
+ [apply leb_true_to_le.reflexivity
+ |apply le_times_r.assumption
+ ]
+ |apply le_to_leb_true.
+ apply (trans_le ? (2*(exp 2 7)))
+ [apply leb_true_to_le.reflexivity
+ |apply le_times_r.assumption
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ |apply (lt_to_le_to_lt ? ? ? ? H).
+ apply leb_true_to_le.reflexivity
+ ]
+qed.
+
+theorem not_bertrand_to_le_B:
+\forall n.exp 2 7 \le n \to not_bertrand n \to
+B (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (pred(sqrt(2*n)/2))).
+intros.
+rewrite > eq_B_B1.
+rewrite > eq_B1_times_B_split1_B_split2.
+apply le_times
+ [apply (trans_le ? (teta ((2*n)/3)))
+ [apply le_B_split1_teta
+ [apply (trans_le ? ? ? ? H).
+ apply leb_true_to_le.reflexivity
+ |assumption
+ ]
+ |apply le_teta
+ ]
+ |apply le_B_split2_exp.
+ assumption
+ ]
+qed.
+
+(*
+theorem not_bertrand_to_le1:
+\forall n.18 \le n \to not_bertrand n \to
+exp 2 (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (S(sqrt(2*n)))).
+*)
+
+theorem le_times_div_m_m: \forall n,m. O < m \to n/m*m \le n.
+intros.
+rewrite > (div_mod n m) in ⊢ (? ? %)
+ [apply le_plus_n_r
+ |assumption
+ ]
+qed.
+
+theorem not_bertrand_to_le1:
+\forall n.exp 2 7 \le n \to not_bertrand n \to
+(exp 2 (2*n / 3)) \le (exp (2*n) (sqrt(2*n)/2)).
+intros.
+apply (le_times_to_le (exp 2 (2*(2 * n / 3))))
+ [apply lt_O_exp.apply lt_O_S
+ |rewrite < exp_plus_times.
+ apply (trans_le ? (exp 2 (2*n)))
+ [apply le_exp
+ [apply lt_O_S
+ |rewrite < sym_plus.
+ change in ⊢ (? % ?) with (3*(2*n/3)).
+ rewrite > sym_times.
+ apply le_times_div_m_m.
+ apply lt_O_S
+ ]
+(* weaker form
+ rewrite < distr_times_plus.
+ apply le_times_r.
+ apply (trans_le ? ((2*n + n)/3))
+ [apply le_plus_div.apply lt_O_S
+ |rewrite < sym_plus.
+ change in ⊢ (? (? % ?) ?) with (3*n).
+ rewrite < sym_times.
+ rewrite > lt_O_to_div_times
+ [apply le_n
+ |apply lt_O_S
+ ]
+ ]
+ ] *)
+ |apply (trans_le ? (2*n*B(2*n)))
+ [apply le_exp_B.
+ apply (trans_le ? ? ? ? H).
+ apply leb_true_to_le.reflexivity
+ |rewrite > S_pred in ⊢ (? ? (? ? (? ? %)))
+ [rewrite > exp_S.
+ rewrite < assoc_times.
+ rewrite < sym_times in ⊢ (? ? (? % ?)).
+ rewrite > assoc_times in ⊢ (? ? %).
+ apply le_times_r.
+ apply not_bertrand_to_le_B;assumption
+ |apply le_times_to_le_div
+ [apply lt_O_S
+ |apply (trans_le ? (sqrt (exp 2 8)))
+ [apply leb_true_to_le.reflexivity
+ |apply monotonic_sqrt.
+ change in ⊢ (? % ?) with (2*(exp 2 7)).
+ apply le_times_r.
+ assumption
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+qed.
+
+theorem not_bertrand_to_le2:
+\forall n.exp 2 7 \le n \to not_bertrand n \to
+2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)).
+intros.
+rewrite < (eq_log_exp 2)
+ [apply (trans_le ? (log 2 ((exp (2*n) (sqrt(2*n)/2)))))
+ [apply le_log
+ [apply le_n
+ |apply not_bertrand_to_le1;assumption
+ ]
+ |apply log_exp1.
+ apply le_n
+ ]
+ |apply le_n
+ ]
+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.
+intros.
+ *)
definition prim: nat \to nat \def
\lambda n. sigma_p (S n) primeb (\lambda p.(S O)).
+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.
+
+(* si dovrebbe poter migliorare *)
+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)).
reflexivity.
qed.
-(* da spostare *)
-theorem or_eq_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.reflexivity
- |elim H.elim H1
- [apply (ex_intro ? ? a).
- right.apply eq_f.assumption
- |apply (ex_intro ? ? (S a)).
- left.rewrite > H2.
- apply sym_eq.
- apply times_SSO
- ]
- ]
-qed.
-
(*
(* a better result *)
theorem le_A_exp3: \forall n. S O < n \to
qed.
theorem le_priml: \forall n. O < n \to
-(S(S O))*n \le (S (log (S(S O)) ((S(S O))*n)))*S(prim ((S(S O))*n)).
+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)))))))
]
qed.
+(* 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 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 prim_SSSSSSO: \forall n.30\le n \to O < prim (8*n) - prim n.
+intros.
+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.
+*)
+
+
+
projects / helm.git / commitdiff