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.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "arithmetics/binomial.ma".
13 include "arithmetics/gcd.ma".
14 include "arithmetics/chebyshev/chebyshev.ma".
16 (* This is chebishev teta function *)
18 definition teta: nat → nat ≝ λn.
19 ∏_{p < S n| primeb p} p.
21 lemma teta_def: ∀n.teta n = ∏_{p < S n| primeb p} p.
24 theorem lt_O_teta: ∀n. O < teta n.
27 |#n1 #Hind cases (true_or_false (primeb (S n1))) #Hc
28 [>teta_def >bigop_Strue
29 [>(times_n_O O) @lt_times // | //]
30 |>teta_def >bigop_Sfalse //
35 theorem divides_fact_to_divides: ∀p,n. prime p → divides p n! →
36 ∃m.O < m ∧ m \le n ∧ divides p m.
38 [normalize in ⊢ (%→?); #H @False_ind @(absurd (p ≤1))
39 [@divides_to_le //|@lt_to_not_le @prime_to_lt_SO @primep]
40 |#n1 #Hind >factS #Hdiv
41 cases (divides_times_to_divides ??? primep Hdiv) #Hcase
42 [%{(S n1)} %[ % [@lt_O_S |@le_n] |@Hcase]
43 |cases(Hind Hcase) #a * * #posa #lea #diva
44 %{a} % [% [// |@le_S //] |//]
49 theorem divides_fact_to_le: ∀p,n. prime p → divides p n! → p ≤ n.
50 #p #n #primep #divp cases (divides_fact_to_divides p n primep divp)
51 #a * * #posa #lea #diva @(transitive_le ? a) [@divides_to_le // | //]
54 theorem prime_to_divides_M: ∀m,p.
55 prime p → S m < p → p ≤ S(2*m) → divides p (M m).
56 #m #p #primep #lemp #lep >Mdef >bceq
57 cases (bc2 (S(2*m)) m ?)
58 [#q #Hq >Hq >commutative_times >div_times
59 [cases (divides_times_to_divides p (m!*(S (2*m)-m)!) q primep ?)
61 cases (divides_times_to_divides p (m!) (S (2*m)-m)! primep ?)
62 [-Hdiv #Hdiv @(absurd (p ≤ m))
63 [@divides_fact_to_le //
64 |@(lt_to_not_le ?? (lt_to_le ?? lemp))
66 |-Hdiv #Hdiv @(absurd (p ≤S m))
67 [@(divides_fact_to_le … primep)
69 [normalize in ⊢ (???(?%?)); <plus_n_O
70 >plus_n_Sm >commutative_plus @minus_plus_m_m
78 |<Hq @divides_fact [@prime_to_lt_O // |//]
80 |>(times_n_O O) in ⊢ (?%?); @lt_times //
82 |normalize in ⊢ (??(?%)); <plus_n_O //
86 theorem divides_pi_p_M1: ∀m.∀i. i ≤ S(S(2*m)) →
87 ∏_{p < i | leb (S(S m)) p ∧ primeb p} p ∣ M m .
89 [#_ @(quotient ?? (M m)) >commutative_times @times_n_1
91 cases (true_or_false (leb (S (S m)) n ∧ primeb n)) #Hc
93 [@divides_to_divides_times
94 [@primeb_true_to_prime @(andb_true_r ?? Hc)
95 |cut (∀p.prime p → n ≤ p → ¬p∣∏_{p < n | leb (S (S m)) p∧primeb p} p)
96 [2: #Hcut @(Hcut … (le_n ?)) @primeb_true_to_prime @(andb_true_r ?? Hc)]
98 [#_ normalize @(not_to_not ? (p ≤ 1))
99 [@divides_to_le @lt_O_S|@lt_to_not_le @prime_to_lt_SO //]
100 |#n1 #Hind1 #Hn1 cases (true_or_false (leb (S (S m)) n1∧primeb n1)) #Hc1
102 [% #Habs cases(divides_times_to_divides ??? primep Habs)
103 [-Habs #Habs @(absurd … Hn1) @le_to_not_lt
104 @(divides_to_le … Habs) @prime_to_lt_O
105 @primeb_true_to_prime @(andb_true_r ?? Hc1)
106 |-Habs #Habs @(absurd … Habs) @Hind1 @lt_to_le //
110 |>bigop_Sfalse // @Hind1 @lt_to_le //
114 [@primeb_true_to_prime @(andb_true_r ?? Hc)
115 |@leb_true_to_le @(andb_true_l ?? Hc)
122 |>bigop_Sfalse // @Hind @lt_to_le @len
127 theorem divides_pi_p_M:∀m.
128 ∏_{p < S(S(2*m)) | leb (S(S m)) p ∧ primeb p} p ∣ (M m).
129 #m @divides_pi_p_M1 @le_n
132 theorem teta_pi_p_teta: ∀m. teta (S (2*m))
133 = (∏_{p < S (S (2*m)) | leb (S (S m)) p∧primeb p} p)*teta (S m).
134 #m >teta_def >teta_def
135 <(bigop_I ???? timesA)
136 >(bigop_sumI 0 (S(S m)) (S(S(2*m))) (λp.primeb p) … timesA (λp.p))
137 [2:@le_S_S @le_S_S // |3:@le_O_n]
139 [>bigop_I_gen // |@(bigop_I … timesA)]
142 theorem div_teta_teta: ∀m.
143 teta (S(2*m))/teta (S m) =
144 ∏_{p < S(S(2*m)) | leb (S(S m)) p ∧ primeb p} p.
145 #m @(div_mod_spec_to_eq ????? 0 (div_mod_spec_div_mod …))
147 |@div_mod_spec_intro [@lt_O_teta |<plus_n_O @teta_pi_p_teta]
151 theorem le_teta_M_teta: ∀m.
152 teta (S(2*m)) ≤ (M m)*teta (S m).
153 #m >teta_pi_p_teta @le_times [2://] @divides_to_le
154 [@lt_O_bc @lt_to_le @le_S_S // | @divides_pi_p_M
158 theorem lt_O_to_le_teta_exp_teta: ∀m. O < m→
159 teta (S(2*m)) < exp 2 (2*m)*teta (S m).
160 #m #posm @(le_to_lt_to_lt ? (M m*teta (S m)))
162 |@monotonic_lt_times_l [@lt_O_teta|@lt_M //]
166 theorem teta_pred: ∀n. 1 < n → teta (2*n) = teta (pred (2*n)).
167 #n #lt1n >teta_def >teta_def >bigop_Sfalse
170 |>(times_n_O 2) in ⊢ (?%?); @monotonic_lt_times_r @lt_to_le //
172 |@not_prime_to_primeb_false % * #lt2n #Hprime
174 [@(Hprime … (le_n ?)) %{n} //
175 |@lt_to_not_eq >(times_n_1 2) in ⊢ (?%?); @monotonic_lt_times_r //
180 theorem le_teta: ∀m.teta m ≤ exp 2 (2*m).
181 #m @(nat_elim1 m) #m1 #Hind
182 cut (∀a. 2 *a = a+a) [//] #times2
183 cases (even_or_odd m1) #a * #Ha >Ha
187 [#_ @leb_true_to_le //
189 [cut (pred (2*S(S n1)) = (S (2*S n1)))
190 [normalize >plus_n_Sm in ⊢ (???%); //] #Hcut >Hcut
191 @(transitive_le ? (exp 2 (2*(S n1))*teta (S (S n1))))
192 [@lt_to_le @lt_O_to_le_teta_exp_teta @lt_O_S
193 |>times2 in ⊢ (??%);>exp_plus_times in ⊢ (??%); @le_times
194 [@le_exp [@lt_O_S |@monotonic_le_times_r @le_n_Sn]
195 |@Hind >Hn1 >times2 //
203 [#_ @leb_true_to_le //
204 |#n #Hn @(transitive_le ? (exp 2 (2*(S n))*teta (S (S n))))
205 [@lt_to_le @lt_O_to_le_teta_exp_teta @lt_O_S
206 |>times2 in ⊢ (??%); <plus_n_Sm <commutative_plus >plus_n_Sm
207 >exp_plus_times in ⊢ (??%); @monotonic_le_times_r
208 cut (∀a. 2*(S a) = S(S(2*a))) [#a normalize <plus_n_Sm //] #timesSS
209 <timesSS @Hind >Hn @le_S_S >times2 //