(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/chebishev".
-
include "nat/log.ma".
include "nat/pi_p.ma".
include "nat/factorization.ma".
include "nat/factorial2.ma".
+include "nat/o.ma".
definition prim: nat \to nat \def
-\lambda n. sigma_p (S n) primeb (\lambda p.(S O)).
+\lambda n. sigma_p (S n) primeb (\lambda p.1).
+
+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.
+
+(* la prova potrebbe essere migliorata *)
+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)).
]
qed.
+(* an equivalent formulation for psi *)
definition A': nat \to nat \def
\lambda n. pi_p (S n) primeb
(\lambda p.(pi_p (log p n) (\lambda i.true) (\lambda i.p))).
]
]
qed.
-
+
theorem lt_max_to_pi_p_primeb: \forall q,m. O < m \to max m (\lambda i.primeb i \land divides_b i m) < q \to
m = pi_p q (\lambda i.primeb i \land divides_b i m) (\lambda p.exp p (ord m p)).
intro.elim q
]
]
qed.
-
+
+(* factorization of n into primes *)
theorem pi_p_primeb_divides_b: \forall n. O < n \to
n = pi_p (S n) (\lambda i.primeb i \land divides_b i n) (\lambda p.exp p (ord n p)).
intros.
assumption.
qed.
-theorem le_ord_log: \forall n,p. O < n \to S O < p \to
+theorem le_ord_log: \forall n,p. O < n \to 1 < p \to
ord n p \le log p n.
intros.
rewrite > (exp_ord p) in ⊢ (? ? (? ? %))
theorem eq_ord_sigma_p:
\forall n,m,x. O < n \to prime x \to
exp x m \le n \to n < exp x (S m) \to
-ord n x=sigma_p m (λi:nat.divides_b (x\sup (S i)) n) (λx:nat.S O).
+ord n x=sigma_p m (λi:nat.divides_b (x\sup (S i)) n) (λx:nat.1).
intros.
lapply (prime_to_lt_SO ? H1).
rewrite > (exp_ord x n) in ⊢ (? ? ? (? ? (λi:?.? ? %) ?))
]
qed.
+(* the factorial function *)
theorem eq_fact_pi_p:\forall n. fact n =
pi_p (S n) (\lambda i.leb (S O) i) (\lambda i.i).
intro.elim n
]
qed.
+(* still another characterization of the factorial *)
theorem fact_pi_p: \forall n. fact n =
pi_p (S n) primeb
(\lambda p.(pi_p (log p n)
intros.
rewrite > eq_fact_pi_p.
apply (trans_eq ? ?
- (pi_p (S n) (λi:nat.leb (S O) i)
- (λn.pi_p (S n) primeb
- (\lambda p.(pi_p (log p n)
- (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))))))
+ (pi_p (S n) (λm:nat.leb (S O) m)
+ (λm.pi_p (S m) primeb
+ (\lambda p.(pi_p (log p m)
+ (\lambda i.divides_b (exp p (S i)) m) (\lambda i.p))))))
[apply eq_pi_p1;intros
[reflexivity
|apply pi_p_primeb1.
apply leb_true_to_le.assumption
]
|apply (trans_eq ? ?
- (pi_p (S n) (λi:nat.leb (S O) i)
- (λn:nat
- .pi_p (S n) (\lambda p.primeb p\land leb p n)
- (λp:nat.pi_p (log p n) (λi:nat.divides_b ((p)\sup(S i)) n) (λi:nat.p)))))
+ (pi_p (S n) (λm:nat.leb (S O) m)
+ (λm:nat
+ .pi_p (S m) (\lambda p.primeb p\land leb p m)
+ (λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))))
[apply eq_pi_p1
[intros.reflexivity
|intros.apply eq_pi_p1
]
]
|apply (trans_eq ? ?
- (pi_p (S n) (λi:nat.leb (S O) i)
+ (pi_p (S n) (λm:nat.leb (S O) m)
(λm:nat
.pi_p (S n) (λp:nat.primeb p∧leb p m)
(λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))))
[apply prime_to_lt_SO.
apply primeb_true_to_prime.
assumption
- |apply (lt_to_le_to_lt ? x)
- [apply prime_to_lt_O.
- apply primeb_true_to_prime.
- assumption
- |apply leb_true_to_le.
- assumption
- ]
|apply le_S_S_to_le.
assumption
]
|
*)
-theorem fact_pi_p2: \forall n. fact ((S(S O))*n) =
-pi_p (S ((S(S O))*n)) primeb
- (\lambda p.(pi_p (log p ((S(S O))*n))
- (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))*(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O)))))))).
+theorem fact_pi_p2: \forall n. fact (2*n) =
+pi_p (S (2*n)) primeb
+ (\lambda p.(pi_p (log p (2*n))
+ (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i))))*(exp p (mod (2*n /(exp p (S i))) 2)))))).
intros.rewrite > fact_pi_p.
apply eq_pi_p1
[intros.reflexivity
]
qed.
-theorem fact_pi_p3: \forall n. fact ((S(S O))*n) =
-pi_p (S ((S(S O))*n)) primeb
- (\lambda p.(pi_p (log p ((S(S O))*n))
- (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))*
-pi_p (S ((S(S O))*n)) primeb
- (\lambda p.(pi_p (log p ((S(S O))*n))
- (\lambda i.true) (\lambda i.(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O))))))).
+theorem fact_pi_p3: \forall n. fact (2*n) =
+pi_p (S (2*n)) primeb
+ (\lambda p.(pi_p (log p (2*n))
+ (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i))))))))*
+pi_p (S (2*n)) primeb
+ (\lambda p.(pi_p (log p (2*n))
+ (\lambda i.true) (\lambda i.(exp p (mod (2*n /(exp p (S i))) 2))))).
intros.
rewrite < times_pi_p.
rewrite > fact_pi_p2.
]
qed.
-theorem pi_p_primeb4: \forall n. S O < n \to
-pi_p (S ((S(S O))*n)) primeb
- (\lambda p.(pi_p (log p ((S(S O))*n))
- (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
+theorem pi_p_primeb4: \forall n. 1 < n \to
+pi_p (S (2*n)) primeb
+ (\lambda p.(pi_p (log p (2*n))
+ (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i))))))))
=
pi_p (S n) primeb
- (\lambda p.(pi_p (log p (S(S O)*n))
- (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
+ (\lambda p.(pi_p (log p (2*n))
+ (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i)))))))).
intros.
apply or_false_eq_SO_to_eq_pi_p
[apply le_S_S.
]
qed.
-theorem pi_p_primeb5: \forall n. S O < n \to
-pi_p (S ((S(S O))*n)) primeb
+theorem pi_p_primeb5: \forall n. 1 < n \to
+pi_p (S (2*n)) primeb
(\lambda p.(pi_p (log p ((S(S O))*n))
- (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
+ (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i))))))))
=
pi_p (S n) primeb
(\lambda p.(pi_p (log p n)
- (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
+ (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i)))))))).
intros.
rewrite > (pi_p_primeb4 ? H).
apply eq_pi_p1;intros
[apply prime_to_lt_SO.
apply primeb_true_to_prime.
assumption
- |apply lt_to_le.assumption
|apply le_times_n.
apply lt_O_S
]
qed.
theorem exp_fact_SSO: \forall n.
-exp (fact n) (S(S O))
+exp (fact n) 2
=
pi_p (S n) primeb
(\lambda p.(pi_p (log p n)
- (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
+ (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i)))))))).
intros.
rewrite > fact_pi_p.
rewrite < exp_pi_p.
(\lambda p.(pi_p (log p n)
(\lambda i.true) (\lambda i.(exp p (mod (n /(exp p (S i))) (S(S O))))))).
+theorem B_SSSO: B 3 = 6.
+reflexivity.
+qed.
+
+theorem B_SSSSO: B 4 = 6.
+reflexivity.
+qed.
+
+theorem B_SSSSSO: B 5 = 30.
+reflexivity.
+qed.
+
+theorem B_SSSSSSO: B 6 = 20.
+reflexivity.
+qed.
+
+theorem B_SSSSSSSO: B 7 = 140.
+reflexivity.
+qed.
+
+theorem B_SSSSSSSSO: B 8 = 70.
+reflexivity.
+qed.
+
theorem eq_fact_B:\forall n.S O < n \to
-fact ((S(S O))*n) = exp (fact n) (S(S O)) * B((S(S O))*n).
+fact (2*n) = exp (fact n) 2 * B(2*n).
intros. unfold B.
rewrite > fact_pi_p3.
apply eq_f2
]
qed.
+theorem le_B_A4: \forall n. O < n \to (S(S O))* B ((S(S(S(S O))))*n) \le A ((S(S(S(S O))))*n).
+intros.unfold B.
+rewrite > eq_A_A'.
+unfold A'.
+cut ((S(S O)) < (S ((S(S(S(S O))))*n)))
+ [cut (O<log (S(S O)) ((S(S(S(S O))))*n))
+ [rewrite > (pi_p_gi ? ? (S(S O)))
+ [rewrite > (pi_p_gi ? ? (S(S O))) in ⊢ (? ? %)
+ [rewrite < assoc_times.
+ apply le_times
+ [rewrite > (pi_p_gi ? ? O)
+ [rewrite > (pi_p_gi ? ? O) in ⊢ (? ? %)
+ [rewrite < assoc_times.
+ apply le_times
+ [rewrite < exp_n_SO.
+ change in ⊢ (? (? ? (? ? (? (? (? % ?) ?) ?))) ?)
+ with ((S(S O))*(S(S O))).
+ rewrite > assoc_times.
+ rewrite > sym_times in ⊢ (? (? ? (? ? (? (? % ?) ?))) ?).
+ rewrite > lt_O_to_div_times
+ [rewrite > divides_to_mod_O
+ [apply le_n
+ |apply lt_O_S
+ |apply (witness ? ? n).reflexivity
+ ]
+ |apply lt_O_S
+ ]
+ |apply le_pi_p.intros.
+ rewrite > exp_n_SO in ⊢ (? ? %).
+ apply le_exp
+ [apply lt_O_S
+ |apply le_S_S_to_le.
+ apply lt_mod_m_m.
+ apply lt_O_S
+ ]
+ ]
+ |assumption
+ |reflexivity
+ ]
+ |assumption
+ |reflexivity
+ ]
+ |apply le_pi_p.intros.
+ apply le_pi_p.intros.
+ rewrite > exp_n_SO in ⊢ (? ? %).
+ apply le_exp
+ [apply prime_to_lt_O.
+ apply primeb_true_to_prime.
+ apply (andb_true_true ? ? H2)
+ |apply le_S_S_to_le.
+ apply lt_mod_m_m.
+ apply lt_O_S
+ ]
+ ]
+ |assumption
+ |reflexivity
+ ]
+ |assumption
+ |reflexivity
+ ]
+ |apply lt_O_log
+ [rewrite > (times_n_O (S(S(S(S O))))) in ⊢ (? % ?).
+ apply lt_times_r1
+ [apply lt_O_S
+ |assumption
+ ]
+ |rewrite > times_n_SO in ⊢ (? % ?).
+ apply le_times
+ [apply le_S.apply le_S.apply le_n
+ |assumption
+ ]
+ ]
+ ]
+ |apply le_S_S.
+ rewrite > times_n_SO in ⊢ (? % ?).
+ apply le_times
+ [apply le_S.apply le_n_Sn
+ |assumption
+ ]
+ ]
+qed.
+
+(* not usefull
theorem le_fact_A:\forall n.S O < n \to
-fact ((S(S O))*n) \le exp (fact n) (S(S O)) * A ((S(S O))*n).
+fact (2*n) \le exp (fact n) 2 * A (2*n).
intros.
rewrite > eq_fact_B
[apply le_times_r.
apply le_B_A
|assumption
]
-qed.
+qed. *)
theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
-B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
+B (2*n) \le exp 2 (pred (2*n)).
intros.
apply (le_times_to_le (exp (fact n) (S(S O))))
[apply lt_O_exp.
qed.
theorem le_B_exp: \forall n.
-B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
+B (2*n) \le exp 2 (pred (2*n)).
intro.cases n
[apply le_n
|cases n1
- [simplify.apply le_S.apply le_S.apply le_n
+ [simplify.apply le_n
|apply lt_SO_to_le_B_exp.
apply le_S_S.apply lt_O_S.
]
]
qed.
+theorem lt_SSSSO_to_le_B_exp: \forall n.4 < n \to
+B (2*n) \le exp 2 ((2*n)-2).
+intros.
+apply (le_times_to_le (exp (fact n) (S(S O))))
+ [apply lt_O_exp.
+ apply lt_O_fact
+ |rewrite < eq_fact_B
+ [rewrite < sym_times in ⊢ (? ? %).
+ rewrite > exp_SSO.
+ rewrite < assoc_times.
+ apply lt_SSSSO_to_fact.assumption
+ |apply lt_to_le.apply lt_to_le.
+ apply lt_to_le.assumption
+ ]
+ ]
+qed.
+
+theorem lt_SO_to_le_exp_B: \forall n. 1 < n \to
+exp 2 (2*n) \le 2 * n * B (2*n).
+intros.
+apply (le_times_to_le (exp (fact n) (S(S O))))
+ [apply lt_O_exp.
+ apply lt_O_fact
+ |rewrite < assoc_times in ⊢ (? ? %).
+ rewrite > sym_times in ⊢ (? ? (? % ?)).
+ rewrite > assoc_times in ⊢ (? ? %).
+ rewrite < eq_fact_B
+ [rewrite < sym_times.
+ apply fact3.
+ apply lt_to_le.assumption
+ |assumption
+ ]
+ ]
+qed.
+
+theorem le_exp_B: \forall n. O < n \to
+exp 2 (2*n) \le 2 * n * B (2*n).
+intros.
+elim H
+ [apply le_n
+ |apply lt_SO_to_le_exp_B.
+ apply le_S_S.assumption
+ ]
+qed.
+
theorem eq_A_SSO_n: \forall n.O < n \to
-A((S(S O))*n) =
- pi_p (S ((S(S O))*n)) primeb
- (\lambda p.(pi_p (log p ((S(S O))*n) )
+A(2*n) =
+ pi_p (S (2*n)) primeb
+ (\lambda p.(pi_p (log p (2*n) )
(\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
*A n.
intro.
[apply prime_to_lt_SO.
apply primeb_true_to_prime.
assumption
- |assumption
|simplify.
apply le_plus_n_r
]
qed.
theorem le_A_BA1: \forall n. O < n \to
-A((S(S O))*n) \le B((S(S O))*n)*A n.
+A(2*n) \le B(2*n)*A n.
intros.
rewrite > eq_A_SSO_n
[apply le_times_l.
assumption
|cut (i\sup(S i1)≤(S(S O))*n)
[apply div_mod_spec_intro
- [alias id "lt_plus_to_lt_minus" = "cic:/matita/nat/map_iter_p.ma/lt_plus_to_lt_minus.con".
- apply lt_plus_to_lt_minus
+ [apply lt_plus_to_lt_minus
[assumption
|simplify in ⊢ (? % ?).
rewrite < plus_n_O.
qed.
theorem le_A_exp: \forall n.
-A((S(S O))*n) \le (exp (S(S O)) ((S(S O)*n)))*A n.
+A(2*n) \le (exp 2 (pred (2*n)))*A n.
intro.
-apply (trans_le ? (B((S(S O))*n)*A n))
+apply (trans_le ? (B(2*n)*A n))
[apply le_A_BA
|apply le_times_l.
apply le_B_exp
]
qed.
-(* da spostare *)
-theorem times_exp: \forall n,m,p.exp n p * exp m p = exp (n*m) p.
-intros.elim p
- [reflexivity
- |simplify.autobatch
+theorem lt_SSSSO_to_le_A_exp: \forall n. 4 < n \to
+A(2*n) \le exp 2 ((2*n)-2)*A n.
+intros.
+apply (trans_le ? (B(2*n)*A n))
+ [apply le_A_BA
+ |apply le_times_l.
+ apply lt_SSSSO_to_le_B_exp.assumption
]
qed.
-theorem le_exp_log: \forall p,n. O < n \to
-exp p (
-log n) \le n.
-intros.
-apply leb_true_to_le.
-unfold log.
-apply (f_max_true (\lambda x.leb (exp p x) n)).
-apply (ex_intro ? ? O).
-split
- [apply le_O_n
- |apply le_to_leb_true.simplify.assumption
+theorem times_SSO_pred: \forall n. 2*(pred n) \le pred (2*n).
+intro.cases n
+ [apply le_n
+ |simplify.apply le_plus_r.
+ apply le_n_Sn
]
qed.
-theorem lt_log_n_n: \forall n. O < n \to log n < n.
+theorem le_S_times_SSO: \forall n. O < n \to S n \le 2*n.
intros.
-cut (log n \le n)
- [elim (le_to_or_lt_eq ? ? Hcut)
+elim H
+ [apply le_n
+ |rewrite > times_SSO.
+ apply le_S_S.
+ apply (trans_le ? (2*n1))
[assumption
- |absurd (exp (S(S O)) n \le n)
- [rewrite < H1 in ⊢ (? (? ? %) ?).
- apply le_exp_log.
+ |apply le_n_Sn
+ ]
+ ]
+qed.
+
+theorem le_A_exp1: \forall n.
+A(exp 2 n) \le (exp 2 ((2*(exp 2 n)-(S(S n))))).
+intro.elim n
+ [simplify.apply le_n
+ |change in ⊢ (? % ?) with (A(2*(exp 2 n1))).
+ apply (trans_le ? ((exp 2 (pred(2*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
+ [apply le_A_exp
+ |apply (trans_le ? ((2)\sup(pred (2*(2)\sup(n1)))*(2)\sup(2*(2)\sup(n1)-S (S n1))))
+ [apply le_times_r.
assumption
- |apply lt_to_not_le.
- apply lt_m_exp_nm.
- apply le_n
+ |rewrite < exp_plus_times.
+ apply le_exp
+ [apply lt_O_S
+ |cut (S(S n1) \le 2*(exp 2 n1))
+ [apply le_S_S_to_le.
+ change in ⊢ (? % ?) with (S(pred (2*(2)\sup(n1)))+(2*(2)\sup(n1)-S (S n1))).
+ rewrite < S_pred
+ [rewrite > eq_minus_S_pred in ⊢ (? ? %).
+ rewrite < S_pred
+ [rewrite < eq_minus_plus_plus_minus
+ [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?).
+ apply le_n
+ |assumption
+ ]
+ |apply lt_to_lt_O_minus.
+ apply (lt_to_le_to_lt ? (2*(S(S n1))))
+ [rewrite > times_n_SO in ⊢ (? % ?).
+ rewrite > sym_times.
+ apply lt_times_l1
+ [apply lt_O_S
+ |apply le_n
+ ]
+ |apply le_times_r.
+ assumption
+ ]
+ ]
+ |unfold.rewrite > times_n_SO in ⊢ (? % ?).
+ apply le_times
+ [apply le_n_Sn
+ |apply lt_O_exp.
+ apply lt_O_S
+ ]
+ ]
+ |elim n1
+ [apply le_n
+ |apply (trans_le ? (2*(S(S n2))))
+ [apply le_S_times_SSO.
+ apply lt_O_S
+ |apply le_times_r.
+ assumption
+ ]
+ ]
+ ]
+ ]
]
]
- |unfold log.apply le_max_n
]
qed.
-theorem le_log_n_n: \forall n. log n \le n.
-intro.
-cases n
+theorem monotonic_A: monotonic nat le A.
+unfold.intros.
+elim H
[apply le_n
- |apply lt_to_le.
- apply lt_log_n_n.
- apply lt_O_S
+ |apply (trans_le ? (A n1))
+ [assumption
+ |unfold A.
+ cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1))
+ ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1))))
+ [apply (bool_elim ? (primeb (S n1)));intro
+ [rewrite > (true_to_pi_p_Sn ? ? ? H3).
+ rewrite > times_n_SO in ⊢ (? % ?).
+ rewrite > sym_times.
+ apply le_times
+ [apply lt_O_exp.apply lt_O_S
+ |assumption
+ ]
+ |rewrite > (false_to_pi_p_Sn ? ? ? H3).
+ assumption
+ ]
+ |apply le_pi_p.intros.
+ apply le_exp
+ [apply prime_to_lt_O.
+ apply primeb_true_to_prime.
+ assumption
+ |apply le_log
+ [apply prime_to_lt_SO.
+ apply primeb_true_to_prime.
+ assumption
+ |apply le_S.apply le_n
+ ]
+ ]
+ ]
+ ]
]
qed.
-theorem lt_exp_log: \forall n. n < exp (S(S O)) (S (log n)).
-intro.cases n
- [simplify.apply le_S.apply le_n
- |apply not_le_to_lt.
- apply leb_false_to_not_le.
- apply (lt_max_to_false ? (S n1) (S (log (S n1))))
- [apply le_S_S.apply le_n
- |apply lt_log_n_n.apply lt_O_S
+(*
+theorem le_A_exp2: \forall n. O < n \to
+A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
+intros.
+apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
+ [apply monotonic_A.
+ apply lt_to_le.
+ apply lt_exp_log.
+ apply le_n
+ |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
+ [apply le_A_exp1
+ |apply le_exp
+ [apply lt_O_S
+ |rewrite > assoc_times.apply le_times_r.
+ change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
+ apply le_times_r.
+ apply le_exp_log.
+ assumption
+ ]
]
]
qed.
+*)
-theorem f_false_to_le_max: \forall f,n,p. (∃i:nat.i≤n∧f i=true) \to
-(\forall m. p < m \to f m = false)
-\to max n f \le p.
-intros.
-apply not_lt_to_le.intro.
-apply not_eq_true_false.
-rewrite < (H1 ? H2).
-apply sym_eq.
-apply f_max_true.
-assumption.
+(* example *)
+theorem A_SO: A (S O) = S O.
+reflexivity.
+qed.
+
+theorem A_SSO: A (S(S O)) = S (S O).
+reflexivity.
+qed.
+
+theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
+reflexivity.
+qed.
+
+theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
+reflexivity.
qed.
-theorem log_times1: \forall n,m. O < n \to O < m \to
-log (n*m) \le S(log n+log m).
+(*
+(* a better result *)
+theorem le_A_exp3: \forall n. S O < n \to
+A(n) \le exp (pred n) (2*(exp 2 (2 * n)).
+intro.
+apply (nat_elim1 n).
intros.
-unfold in ⊢ (? (% ?) ?).
-apply f_false_to_le_max
- [apply (ex_intro ? ? O).
- split
- [apply le_O_n
- |apply le_to_leb_true.
+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))*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))*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.
+ apply le_n
+ ]
+ |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.
- rewrite > times_n_SO.
- apply le_times;assumption
+ 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
+ ]
]
- |intros.
- apply lt_to_leb_false.
- apply (lt_to_le_to_lt ? ((exp (S(S O)) (S(log n)))*(exp (S(S O)) (S(log m)))))
- [apply lt_times;apply lt_exp_log
- |rewrite < exp_plus_times.
- apply le_exp
- [apply lt_O_S
- |simplify.
- rewrite < plus_n_Sm.
- assumption
+ |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))*(S a)))))
+ [apply le_times_r.
+ apply H
+ [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
+ ]
+ |rewrite > sym_times.
+ rewrite > assoc_times.
+ rewrite < exp_plus_times.
+ apply (trans_le ?
+ (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
+ [rewrite > assoc_times.
+ apply le_times_r.
+ rewrite < exp_plus_times.
+ apply le_exp
+ [apply lt_O_S
+ |rewrite > times_SSO.
+ rewrite < H3.
+ simplify.
+ rewrite < plus_n_Sm.
+ rewrite < plus_n_O.
+ apply le_n
+ ]
+ |apply le_times_l.
+ rewrite > times_exp.
+ apply monotonic_exp1.
+ rewrite > H3.
+ rewrite > sym_times.
+ apply le_n
+ ]
+ ]
+ ]
]
+ |rewrite < H4 in H3.simplify in H3.
+ apply False_ind.
+ apply (lt_to_not_le ? ? H1).
+ rewrite > H3.
+ apply le_
]
]
qed.
-
-theorem log_times: \forall n,m.log (n*m) \le S(log n+log m).
+*)
+
+theorem le_A_exp4: \forall n. S O < n \to
+A(n) \le (pred n)*exp 2 ((2 * n) -3).
+intro.
+apply (nat_elim1 n).
intros.
-cases n
- [apply le_O_n
- |cases m
- [rewrite < times_n_O.
- apply le_O_n
- |apply log_times1;apply lt_O_S
+elim (or_eq_eq_S m).
+elim H2
+ [elim (le_to_or_lt_eq (S O) a)
+ [rewrite > H3 in ⊢ (? % ?).
+ apply (trans_le ? (exp 2 (pred(2*a))*A a))
+ [apply le_A_exp
+ |apply (trans_le ? (2\sup(pred(2*a))*((pred a)*2\sup((2*a)-3))))
+ [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 < H3.
+ rewrite < assoc_times.
+ rewrite > sym_times in ⊢ (? (? % ?) ?).
+ rewrite > assoc_times.
+ apply le_times
+ [rewrite > H3.
+ elim a[apply le_n|simplify.apply le_plus_n_r]
+ |rewrite < exp_plus_times.
+ apply le_exp
+ [apply lt_O_S
+ |apply (trans_le ? (m+(m-3)))
+ [apply le_plus_l.
+ cases m[apply le_n|apply le_n_Sn]
+ |simplify.rewrite < plus_n_O.
+ rewrite > eq_minus_plus_plus_minus
+ [apply le_n
+ |rewrite > H3.
+ apply (trans_le ? (2*2))
+ [simplify.apply (le_n_Sn 3)
+ |apply le_times_r.assumption
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ |rewrite > H3.rewrite < H4.simplify.
+ apply le_S_S.apply lt_O_S
+ |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 2 (pred(2*(S a))))*A (S a)))
+ [apply le_A_exp
+ |apply (trans_le ? ((2\sup(pred (2*S a)))*(a*(exp 2 ((2*(S a))-3)))))
+ [apply le_times_r.
+ apply H
+ [rewrite > H3.
+ apply le_S_S.
+ apply le_S_times_SSO.
+ assumption
+ |apply le_S_S.assumption
+ ]
+ |rewrite > H3.
+ change in ⊢ (? ? (? % ?)) with (2*a).
+ rewrite > times_SSO.
+ change in ⊢ (? (? (? ? %) ?) ?) with (S(2*a)).
+ rewrite > minus_Sn_m
+ [change in ⊢ (? (? ? (? ? %)) ?) with (2*(exp 2 (S(2*a)-3))).
+ rewrite < assoc_times in ⊢ (? (? ? %) ?).
+ rewrite < assoc_times.
+ rewrite > sym_times in ⊢ (? (? % ?) ?).
+ rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
+ rewrite > assoc_times.
+ apply le_times_r.
+ rewrite < exp_plus_times.
+ apply le_exp
+ [apply lt_O_S
+ |rewrite < eq_minus_plus_plus_minus
+ [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?).
+ apply le_n
+ |apply le_S_S.
+ apply O_lt_const_to_le_times_const.
+ assumption
+ ]
+ ]
+ |apply le_S_S.
+ apply O_lt_const_to_le_times_const.
+ assumption
+ ]
+ ]
+ ]
+ ]
+ |rewrite < H4 in H3.simplify in H3.
+ apply False_ind.
+ apply (lt_to_not_le ? ? H1).
+ rewrite > H3.
+ apply le_n
]
]
qed.
-theorem log_exp: \forall n,m.O < m \to
-log ((exp (S(S O)) n)*m)=n+log m.
+theorem le_n_SSSSSSSSO_to_le_A_exp:
+\forall n. n \le 8 \to A(n) \le exp 2 ((2 * n) -3).
+intro.cases n
+ [intro.apply le_n
+ |cases n1
+ [intro.apply le_n
+ |cases n2
+ [intro.apply le_n
+ |cases n3
+ [intro.apply leb_true_to_le.reflexivity
+ |cases n4
+ [intro.apply leb_true_to_le.reflexivity
+ |cases n5
+ [intro.apply leb_true_to_le.reflexivity
+ |cases n6
+ [intro.apply leb_true_to_le.reflexivity
+ |cases n7
+ [intro.apply leb_true_to_le.reflexivity
+ |cases n8
+ [intro.apply leb_true_to_le.reflexivity
+ |intro.apply False_ind.
+ apply (lt_to_not_le ? ? H).
+ apply leb_true_to_le.reflexivity
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+qed.
+
+theorem le_A_exp5: \forall n. A(n) \le exp 2 ((2 * n) -3).
+intro.
+apply (nat_elim1 n).
intros.
-unfold log in ⊢ (? ? (% ?) ?).
-apply max_spec_to_max.
-unfold max_spec.
-split
- [split
- [elim n
- [simplify.
- rewrite < plus_n_O.
- apply le_log_n_n
- |simplify.
- rewrite < plus_n_O.
- rewrite > times_plus_l.
- apply (trans_le ? (S((S(S O))\sup(n1)*m)))
- [apply le_S_S.assumption
- |apply (lt_O_n_elim ((S(S O))\sup(n1)*m))
- [rewrite > (times_n_O O) in ⊢ (? % ?).
- apply lt_times
- [apply lt_O_exp.
- apply lt_O_S
- |assumption
+elim (decidable_le 9 m)
+ [elim (or_eq_eq_S m).
+ elim H2
+ [rewrite > H3 in ⊢ (? % ?).
+ apply (trans_le ? (exp 2 (pred(2*a))*A a))
+ [apply le_A_exp
+ |apply (trans_le ? (2\sup(pred(2*a))*(2\sup((2*a)-3))))
+ [apply le_times_r.
+ apply H.
+ rewrite > H3.
+ apply lt_m_nm
+ [apply (trans_lt ? 4)
+ [apply lt_O_S
+ |apply (lt_times_to_lt 2)
+ [apply lt_O_S
+ |rewrite < H3.assumption
+ ]
+ ]
+ |apply le_n
+ ]
+ |rewrite < H3.
+ rewrite < exp_plus_times.
+ apply le_exp
+ [apply lt_O_S
+ |simplify.rewrite < plus_n_O.
+ rewrite > eq_minus_plus_plus_minus
+ [apply le_plus_l.
+ apply le_pred_n
+ |apply (trans_le ? 9)
+ [apply leb_true_to_le. reflexivity
+ |assumption
+ ]
+ ]
+ ]
+ ]
+ ]
+ |apply (trans_le ? (A (2*(S a))))
+ [apply monotonic_A.
+ rewrite > H3.
+ rewrite > times_SSO.
+ apply le_n_Sn
+ |apply (trans_le ? ((exp 2 ((2*(S a))-2))*A (S a)))
+ [apply lt_SSSSO_to_le_A_exp.
+ apply le_S_S.
+ apply (le_times_to_le 2)
+ [apply le_n_Sn.
+ |apply le_S_S_to_le.rewrite < H3.assumption
+ ]
+ |apply (trans_le ? ((2\sup((2*S a)-2))*(exp 2 ((2*(S a))-3))))
+ [apply le_times_r.
+ apply H.
+ rewrite > H3.
+ apply le_S_S.
+ apply lt_m_nm
+ [apply (lt_to_le_to_lt ? 4)
+ [apply lt_O_S
+ |apply (le_times_to_le 2)
+ [apply lt_O_S
+ |apply le_S_S_to_le.
+ rewrite < H3.assumption
+ ]
+ ]
+ |apply le_n
+ ]
+ |rewrite > times_SSO.
+ rewrite < H3.
+ rewrite < exp_plus_times.
+ apply le_exp
+ [apply lt_O_S
+ |cases m
+ [apply le_n
+ |cases n1
+ [apply le_n
+ |simplify.
+ rewrite < minus_n_O.
+ rewrite < plus_n_O.
+ rewrite < plus_n_Sm.
+ simplify.rewrite < minus_n_O.
+ rewrite < plus_n_Sm.
+ apply le_n
+ ]
+ ]
]
- |intro.simplify.apply le_S_S.
- apply le_plus_n
]
]
]
- |simplify.
- apply le_to_leb_true.
- rewrite > exp_plus_times.
- apply le_times_r.
- apply le_exp_log.
- assumption
]
- |intros.
- simplify.
- apply lt_to_leb_false.
- apply (lt_to_le_to_lt ? ((exp (S(S O)) n)*(exp (S(S O)) (S(log m)))))
- [apply lt_times_r1
- [apply lt_O_exp.apply lt_O_S
- |apply lt_exp_log.
+ |apply le_n_SSSSSSSSO_to_le_A_exp.
+ apply le_S_S_to_le.
+ apply not_le_to_lt.
+ assumption
+ ]
+qed.
+
+theorem le_exp_Al:\forall n. O < n \to exp 2 n \le A (2 * n).
+intros.
+apply (trans_le ? ((exp 2 (2*n))/(2*n)))
+ [apply le_times_to_le_div
+ [rewrite > (times_n_O O) in ⊢ (? % ?).
+ apply lt_times
+ [apply lt_O_S
+ |assumption
]
- |rewrite < exp_plus_times.
- apply le_exp
+ |simplify in ⊢ (? ? (? ? %)).
+ rewrite < plus_n_O.
+ rewrite > exp_plus_times.
+ apply le_times_l.
+ apply le_times_SSO_n_exp_SSO_n
+ ]
+ |apply le_times_to_le_div2
+ [rewrite > (times_n_O O) in ⊢ (? % ?).
+ apply lt_times
[apply lt_O_S
- |rewrite < plus_n_Sm.
+ |assumption
+ ]
+ |apply (trans_le ? ((B (2*n)*(2*n))))
+ [rewrite < sym_times in ⊢ (? ? %).
+ apply le_exp_B.
assumption
+ |apply le_times_l.
+ apply le_B_A
]
]
]
qed.
-theorem log_SSO: \forall n. O < n \to
-log ((S(S O))*n) = S (log n).
+theorem le_exp_A2:\forall n. 1 < n \to exp 2 (n / 2) \le A n.
intros.
-change with (log ((exp (S(S O)) (S O))*n)=S (log n)).
-rewrite > log_exp.reflexivity.assumption.
-qed.
-
-theorem or_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.apply times_n_O
- |elim H.elim H1
- [apply (ex_intro ? ? a).right.apply eq_f.assumption
- |apply (ex_intro ? ? (S a)).left.
- rewrite > H2.simplify.
- rewrite < plus_n_O.
- rewrite < plus_n_Sm.
- reflexivity
+apply (trans_le ? (A(n/2*2)))
+ [rewrite > sym_times.
+ apply le_exp_Al.
+ elim (le_to_or_lt_eq ? ? (le_O_n (n/2)))
+ [assumption
+ |apply False_ind.
+ apply (lt_to_not_le ? ? H).
+ rewrite > (div_mod n 2)
+ [rewrite < H1.
+ change in ⊢ (? % ?) with (n\mod 2).
+ apply le_S_S_to_le.
+ apply lt_mod_m_m.
+ apply lt_O_S
+ |apply lt_O_S
+ ]
]
+ |apply monotonic_A.
+ rewrite > (div_mod n 2) in ⊢ (? ? %).
+ apply le_plus_n_r.
+ apply lt_O_S
]
qed.
-theorem lt_O_to_or_eq_S: \forall n.O < n \to \exists m.m < n \land
-((n = (S(S O))*m) \lor (n = S((S(S O))*m))).
-intros.
-elim (or_eq_S n).
-elim H1
- [apply (ex_intro ? ? a).split
- [rewrite > H2.
- rewrite > times_n_SO in ⊢ (? % ?).
- rewrite > sym_times.
- apply lt_times_l1
- [apply (divides_to_lt_O a n ? ?)
- [assumption
- |apply (witness a n (S (S O))).
- rewrite > sym_times.
- assumption
- ]
- |apply le_n
- ]
- |left.assumption
- ]
- |apply (ex_intro ? ? a).split
- [rewrite > H2.
- apply (le_to_lt_to_lt ? ((S(S O))*a))
- [rewrite > times_n_SO in ⊢ (? % ?).
- rewrite > sym_times.
- apply le_times_l.
- apply le_n_Sn
- |apply le_n
- ]
- |right.assumption
+theorem eq_sigma_pi_SO_n: \forall n.
+sigma_p n (\lambda i.true) (\lambda i.S O) = n.
+intro.elim n
+ [reflexivity
+ |rewrite > true_to_sigma_p_Sn
+ [rewrite > H.reflexivity
+ |reflexivity
]
]
qed.
-theorem factS: \forall n. fact (S n) = (S n)*(fact n).
-intro.simplify.reflexivity.
+theorem leA_prim: \forall n.
+exp n (prim n) \le A n * pi_p (S n) primeb (λp:nat.p).
+intro.
+unfold prim.
+rewrite < (exp_sigma_p (S n) n primeb).
+unfold A.
+rewrite < times_pi_p.
+apply le_pi_p.
+intros.
+rewrite > sym_times.
+change in ⊢ (? ? %) with (exp i (S (log i n))).
+apply lt_to_le.
+apply lt_exp_log.
+apply prime_to_lt_SO.
+apply primeb_true_to_prime.
+assumption.
qed.
-theorem exp_S: \forall n,m. exp m (S n) = m*exp m n.
-intros.reflexivity.
+
+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.
-lemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
-intro.simplify.rewrite < plus_n_Sm.reflexivity.
+
+(* the inequalities *)
+theorem le_exp_priml: \forall n. O < n \to
+exp 2 (2*n) \le exp (2*n) (S(prim (2*n))).
+intros.
+apply (trans_le ? (((2*n*(B (2*n))))))
+ [apply le_exp_B.assumption
+ |change in ⊢ (? ? %) with (((2*n))*((2*n))\sup (prim (2*n))).
+ apply le_times_r.
+ apply (trans_le ? (A (2*n)))
+ [apply le_B_A
+ |apply le_Al
+ ]
+ ]
qed.
-theorem fact1: \forall n.
-fact ((S(S O))*n) \le (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n).
-intro.elim n
- [rewrite < times_n_O.apply le_n
- |rewrite > times_SSO.
- rewrite > factS.
- rewrite > factS.
+theorem le_exp_prim4l: \forall n. O < n \to
+exp 2 (S(4*n)) \le exp (4*n) (S(prim (4*n))).
+intros.
+apply (trans_le ? (2*(4*n*(B (4*n)))))
+ [change in ⊢ (? % ?) with (2*(exp 2 (4*n))).
+ apply le_times_r.
+ cut (4*n = 2*(2*n))
+ [rewrite > Hcut.
+ apply le_exp_B.
+ apply lt_to_le.unfold.
+ rewrite > times_n_SO in ⊢ (? % ?).
+ apply le_times_r.assumption
+ |rewrite < assoc_times.
+ reflexivity
+ ]
+ |change in ⊢ (? ? %) with ((4*n)*(4*n)\sup (prim (4*n))).
rewrite < assoc_times.
- rewrite > factS.
- apply (trans_le ? (((S(S O))*(S n1))*((S(S O))*(S n1))*(fact (((S(S O))*n1)))))
- [apply le_times_l.
- rewrite > times_SSO.
- apply le_times_r.
- apply le_n_Sn
- |rewrite > assoc_times.
- rewrite > assoc_times.
- rewrite > assoc_times in ⊢ (? ? %).
- rewrite > exp_S.
- rewrite > assoc_times in ⊢ (? ? %).
- apply le_times_r.
- rewrite < assoc_times.
- rewrite < assoc_times.
- rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?).
- rewrite > assoc_times.
- rewrite > assoc_times.
- rewrite > exp_S.
- rewrite > assoc_times in ⊢ (? ? %).
- apply le_times_r.
- rewrite > sym_times in ⊢ (? ? %).
- rewrite > assoc_times in ⊢ (? ? %).
- rewrite > assoc_times in ⊢ (? ? %).
- apply le_times_r.
- rewrite < assoc_times in ⊢ (? ? %).
- rewrite < assoc_times in ⊢ (? ? %).
- rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
- rewrite > assoc_times in ⊢ (? ? %).
- rewrite > assoc_times in ⊢ (? ? %).
- apply le_times_r.
- rewrite > sym_times in ⊢ (? ? (? ? %)).
- rewrite > sym_times in ⊢ (? ? %).
- assumption
+ rewrite > sym_times in ⊢ (? (? % ?) ?).
+ rewrite > assoc_times.
+ apply le_times_r.
+ apply (trans_le ? (A (4*n)))
+ [apply le_B_A4.assumption
+ |apply le_Al
]
]
qed.
-theorem monotonic_log: monotonic nat le log.
-unfold monotonic.intros.
-elim (le_to_or_lt_eq ? ? H) 0
- [cases x;intro
- [apply le_O_n
- |apply lt_S_to_le.
- apply (lt_exp_to_lt (S(S O)))
+theorem le_priml: \forall n. O < n \to
+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)))))))
+ [apply le_log
[apply le_n
- |apply (le_to_lt_to_lt ? (S n))
- [apply le_exp_log.
- apply lt_O_S
- |apply (trans_lt ? y)
- [assumption
- |apply lt_exp_log
- ]
- ]
+ |apply le_exp_priml.assumption
]
+ |rewrite > sym_times in ⊢ (? ? %).
+ apply log_exp1.
+ apply le_n
]
- |intro.rewrite < H1.apply le_n
+ |apply le_n
]
qed.
-theorem lt_O_fact: \forall n. O < fact n.
-intro.elim n
- [simplify.apply lt_O_S
- |rewrite > factS.
- rewrite > (times_n_O O).
- apply lt_times
- [apply lt_O_S
- |assumption
- ]
+theorem le_exp_primr: \forall n.
+exp n (prim n) \le exp 2 (2*(2*n-3)).
+intros.
+apply (trans_le ? (exp (A n) 2))
+ [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))).
+ rewrite < times_n_SO.
+ apply leA_r2
+ |rewrite > sym_times.
+ rewrite < exp_exp_times.
+ apply monotonic_exp1.
+ apply le_A_exp5
]
qed.
-theorem fact2: \forall n.O < n \to
-(exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n) < fact (S((S(S O))*n)).
-intros.elim H
- [simplify.apply le_S.apply le_n
- |rewrite > times_SSO.
- rewrite > factS.
- rewrite > factS.
- rewrite < assoc_times.
- rewrite > factS.
- rewrite < times_SSO in ⊢ (? ? %).
- apply (trans_lt ? (((S(S O))*S n1)*((S(S O))*S n1*(S ((S(S O))*n1))!)))
- [rewrite > assoc_times in ⊢ (? ? %).
- rewrite > exp_S.
- rewrite > assoc_times.
- rewrite > assoc_times.
- rewrite > assoc_times.
- apply lt_times_r.
- rewrite > exp_S.
- rewrite > assoc_times.
- rewrite > sym_times in ⊢ (? ? %).
- rewrite > assoc_times in ⊢ (? ? %).
- rewrite > assoc_times in ⊢ (? ? %).
- apply lt_times_r.
- rewrite > sym_times.
- rewrite > assoc_times.
- rewrite > assoc_times.
- apply lt_times_r.
- rewrite < assoc_times.
- rewrite < assoc_times.
- rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
- rewrite > assoc_times.
- rewrite > assoc_times.
- rewrite > sym_times in ⊢ (? ? %).
- apply lt_times_r.
- rewrite < assoc_times.
- rewrite < sym_times.
- rewrite < assoc_times.
- assumption
- |apply lt_times_l1
- [rewrite > (times_n_O O) in ⊢ (? % ?).
- apply lt_times
- [rewrite > (times_n_O O) in ⊢ (? % ?).
- apply lt_times
- [apply lt_O_S
- |apply lt_O_S
- ]
- |apply lt_O_fact
+(* 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 lt_O_log: \forall n. S O < n \to O < log n.
-intros.elim H
- [simplify.apply lt_O_S
- |apply (lt_to_le_to_lt ? (log n1))
- [assumption
- |apply monotonic_log.
- apply le_n_Sn
+
+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 log_fact_SSSO: log (fact (S(S(S O)))) = S (S O).
-reflexivity.
-qed.
-
-lemma exp_SSO_SSO: exp (S(S O)) (S(S O)) = S(S(S(S O))).
-reflexivity.
-qed.
(*
-theorem log_fact_SSSSO: log (fact (S(S(S(S O))))) = S(S(S(S O))).
-reflexivity.
-qed.
-*)
-theorem log_fact_SSSSSO: log (fact (S(S(S(S(S O)))))) = S(S(S(S O))).
-reflexivity.
-qed.
-
-theorem bof_bof: \forall n.(S(S(S(S O)))) < n \to
-n \le (S(S(S(S(S(S(S(S O)))))))) \to log (fact n) < n*log n - n.
+theorem prim_SSSSSSO: \forall n.30\le n \to O < prim (8*n) - prim n.
intros.
-elim H
- [rewrite > factS in ⊢ (? (? %) ?).
- rewrite > factS in ⊢ (? (? (? ? %)) ?).
- rewrite < assoc_times in ⊢ (? (? %) ?).
- rewrite < sym_times in ⊢ (? (? (? % ?)) ?).
- rewrite > assoc_times in ⊢ (? (? %) ?).
- change with (exp (S(S O)) (S(S O))) in ⊢ (? (? (? % ?)) ?).
-
-theorem bof: \forall n.(S(S(S(S O))))) < n \to log (fact n) < n*log n - n.
-intro.apply (nat_elim1 n).
-intros.
-elim (lt_O_to_or_eq_S m)
- [elim H2.clear H2.
- elim H4.clear H4.
- rewrite > H2.
- apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
- [apply monotonic_log.
- apply fact1
- |rewrite > assoc_times in ⊢ (? (? %) ?).
- rewrite > log_exp.
- apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
- [apply le_plus_r.
- apply log_times
- |rewrite > plus_n_Sm.
- rewrite > log_SSO.
- rewrite < times_n_Sm.
- apply (le_to_lt_to_lt ? ((S(S O))*a+(log a!+(a*log a-a))))
- [apply le_plus_r.
- apply le_plus_r.
- apply H.assumption
- |apply (lt_to_le_to_lt ? ((S(S O))*a+((a*log a-a)+(a*log a-a))))
- [apply lt_plus_r.
- apply lt_plus_l.
- apply H.
- assumption.
- |rewrite > times_SSO_n.
- rewrite > distr_times_minus.
- rewrite > sym_plus.
- rewrite > plus_minus
- [rewrite > sym_plus.
- rewrite < assoc_times.
- apply le_n
- |rewrite < assoc_times.
- rewrite > times_n_SO in ⊢ (? % ?).
- apply le_times
- [apply le_n
- |apply lt_O_log.
- apply (lt_times_n_to_lt_r (S(S O)))
- [apply lt_O_S
- |rewrite < times_n_SO.
- rewrite < H2.
- assumption
- ]
- ]
- ]
- ]
-
- .
- ]
- |
- rewrite < eq_plus_minus_minus_plus.
-
- rewrite > assoc_plus.
- apply lt_plus_r.
- rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
- change with
- (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
- apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
- [apply le_S_S.
- apply lt_plus_r.
- apply lt_times_r.
- apply H.
- assumption
- |
-
-theorem stirling: \forall n,k.k \le n \to
-log (fact n) < n*log n - n + k*log n.
-intro.
-apply (nat_elim1 n).
-intros.
-elim (lt_O_to_or_eq_S m)
- [elim H2.clear H2.
- elim H4.clear H4.
- rewrite > H2.
- apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
- [apply monotonic_log.
- apply fact1
- |rewrite > assoc_times in ⊢ (? (? %) ?).
- rewrite > log_exp.
- apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
- [apply le_plus_r.
- apply log_times
- |rewrite < plus_n_Sm.
- rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
- change with
- (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
- apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
- [apply le_S_S.
- apply lt_plus_r.
- apply lt_times_r.
- apply H.
- assumption
- |
-
- [
-
- a*log a-a+k*log a
-
-*)
\ No newline at end of file
+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