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
]
qed.
-(* si dovrebbe poter migliorare *)
+(* la prova potrebbe essere migliorata *)
theorem le_prim_n3: \forall n. 15 \le n \to
prim n \le pred (n/2).
intros.
]
]
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
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:?.? ? %) ?))
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)))))
|
*)
-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
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.
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.
-
+
+(* not usefull
theorem le_fact_A:\forall n.S O < n \to
fact (2*n) \le exp (fact n) 2 * A (2*n).
intros.
apply le_B_A
|assumption
]
-qed.
+qed. *)
theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
B (2*n) \le exp 2 (pred (2*n)).
]
qed.
-theorem lt_SO_to_le_exp_B: \forall n. S O < n \to
-exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
+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.
qed.
theorem le_exp_B: \forall n. O < n \to
-exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
+exp 2 (2*n) \le 2 * n * B (2*n).
intros.
elim H
[apply le_n
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.
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.
]
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
+ ]
+ |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
+ |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 le_exp_A2:\forall n. 1 < n \to exp 2 (n / 2) \le A n.
+intros.
+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 eq_sigma_pi_SO_n: \forall n.
sigma_p n (\lambda i.true) (\lambda i.S O) = n.
intro.elim n
(* the inequalities *)
theorem le_exp_priml: \forall n. O < n \to
-exp (S(S O)) ((S(S O))*n) \le exp ((S(S O))*n) (S(prim ((S(S O))*n))).
+exp 2 (2*n) \le exp (2*n) (S(prim (2*n))).
intros.
-apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n))))))
+apply (trans_le ? (((2*n*(B (2*n))))))
[apply le_exp_B.assumption
- |change in ⊢ (? ? %) with ((((S(S O))*n))*(((S(S O))*n))\sup (prim ((S(S O))*n))).
+ |change in ⊢ (? ? %) with (((2*n))*((2*n))\sup (prim (2*n))).
apply le_times_r.
- apply (trans_le ? (A ((S(S O))*n)))
+ apply (trans_le ? (A (2*n)))
[apply le_B_A
|apply le_Al
]