From: Andrea Asperti Date: Tue, 18 Dec 2012 11:33:24 +0000 (+0000) Subject: chebyshev_teta X-Git-Tag: make_still_working~1387 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1bfde0925874b6c3ec12998d6ebb30ae597c2060;p=helm.git chebyshev_teta --- diff --git a/matita/matita/lib/arithmetics/chebyshev/chebyshev_teta.ma b/matita/matita/lib/arithmetics/chebyshev/chebyshev_teta.ma new file mode 100644 index 000000000..5bb3a2507 --- /dev/null +++ b/matita/matita/lib/arithmetics/chebyshev/chebyshev_teta.ma @@ -0,0 +1,214 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "arithmetics/binomial.ma". +include "arithmetics/gcd.ma". +include "arithmetics/chebyshev/chebyshev.ma". + +(* This is chebishev teta function *) + +definition teta: nat → nat ≝ λn. + ∏_{p < S n| primeb p} p. + +lemma teta_def: ∀n.teta n = ∏_{p < S n| primeb p} p. +// qed. + +theorem lt_O_teta: ∀n. O < teta n. +#n elim n + [@le_n + |#n1 #Hind cases (true_or_false (primeb (S n1))) #Hc + [>teta_def >bigop_Strue + [>(times_n_O O) @lt_times // | //] + |>teta_def >bigop_Sfalse // + ] + ] +qed. + +theorem divides_fact_to_divides: ∀p,n. prime p → divides p n! → + ∃m.O < m ∧ m \le n ∧ divides p m. +#p #n #primep elim n + [normalize in ⊢ (%→?); #H @False_ind @(absurd (p ≤1)) + [@divides_to_le //|@lt_to_not_le @prime_to_lt_SO @primep] + |#n1 #Hind >factS #Hdiv + cases (divides_times_to_divides ??? primep Hdiv) #Hcase + [%{(S n1)} %[ % [@lt_O_S |@le_n] |@Hcase] + |cases(Hind Hcase) #a * * #posa #lea #diva + %{a} % [% [// |@le_S //] |//] + ] + ] +qed. + +theorem divides_fact_to_le: ∀p,n. prime p → divides p n! → p ≤ n. +#p #n #primep #divp cases (divides_fact_to_divides p n primep divp) +#a * * #posa #lea #diva @(transitive_le ? a) [@divides_to_le // | //] +qed. + +theorem prime_to_divides_M: ∀m,p. + prime p → S m < p → p ≤ S(2*m) → divides p (M m). +#m #p #primep #lemp #lep >Mdef >bceq +cases (bc2 (S(2*m)) m ?) + [#q #Hq >Hq >commutative_times >div_times + [cases (divides_times_to_divides p (m!*(S (2*m)-m)!) q primep ?) + [#Hdiv @False_ind + cases (divides_times_to_divides p (m!) (S (2*m)-m)! primep ?) + [-Hdiv #Hdiv @(absurd (p ≤ m)) + [@divides_fact_to_le // + |@(lt_to_not_le ?? (lt_to_le ?? lemp)) + ] + |-Hdiv #Hdiv @(absurd (p ≤S m)) + [@(divides_fact_to_le … primep) + cut (S m = S(2*m)-m) + [normalize in ⊢ (???(?%?)); plus_n_Sm >commutative_plus @minus_plus_m_m + ] #HSm + >HSm // + |@lt_to_not_le // + ] + |// + ] + |// + |(times_n_O O) in ⊢ (?%?); @lt_times // + ] + |normalize in ⊢ (??(?%)); commutative_times @times_n_1 + |#n #Hind #len + cases (true_or_false (leb (S (S m)) n ∧ primeb n)) #Hc + [>bigop_Strue + [@divides_to_divides_times + [@primeb_true_to_prime @(andb_true_r ?? Hc) + |cut (∀p.prime p → n ≤ p → ¬p∣∏_{p < n | leb (S (S m)) p∧primeb p} p) + [2: #Hcut @(Hcut … (le_n ?)) @primeb_true_to_prime @(andb_true_r ?? Hc)] + #p #primep elim n + [#_ normalize @(not_to_not ? (p ≤ 1)) + [@divides_to_le @lt_O_S|@lt_to_not_le @prime_to_lt_SO //] + |#n1 #Hind1 #Hn1 cases (true_or_false (leb (S (S m)) n1∧primeb n1)) #Hc1 + [>bigop_Strue + [% #Habs cases(divides_times_to_divides ??? primep Habs) + [-Habs #Habs @(absurd … Hn1) @le_to_not_lt + @(divides_to_le … Habs) @prime_to_lt_O + @primeb_true_to_prime @(andb_true_r ?? Hc1) + |-Habs #Habs @(absurd … Habs) @Hind1 @lt_to_le // + ] + |@Hc1 + ] + |>bigop_Sfalse // @Hind1 @lt_to_le // + ] + ] + |@prime_to_divides_M + [@primeb_true_to_prime @(andb_true_r ?? Hc) + |@leb_true_to_le @(andb_true_l ?? Hc) + |@le_S_S_to_le // + ] + |@Hind @lt_to_le // + ] + |@Hc + ] + |>bigop_Sfalse // @Hind @lt_to_le @len + ] + ] +qed. + +theorem divides_pi_p_M:∀m. + ∏_{p < S(S(2*m)) | leb (S(S m)) p ∧ primeb p} 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 +<(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] +@eq_f2 + [>bigop_I_gen // |@(bigop_I … timesA)] +qed. + +theorem div_teta_teta: ∀m. + teta (S(2*m))/teta (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 |teta_pi_p_teta @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 //] + ] +qed. + +theorem teta_pred: ∀n. 1 < n → teta (2*n) = teta (pred (2*n)). +#n #lt1n >teta_def >teta_def >bigop_Sfalse + [>S_pred + [// + |>(times_n_O 2) in ⊢ (?%?); @monotonic_lt_times_r @lt_to_le // + ] + |@not_prime_to_primeb_false % * #lt2n #Hprime + @(absurd (2=2*n)) + [@(Hprime … (le_n ?)) %{n} // + |@lt_to_not_eq >(times_n_1 2) in ⊢ (?%?); @monotonic_lt_times_r // + ] + ] +qed. + +theorem le_teta: ∀m.teta 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 + [lapply Ha cases a + [#_ @le_n + |#n cases n + [#_ @leb_true_to_le // + |#n1 #Hn1 >teta_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 + |>times2 in ⊢ (??%);>exp_plus_times in ⊢ (??%); @le_times + [@le_exp [@lt_O_S |@monotonic_le_times_r @le_n_Sn] + |@Hind >Hn1 >times2 // + ] + ] + |@le_S_S @lt_O_S + ] + ] + ] + |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 + |>times2 in ⊢ (??%); plus_n_Sm + >exp_plus_times in ⊢ (??%); @monotonic_le_times_r + cut (∀a. 2*(S a) = S(S(2*a))) [#a normalize Hn @le_S_S >times2 // + ] + ] + ] +qed. +