helm/software/matita/library/nat/chebyshev_teta.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        Matita is distributed under the terms of the          *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/nat/chebyshev_teta".
  16
  17 include "nat/binomial.ma".
  18 include "nat/pi_p.ma".
  19
  20 (* This is chebishev teta function *)
  21
  22 definition teta: nat \to nat \def
  23 \lambda n. pi_p (S n) primeb (\lambda p.p).
  24
  25 definition M \def \lambda m.bc (2*m+1) m.
  26
  27 theorem lt_M: \forall m. O < m \to M m < exp 2 (2*m).
  28 intros.
  29 apply (lt_times_to_lt 2)
  30   [apply lt_O_S
  31   |change in ⊢ (? ? %) with (exp 2 (S(2*m))).
  32    change in ⊢ (? ? (? % ?)) with (1+1).
  33    rewrite > exp_plus_sigma_p.
  34    apply (le_to_lt_to_lt ? (sigma_p (S (S (2*m))) (λk:nat.orb (eqb k m) (eqb k (S m)))
  35             (λk:nat.bc (S (2*m)) k*(1)\sup(S (2*m)-k)*(1)\sup(k))))
  36     [rewrite > (sigma_p_gi ? ? m)
  37       [rewrite > (sigma_p_gi ? ? (S m))
  38         [rewrite > (false_to_eq_sigma_p O (S(S(2*m))))
  39           [simplify in ⊢ (? ? (? ? (? ? %))).
  40            simplify in ⊢ (? % ?).
  41            rewrite < exp_SO_n.rewrite < exp_SO_n.
  42            rewrite < exp_SO_n.rewrite < exp_SO_n.
  43            rewrite < times_n_SO.rewrite < times_n_SO.
  44            rewrite < times_n_SO.rewrite < times_n_SO.
  45            apply le_plus
  46             [unfold M.rewrite < plus_n_SO.apply le_n
  47             |apply le_plus_l.unfold M.rewrite < plus_n_SO.
  48              change in \vdash (? ? %) with (fact (S(2*m))/(fact (S m)*(fact ((2*m)-m)))).
  49              simplify in \vdash (? ? (? ? (? ? (? (? % ?))))).
  50              rewrite < plus_n_O.rewrite < minus_plus_m_m.
  51              rewrite < sym_times in \vdash (? ? (? ? %)).
  52              change in \vdash (? % ?) with (fact (S(2*m))/(fact m*(fact (S(2*m)-m)))).
  53              simplify in \vdash (? (? ? (? ? (? (? (? %) ?)))) ?).
  54              rewrite < plus_n_O.change in \vdash (? (? ? (? ? (? (? % ?)))) ?) with (S m + m).
  55              rewrite < minus_plus_m_m.
  56              apply le_n
  57             ]
  58           |apply le_O_n
  59           |intros.
  60            elim (eqb i m);elim (eqb i (S m));reflexivity
  61           ]
  62         |apply le_S_S.apply le_S_S.
  63          apply le_times_n.
  64          apply le_n_Sn
  65         |rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S m))).
  66          rewrite > (not_eq_to_eqb_false (S m) m)
  67           [reflexivity
  68           |intro.apply (not_eq_n_Sn m).
  69            apply sym_eq.assumption
  70           ]
  71         ]
  72       |apply le_S.apply le_S_S.
  73        apply le_times_n.
  74        apply le_n_Sn
  75       |rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S m))).
  76        reflexivity
  77       ]
  78     |rewrite > (bool_to_nat_to_eq_sigma_p (S(S(2*m))) ? (\lambda k.true) ?
  79       (\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))))
  80      in \vdash (? % ?)
  81       [apply lt_sigma_p
  82         [intros.elim (eqb i m\lor eqb i (S m))
  83           [rewrite > sym_times.rewrite < times_n_SO.apply le_n
  84           |apply le_O_n
  85           ]
  86         |apply (ex_intro ? ? O).
  87          split
  88           [split[apply lt_O_S|reflexivity]
  89           |rewrite > (not_eq_to_eqb_false ? ? (not_eq_O_S m)).
  90            rewrite > (not_eq_to_eqb_false ? ? (lt_to_not_eq ? ? H)).
  91            simplify in \vdash (? % ?).
  92            rewrite < exp_SO_n.rewrite < exp_SO_n.
  93            rewrite > bc_n_O.simplify.
  94            apply le_n
  95           ]
  96         ]
  97       |intros.rewrite > sym_times in \vdash (? ? ? %).
  98
  99
 100
 101              simplify in \vdash (? ? %).
 102
 103
 104