Results about Chebyshev teta function.

diff --git a/helm/software/matita/library/nat/chebyshev_teta.ma b/helm/software/matita/library/nat/chebyshev_teta.ma
new file mode 100644 (file)
index 0000000..bb0f4e8
--- /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 (? ? %).
+             
+
+