From fe40d64367a3105b09696557c256f5a78d4b7384 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 7 Feb 2008 12:02:01 +0000 Subject: [PATCH] Results about Chebyshev teta function. --- .../matita/library/nat/chebyshev_teta.ma | 104 ++++++++++++++++++ 1 file changed, 104 insertions(+) create mode 100644 helm/software/matita/library/nat/chebyshev_teta.ma diff --git a/helm/software/matita/library/nat/chebyshev_teta.ma b/helm/software/matita/library/nat/chebyshev_teta.ma new file mode 100644 index 000000000..bb0f4e838 --- /dev/null +++ b/helm/software/matita/library/nat/chebyshev_teta.ma @@ -0,0 +1,104 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/chebyshev_teta". + +include "nat/binomial.ma". +include "nat/pi_p.ma". + +(* This is chebishev teta function *) + +definition teta: nat \to nat \def +\lambda n. pi_p (S n) primeb (\lambda p.p). + +definition M \def \lambda m.bc (2*m+1) m. + +theorem lt_M: \forall m. O < m \to M m < exp 2 (2*m). +intros. +apply (lt_times_to_lt 2) + [apply lt_O_S + |change in ⊢ (? ? %) with (exp 2 (S(2*m))). + change in ⊢ (? ? (? % ?)) with (1+1). + rewrite > exp_plus_sigma_p. + apply (le_to_lt_to_lt ? (sigma_p (S (S (2*m))) (λk:nat.orb (eqb k m) (eqb k (S m))) + (λk:nat.bc (S (2*m)) k*(1)\sup(S (2*m)-k)*(1)\sup(k)))) + [rewrite > (sigma_p_gi ? ? m) + [rewrite > (sigma_p_gi ? ? (S m)) + [rewrite > (false_to_eq_sigma_p O (S(S(2*m)))) + [simplify in ⊢ (? ? (? ? (? ? %))). + simplify in ⊢ (? % ?). + rewrite < exp_SO_n.rewrite < exp_SO_n. + rewrite < exp_SO_n.rewrite < exp_SO_n. + rewrite < times_n_SO.rewrite < times_n_SO. + rewrite < times_n_SO.rewrite < times_n_SO. + apply le_plus + [unfold M.rewrite < plus_n_SO.apply le_n + |apply le_plus_l.unfold M.rewrite < plus_n_SO. + change in \vdash (? ? %) with (fact (S(2*m))/(fact (S m)*(fact ((2*m)-m)))). + simplify in \vdash (? ? (? ? (? ? (? (? % ?))))). + rewrite < plus_n_O.rewrite < minus_plus_m_m. + rewrite < sym_times in \vdash (? ? (? ? %)). + change in \vdash (? % ?) with (fact (S(2*m))/(fact m*(fact (S(2*m)-m)))). + simplify in \vdash (? (? ? (? ? (? (? (? %) ?)))) ?). + rewrite < plus_n_O.change in \vdash (? (? ? (? ? (? (? % ?)))) ?) with (S m + m). + rewrite < minus_plus_m_m. + apply le_n + ] + |apply le_O_n + |intros. + elim (eqb i m);elim (eqb i (S m));reflexivity + ] + |apply le_S_S.apply le_S_S. + apply le_times_n. + apply le_n_Sn + |rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S m))). + rewrite > (not_eq_to_eqb_false (S m) m) + [reflexivity + |intro.apply (not_eq_n_Sn m). + apply sym_eq.assumption + ] + ] + |apply le_S.apply le_S_S. + apply le_times_n. + apply le_n_Sn + |rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S m))). + reflexivity + ] + |rewrite > (bool_to_nat_to_eq_sigma_p (S(S(2*m))) ? (\lambda k.true) ? + (\lambda k.bool_to_nat (eqb k m\lor eqb k (S m))*(bc (S (2*m)) k*(1)\sup(S (2*m)-k)*(1)\sup(k)))) + in \vdash (? % ?) + [apply lt_sigma_p + [intros.elim (eqb i m\lor eqb i (S m)) + [rewrite > sym_times.rewrite < times_n_SO.apply le_n + |apply le_O_n + ] + |apply (ex_intro ? ? O). + split + [split[apply lt_O_S|reflexivity] + |rewrite > (not_eq_to_eqb_false ? ? (not_eq_O_S m)). + rewrite > (not_eq_to_eqb_false ? ? (lt_to_not_eq ? ? H)). + simplify in \vdash (? % ?). + rewrite < exp_SO_n.rewrite < exp_SO_n. + rewrite > bc_n_O.simplify. + apply le_n + ] + ] + |intros.rewrite > sym_times in \vdash (? ? ? %). + + + + simplify in \vdash (? ? %). + + + -- 2.39.2