definition prim: nat \to nat \def
\lambda n. sigma_p (S n) primeb (\lambda p.(S O)).
+(* This is chebishev psi funcion *)
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.
-
+
+(* 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.
]
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)
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_exp4: \forall n. S O < n \to
+A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * (pred n))).
+intro.
+apply (nat_elim1 n).
+intros.
+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))*(pred 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))*(pred 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.
+ rewrite < plus_n_O;
+ apply le_S_S_to_le;
+ rewrite > plus_n_Sm in \vdash (? ? %);
+ rewrite < S_pred;
+ [change in \vdash (? % ?) with ((S (pred a + pred a)) + m);
+ apply le_plus_l;
+ apply le_S_S_to_le;
+ rewrite < S_pred;
+ [rewrite > plus_n_Sm;rewrite > sym_plus;
+ rewrite > plus_n_Sm;
+ rewrite > H3;simplify in \vdash (? ? %);
+ rewrite < plus_n_O;rewrite < S_pred;
+ [apply le_n
+ |apply lt_to_le;assumption]
+ |apply lt_to_le;assumption]
+ |apply lt_to_le;assumption]]
+ |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.
+ 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
+ ]
+ ]
+ |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))*a))))
+ [apply le_times_r.
+ apply (trans_le ? ? ? (H (S a) ? ?));
+ [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
+ |simplify in ⊢ (? (? (? % ?) ?) ?);
+ apply le_times_r;apply le_exp;
+ [apply le_S;apply le_n
+ |apply le_times_r;simplify;apply le_n]
+ ]
+ |rewrite > sym_times.
+ rewrite > assoc_times.
+ rewrite < exp_plus_times.
+ rewrite > H3;
+ change in ⊢ (? ? (? (? % ?) ?)) with ((S (S O))*a);
+ rewrite < times_exp;
+ rewrite < sym_times in \vdash (? ? (? % ?));
+ rewrite > assoc_times;
+ apply le_times_r;
+ rewrite < times_n_Sm in ⊢ (? (? ? (? ? %)) ?);
+ rewrite > sym_plus in \vdash (? (? ? %) ?);
+ rewrite > assoc_plus in \vdash (? (? ? %) ?);
+ rewrite > exp_plus_times;apply le_times_r;
+ rewrite < distr_times_plus in ⊢ (? (? ? %) ?);
+ simplify in ⊢ (? ? (? ? (? ? %)));rewrite < plus_n_O;
+ apply le_n
+ ]
+ ]
+ ]
+ |rewrite < H4 in H3.simplify in H3.
+ apply False_ind.
+ apply (lt_to_not_le ? ? H1).
+ rewrite > H3.
+ apply le_n
+ ]
+ ]
+qed.
+
+
theorem eq_sigma_pi_SO_n: \forall n.
sigma_p n (\lambda i.true) (\lambda i.S O) = n.
intro.elim n
assumption.
qed.
+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.
+
(* the inequalities *)
theorem le_exp_priml: \forall n. O < n \to
projects / helm.git / blobdiff