Refactoring

[helm.git] / matita / matita / lib / arithmetics / chebyshev / chebyshev_teta.ma

diff --git a/matita/matita/lib/arithmetics/chebyshev/chebyshev_teta.ma b/matita/matita/lib/arithmetics/chebyshev/chebyshev_teta.ma
index 5bb3a25072ef9020e22906a086f942d78998f167..d2fb6bbd4d9333158a27f95d018bce5a8930de22 100644 (file)
--- a/matita/matita/lib/arithmetics/chebyshev/chebyshev_teta.ma
+++ b/matita/matita/lib/arithmetics/chebyshev/chebyshev_teta.ma
@@ -11,23 +11,23 @@
 
 include "arithmetics/binomial.ma".
 include "arithmetics/gcd.ma".
-include "arithmetics/chebyshev/chebyshev.ma".
+include "arithmetics/chebyshev/chebyshev_psi.ma". 
 
-(* This is chebishev teta function *)
+(* This is chebishev theta function *)
 
-definition teta: nat → nat ≝ λn. 
+definition theta: nat → nat ≝ λn. 
   ∏_{p < S n| primeb p} p.
   
-lemma teta_def: ∀n.teta n = ∏_{p < S n| primeb p} p.
+lemma theta_def: ∀n.theta n = ∏_{p < S n| primeb p} p.
 // qed.
 
-theorem lt_O_teta: ∀n. O < teta n.
+theorem lt_O_theta: ∀n. O < theta n.
 #n elim n
   [@le_n
   |#n1 #Hind cases (true_or_false (primeb (S n1))) #Hc 
-    [>teta_def >bigop_Strue
+    [>theta_def >bigop_Strue
       [>(times_n_O O) @lt_times // | //]
-    |>teta_def >bigop_Sfalse // 
+    |>theta_def >bigop_Sfalse // 
     ]
   ]
 qed.
@@ -129,9 +129,9 @@ theorem divides_pi_p_M:∀m.
 #m  @divides_pi_p_M1 @le_n
 qed.  
 
-theorem teta_pi_p_teta: ∀m. teta (S (2*m))
-= (∏_{p < S (S (2*m)) | leb (S (S m)) p∧primeb p} p)*teta (S m).
-#m >teta_def >teta_def 
+theorem theta_pi_p_theta: ∀m. theta (S (2*m))
+= (∏_{p < S (S (2*m)) | leb (S (S m)) p∧primeb p} p)*theta (S m).
+#m >theta_def >theta_def 
 <(bigop_I ???? timesA)
 >(bigop_sumI 0 (S(S m)) (S(S(2*m))) (λp.primeb p) … timesA (λp.p))
   [2:@le_S_S @le_S_S // |3:@le_O_n]
@@ -139,32 +139,32 @@ theorem teta_pi_p_teta: ∀m. teta (S (2*m))
   [>bigop_I_gen // |@(bigop_I … timesA)]
 qed.
 
-theorem div_teta_teta: ∀m. 
-  teta (S(2*m))/teta (S m) = 
+theorem div_theta_theta: ∀m. 
+  theta (S(2*m))/theta (S m) = 
     ∏_{p < S(S(2*m)) | leb (S(S m)) p ∧ primeb p} p.
 #m @(div_mod_spec_to_eq ????? 0 (div_mod_spec_div_mod …))
-  [@lt_O_teta
-  |@div_mod_spec_intro [@lt_O_teta |<plus_n_O @teta_pi_p_teta]
+  [@lt_O_theta
+  |@div_mod_spec_intro [@lt_O_theta |<plus_n_O @theta_pi_p_theta]
   ]
 qed.
                      
-theorem le_teta_M_teta: ∀m. 
-  teta (S(2*m)) ≤ (M m)*teta (S m).  
-#m >teta_pi_p_teta @le_times [2://] @divides_to_le
+theorem le_theta_M_theta: ∀m. 
+  theta (S(2*m)) ≤ (M m)*theta (S m).  
+#m >theta_pi_p_theta @le_times [2://] @divides_to_le
   [@lt_O_bc @lt_to_le @le_S_S // | @divides_pi_p_M
   ]
 qed.
 
-theorem lt_O_to_le_teta_exp_teta: ∀m. O < m→
-  teta (S(2*m)) < exp 2 (2*m)*teta (S m). 
-#m #posm @(le_to_lt_to_lt ? (M m*teta (S m)))
-  [@le_teta_M_teta
-  |@monotonic_lt_times_l [@lt_O_teta|@lt_M //]
+theorem lt_O_to_le_theta_exp_theta: ∀m. O < m→
+  theta (S(2*m)) < exp 2 (2*m)*theta (S m). 
+#m #posm @(le_to_lt_to_lt ? (M m*theta (S m)))
+  [@le_theta_M_theta
+  |@monotonic_lt_times_l [@lt_O_theta|@lt_M //]
   ]
 qed.
 
-theorem teta_pred: ∀n. 1 < n → teta (2*n) = teta (pred (2*n)).
-#n #lt1n >teta_def >teta_def >bigop_Sfalse
+theorem theta_pred: ∀n. 1 < n → theta (2*n) = theta (pred (2*n)).
+#n #lt1n >theta_def >theta_def >bigop_Sfalse
   [>S_pred
     [//
     |>(times_n_O 2) in ⊢ (?%?); @monotonic_lt_times_r @lt_to_le //
@@ -177,7 +177,7 @@ theorem teta_pred: ∀n. 1 < n → teta (2*n) = teta (pred (2*n)).
   ]
 qed.
   
-theorem le_teta: ∀m.teta m ≤ exp 2 (2*m).
+theorem le_theta: ∀m.theta m ≤ exp 2 (2*m).
 #m @(nat_elim1 m) #m1 #Hind
 cut (∀a. 2 *a = a+a) [//] #times2
 cases (even_or_odd m1) #a * #Ha >Ha
@@ -185,11 +185,11 @@ cases (even_or_odd m1) #a * #Ha >Ha
     [#_ @le_n
     |#n cases n 
       [#_ @leb_true_to_le //
-      |#n1 #Hn1 >teta_pred
+      |#n1 #Hn1 >theta_pred
         [cut (pred (2*S(S n1)) = (S (2*S n1)))
           [normalize >plus_n_Sm in ⊢ (???%); //] #Hcut >Hcut
-         @(transitive_le ? (exp 2 (2*(S n1))*teta (S (S n1))))
-          [@lt_to_le @lt_O_to_le_teta_exp_teta @lt_O_S
+         @(transitive_le ? (exp 2 (2*(S n1))*theta (S (S n1))))
+          [@lt_to_le @lt_O_to_le_theta_exp_theta @lt_O_S
           |>times2 in ⊢ (??%);>exp_plus_times in ⊢ (??%); @le_times
             [@le_exp [@lt_O_S |@monotonic_le_times_r @le_n_Sn]
             |@Hind >Hn1 >times2 //
@@ -201,8 +201,8 @@ cases (even_or_odd m1) #a * #Ha >Ha
     ]
   |lapply Ha cases a
     [#_ @leb_true_to_le // 
-    |#n #Hn @(transitive_le ? (exp 2 (2*(S n))*teta (S (S n))))
-      [@lt_to_le @lt_O_to_le_teta_exp_teta @lt_O_S
+    |#n #Hn @(transitive_le ? (exp 2 (2*(S n))*theta (S (S n))))
+      [@lt_to_le @lt_O_to_le_theta_exp_theta @lt_O_S
       |>times2 in ⊢ (??%); <plus_n_Sm <commutative_plus >plus_n_Sm
        >exp_plus_times in ⊢ (??%); @monotonic_le_times_r
        cut (∀a. 2*(S a) = S(S(2*a))) [#a normalize <plus_n_Sm //] #timesSS