]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/arithmetics/chebyshev/chebyshev_psi.ma
Refactoring
[helm.git] / matita / matita / lib / arithmetics / chebyshev / chebyshev_psi.ma
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic   
3     ||A||  Library of Mathematics, developed at the Computer Science 
4     ||T||  Department of the University of Bologna, Italy.           
5     ||I||                                                            
6     ||T||  
7     ||A||  
8     \   /  This file is distributed under the terms of the       
9      \ /   GNU General Public License Version 2   
10       V_____________________________________________________________*)
11
12 include "arithmetics/log.ma". 
13 include "arithmetics/sigma_pi.ma". 
14
15 (* (prim n) counts the number of prime numbers up to n included *)
16 definition prim ≝ λn. ∑_{i < S n | primeb i} 1.
17
18 lemma le_prim_n: ∀n. prim n ≤ n.
19 #n elim n // -n #n #H
20 whd in ⊢ (?%?); cases (primeb (S n)) whd in ⊢ (?%?);
21   [@le_S_S @H |@le_S @H]
22 qed.
23
24 lemma not_prime_times_2: ∀n. 1 < n → ¬prime (2*n).
25 #n #ltn % * #H #H1 @(absurd (2 = 2*n))
26   [@H1 // %{n} //
27   |@lt_to_not_eq >(times_n_1 2) in ⊢ (?%?); @monotonic_lt_times_r //
28   ]
29 qed.
30
31 theorem eq_prim_prim_pred: ∀n. 1 < n → 
32   prim (2*n) = prim (pred (2*n)).
33 #n #ltn 
34 lapply (S_pred (2*n) ?) [>(times_n_1 0) in ⊢ (?%?); @lt_times //] #H2n
35 lapply (not_prime_times_2 n ltn) #notp2n
36 whd in ⊢ (??%?); >(not_prime_to_primeb_false … notp2n) whd in ⊢ (??%?);
37 <H2n in ⊢ (??%?); % 
38 qed.
39
40 theorem le_prim_n1: ∀n. 4 ≤ n → 
41   prim (S(2*n)) ≤ n.
42 #n #le4 elim le4 -le4
43   [@le_n
44   |#m #le4 cut (S (2*m) = pred (2*(S m))) [normalize //] #Heq >Heq
45    <eq_prim_prim_pred [2: @le_S_S @(transitive_le … le4) //] 
46    #H whd in ⊢ (?%?); cases (primeb (S (2*S m))) 
47     [@le_S_S @H |@le_S @H]
48   ]
49 qed.
50     
51 (* usefull to kill a successor in bertrand *) 
52 theorem le_prim_n2: ∀n. 7 ≤ n → prim (S(2*n)) ≤ pred n.
53 #n #le7 elim le7 -le7
54   [@le_n
55   |#m #le7 cut (S (2*m) = pred (2*(S m))) [normalize //] #Heq >Heq
56    <eq_prim_prim_pred [2: @le_S_S @(transitive_le … le7) //] 
57    #H whd in ⊢ (?%?); 
58    whd in ⊢ (??%); <(S_pred m) in ⊢ (??%); [2: @(transitive_le … le7) //]
59    cases (primeb (S (2*S m))) [@le_S_S @H |@le_S @H]
60   ]
61 qed.
62
63 lemma even_or_odd: ∀n.∃a.n=2*a ∨ n = S(2*a).
64 #n elim n -n 
65   [%{0} %1 %
66   |#n * #a * #Hn [%{a} %2 @eq_f @Hn | %{(S a)} %1 >Hn normalize //
67   ]
68 qed.
69
70 (* la prova potrebbe essere migliorata *)
71 theorem le_prim_n3: ∀n. 15 ≤ n →
72   prim n ≤ pred (n/2).
73 #n #len cases (even_or_odd (pred n)) #a * #Hpredn
74   [cut (n = S (2*a)) [<Hpredn @sym_eq @S_pred @(transitive_le … len) //] #Hn
75    >Hn @(transitive_le ? (pred a))
76     [@le_prim_n2 @(le_times_to_le 2) [//|@le_S_S_to_le <Hn @len]
77     |@monotonic_pred @le_times_to_le_div //
78     ]
79   |cut (n = (2*S a)) 
80     [normalize normalize in Hpredn:(???%); <plus_n_Sm <Hpredn @sym_eq @S_pred
81      @(transitive_le … len) //] #Hn 
82    >Hn @(transitive_le ? (pred a)) 
83     [>eq_prim_prim_pred 
84       [2:@(lt_times_n_to_lt_r 2) <Hn @(transitive_le … len) //]
85      <Hn >Hpredn @le_prim_n2 @le_S_S_to_le @(lt_times_n_to_lt_r 2) <Hn @len
86     |@monotonic_pred @le_times_to_le_div //
87     ]
88   ]
89 qed. 
90
91 (* This is chebishev psi function *)
92 definition Psi: nat → nat ≝
93   λn.∏_{p < S n | primeb p} (exp p (log p n)).
94   
95 definition psi_def : ∀n. 
96   Psi n = ∏_{p < S n | primeb p} (exp p (log p n)).
97 // qed.
98
99 theorem le_Psil1: ∀n.
100   Psi n ≤ ∏_{p < S n | primeb p} n.
101 #n cases n [@le_n |#m @le_pi #i #_ #_ @le_exp_log //]
102 qed.
103
104 theorem le_Psil: ∀n. Psi n ≤ exp n (prim n).
105 #n <exp_sigma @le_Psil1
106 qed.
107
108 theorem lePsi_r2: ∀n.
109   exp n (prim n) ≤ Psi n * Psi n.
110 #n elim (le_to_or_lt_eq ?? (le_O_n n)) #Hn
111   [<(exp_sigma (S n) n primeb) <times_pi
112    @le_pi #i #lti #primei 
113    cut (1<n) 
114      [@(lt_to_le_to_lt … (le_S_S_to_le … lti)) @prime_to_lt_SO 
115       @primeb_true_to_prime //] #lt1n
116    <exp_plus_times
117    @(transitive_le ? (exp i (S(log i n))))
118     [@lt_to_le @lt_exp_log @prime_to_lt_SO @primeb_true_to_prime //
119     |@le_exp 
120       [@prime_to_lt_O @primeb_true_to_prime //
121       |>(plus_n_O (log i n)) in ⊢ (?%?); >plus_n_Sm
122        @monotonic_le_plus_r @lt_O_log //
123        @le_S_S_to_le //
124       ]
125     ]
126   |<Hn @le_n
127   ]
128 qed.
129
130 (* an equivalent formulation for psi *)
131 definition Psi': nat → nat ≝
132 λn. ∏_{p < S n | primeb p} (∏_{i < log p n} p).
133
134 lemma Psidef: ∀n. Psi' n = ∏_{p < S n | primeb p} (∏_{i < log p n} p).
135 // qed-.
136
137 theorem eq_Psi_Psi': ∀n.Psi n = Psi' n.
138 #n @same_bigop // #i #lti #primebi
139 @(trans_eq ? ? (exp i (∑_{x < log i n} 1)))
140   [@eq_f @sym_eq @sigma_const
141   |@sym_eq @exp_sigma
142   ]
143 qed.