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 / blobdiff