From 342278d86d2ebb11b046dcc9f44cc5d08cd16352 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 3 Jan 2013 16:15:54 +0000 Subject: [PATCH] Chebishev ported --- matita/matita/lib/arithmetics/bigops.ma | 2 +- matita/matita/lib/arithmetics/binomial.ma | 10 -- .../lib/arithmetics/chebyshev/bertrand.ma | 50 +++++----- .../lib/arithmetics/chebyshev/bertrand256.ma | 96 +++++++------------ .../lib/arithmetics/chebyshev/chebyshev.ma | 23 ++--- matita/matita/lib/arithmetics/log.ma | 2 +- matita/matita/lib/arithmetics/minimization.ma | 19 +++- matita/matita/lib/arithmetics/ord.ma | 11 +-- matita/matita/lib/arithmetics/sqrt.ma | 66 ++++++++++++- 9 files changed, 155 insertions(+), 124 deletions(-) diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma index a1b98e180..e51cd799a 100644 --- a/matita/matita/lib/arithmetics/bigops.ma +++ b/matita/matita/lib/arithmetics/bigops.ma @@ -163,7 +163,7 @@ op (\big[op,nil]_{i(commutative_plus c) +#a #b #c #lecb @sym_eq @plus_to_minus >(commutative_plus c) >associative_plus H2 in ⊢ (??(?%?)); ] qed. -(* -theorem exp_Sn_SSO: \forall n. exp (S n) 2 = S((exp n 2) + 2*n). -intros.simplify. -rewrite < times_n_SO. -rewrite < plus_n_O. -rewrite < sym_times.simplify. -rewrite < assoc_plus. -rewrite < sym_plus. -reflexivity. -qed. *) diff --git a/matita/matita/lib/arithmetics/chebyshev/bertrand.ma b/matita/matita/lib/arithmetics/chebyshev/bertrand.ma index df94a30f6..d4a228a2c 100644 --- a/matita/matita/lib/arithmetics/chebyshev/bertrand.ma +++ b/matita/matita/lib/arithmetics/chebyshev/bertrand.ma @@ -10,8 +10,8 @@ V_______________________________________________________________ *) include "arithmetics/sqrt.ma". -include "arithmetics/chebyshev/chebyshev_B.ma". -include "arithmetics/chebyshev/chebyshev_teta.ma". +include "arithmetics/chebyshev/psi_bounds.ma". +include "arithmetics/chebyshev/chebyshev_teta.ma". definition bertrand ≝ λn. ∃p.n < p ∧ p ≤ 2*n ∧ prime p. @@ -85,38 +85,38 @@ theorem le_k: ∀n,p. k n p ≤ log p n. ] qed. -definition B1 ≝ λn. +definition Bk ≝ λn. ∏_{p < S n | primeb p}(exp p (k n p)). -lemma B1_def : ∀n. B1 n = ∏_{p < S n | primeb p}(exp p (k n p)). +lemma Bk_def : ∀n. Bk n = ∏_{p < S n | primeb p}(exp p (k n p)). // qed. definition Dexp ≝ mk_Dop nat 1 timesAC (λa,b.exp b a) ??. [// | normalize //] qed. -theorem eq_B_B1: ∀n. B n = B1 n. -#n >Bdef >B1_def @same_bigop +theorem eq_B_Bk: ∀n. B n = Bk n. +#n >Bdef >Bk_def @same_bigop [// |#i #ltiS #_ >k_def @exp_sigma_l] qed. -definition B_split1 ≝ λn. +definition B1 ≝ λn. ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb (k n p) 1)* (k n p))). -lemma B_split1_def : ∀n. - B_split1 n = ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb (k n p) 1)* (k n p))). +lemma B1_def : ∀n. + B1 n = ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb (k n p) 1)* (k n p))). // qed. -definition B_split2 ≝ λn. +definition B2 ≝ λn. ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb 2 (k n p))* (k n p))). -lemma B_split2_def : ∀n. - B_split2 n = ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb 2 (k n p))* (k n p))). +lemma B2_def : ∀n. + B2 n = ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb 2 (k n p))* (k n p))). // qed. -theorem eq_B1_times_B_split1_B_split2: ∀n. - B1 n = B_split1 n * B_split2 n. -#n >B1_def >B_split1_def >B_split2_def Bk_def >B1_def >B2_def Hc @@ -189,9 +189,9 @@ elim (log p (2*n)) ] qed. -theorem le_B_split1_teta:∀n.18 ≤ n → not_bertrand n → - B_split1 (2*n) ≤ teta (2 * n / 3). -#n #le18 #not_Bn >B_split1_def >teta_def +theorem le_B1_teta:∀n.18 ≤ n → not_bertrand n → + B1 (2*n) ≤ teta (2 * n / 3). +#n #le18 #not_Bn >B1_def >teta_def @(transitive_le ? (∏_{p < S (2*n) | primeb p} (p\sup(bool_to_nat (eqb (k (2*n) p) 1))))) [@le_pi #p #ltp #primebp @le_exp [@prime_to_lt_O @primeb_true_to_prime // @@ -224,9 +224,9 @@ theorem le_B_split1_teta:∀n.18 ≤ n → not_bertrand n → ] qed. -theorem le_B_split2_exp: ∀n. exp 2 7 ≤ n → - B_split2 (2*n) ≤ exp (2*n) (pred(sqrt(2*n)/2)). -#n #len >B_split2_def +theorem le_B2_exp: ∀n. exp 2 7 ≤ n → + B2 (2*n) ≤ exp (2*n) (pred(sqrt(2*n)/2)). +#n #len >B2_def cut (O < n) [@(lt_to_le_to_lt … len) @leb_true_to_le //] #posn @(transitive_le ? (∏_{p < S (sqrt (2*n)) | primeb p} @@ -279,12 +279,12 @@ qed. theorem not_bertrand_to_le_B: ∀n.exp 2 7 ≤ n → not_bertrand n → B (2*n) ≤ (exp 2 (2*(2 * n / 3)))*(exp (2*n) (pred(sqrt(2*n)/2))). -#n #len #notB >eq_B_B1 >eq_B1_times_B_split1_B_split2 @le_times +#n #len #notB >eq_B_Bk >eq_Bk_B1_B2 @le_times [@(transitive_le ? (teta ((2*n)/3))) - [@le_B_split1_teta [@(transitive_le … len) @leb_true_to_le //|//] + [@le_B1_teta [@(transitive_le … len) @leb_true_to_le //|//] |@le_teta ] - |@le_B_split2_exp // + |@le_B2_exp // ] qed. @@ -429,7 +429,7 @@ cut (0 match t1 with - [ nil ⇒ true - | cons h2 t2 ⇒ (andb (checker t1) (leb h1 (2*h2))) ]]. - -lemma checker_ab: ∀a,b,l. - checker (a::b::l) = (andb (checker (b::l)) (leb a (2*b))). -// qed. - -lemma checker_cons : ∀a,l.checker (a::l) = true → checker l = true. -#a #l cases l [//|#b #tl >checker_ab #H @(andb_true_l ?? H)] -qed. - -theorem list_of_primes_to_bertrand: -∀n,pn,l.0 < n → prime pn → n < pn → all_primes l → -(∀p. prime p → p ≤ pn → mem ? p l) → -(∀p. mem ? p l → 2 < p → - ∃pp. mem ? pp l ∧ pp < p ∧ p \le 2*pp) → bertrand n. -#n #pn #l #posn #primepn #ltnp #allprimes #H1 #H2 +(* check *) +theorem primes_below_to_bertrand: +∀pm,l.prime pm → primes_below l (S pm) → + (∀p. mem ? p l → 2 < p → ∃pp. mem ? pp l ∧ pp < p ∧ p ≤ 2*pp) + → ∀n.0 < n → n < pm → bertrand n. +#pm #l #primepm * * #Hall #Hbelow #Hcomplete #H #n #posn #ltn cases (min_prim n) #p1 * * #ltnp1 #primep1 #Hmin %{p1} % // % [//] cases(le_to_or_lt_eq ? ? (prime_to_lt_SO ? primep1)) #Hp1 - [cases (H2 … Hp1) - [#x * * #memxl #ltxp1 #H @(transitive_le … H) @monotonic_le_times_r - @Hmin [@allprimes //|//] - |@H1 [//] @not_lt_to_le % #ltpn @(absurd ? ltnp) + [cases (H … Hp1) + [#x * * #memxl #ltxp1 #Hp1 @(transitive_le … Hp1) @monotonic_le_times_r + @Hmin [@Hall //|//] + |@Hcomplete [//] @le_S_S @not_lt_to_le % #ltpm @(absurd ? ltn) @le_to_not_lt @Hmin // ] |(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r // ] qed. -let rec check_list l ≝ +let rec checker l ≝ match l with [ nil ⇒ true - | cons (hd:nat) tl ⇒ + | cons hd tl ⇒ match tl with [ nil ⇒ true | cons hd1 tl1 ⇒ - (leb (S hd) hd1 ∧ leb hd1 (2*hd) ∧ check_list tl) + leb (S hd) hd1 ∧ leb hd1 (2*hd) ∧ checker tl ] - ] -. + ]. -lemma check_list_ab: ∀a,b,l.check_list (a::b::l) = - (leb (S a) b ∧ leb b (2*a) ∧ check_list (b::l)). +lemma checker_ab: ∀a,b,l.checker (a::b::l) = + (leb (S a) b ∧ leb b (2*a) ∧ checker (b::l)). // qed. -lemma check_list_abl: ∀a,b,l.check_list (a::b::l) = true → - a < b ∧ - b ≤ 2*a ∧ - check_list (b::l) = true ∧ - check_list l = true. -#a #b #l >check_list_ab #H -lapply (andb_true_r ?? H) #H1 -lapply (andb_true_l ?? H) -H #H2 -lapply (andb_true_r ?? H2) #H3 -lapply (andb_true_l ?? H2) -H2 #H4 -% [% [% [@(leb_true_to_le … H4) |@(leb_true_to_le … H3)]|@H1] - |lapply H1 cases l - [// - |#c #d >check_list_ab #H @(andb_true_r … H) - ] +lemma checker_abl: ∀a,b,l.checker (a::b::l) = true → + a < b ∧ b ≤ 2*a ∧ checker (b::l) = true. +#a #b #l >checker_ab #H +% [% [@leb_true_to_le @(andb_true_l … (andb_true_l … H)) + |@leb_true_to_le @(andb_true_r … (andb_true_l … H)) + ] + |@(andb_true_r … H) ] qed. -theorem check_list_spec: ∀tl,a,l. check_list l = true → l = a::tl → +theorem checker_spec: ∀tl,a,l. checker l = true → l = a::tl → ∀p. mem ? p tl → ∃pp. mem nat pp l ∧ pp < p ∧ p ≤ 2*pp. #tl elim tl [#a #l #_ #_ #p whd in ⊢ (%→?); @False_ind |#b #tl #Hind #a #l #Hc #Hl #p #Hmem >Hl in Hc; - #Hc cases(check_list_abl … Hc) * * - #ltab #leb #Hc2 #Hc3 cases Hmem #Hc + #Hc cases(checker_abl … Hc) * + #ltab #leb #Hc2 cases Hmem #Hc [>Hc -Hc %{a} % [ % [ % % |//]|//] |cases(Hind b (b::tl) Hc2 (refl …) ? Hc) #pp * * #Hmemnp #ltpp #lepp %{pp} % [ % [ %2 //|//]|//] @@ -237,17 +213,14 @@ theorem check_list_spec: ∀tl,a,l. check_list l = true → l = a::tl → ] qed. -lemma le_to_bertrand : ∀n.O < n → n ≤ 2^8 → bertrand n. +lemma bertrand_down : ∀n.O < n → n ≤ 2^8 → bertrand n. #n #posn #len cut (∃it.it=2^8) [%{(2^8)} %] * #it #itdef lapply(primes_below_lop … it) * * #Hall #Hbelow #Hcomplete -@(list_of_primes_to_bertrand ? (S it) (list_of_primes it) posn) +@(primes_below_to_bertrand (S it) (list_of_primes it) … posn) [@primeb_true_to_prime >itdef % - |@le_S_S >itdef @len - |@Hall - |#p #primep #lep @Hcomplete - [@primep |(plus_n_O it) in ⊢ (??%); >plus_n_Sm >plus_n_Sm @primes_below_lop + |#p #memp #lt2p @(checker_spec (tail ? (list_of_primes it)) 2 (list_of_primes it)) [>itdef % |>itdef @eq_lop @lt_O_S |>eq_lop in memp; [2:>itdef @lt_O_S] * @@ -255,17 +228,14 @@ lapply(primes_below_lop … it) * * #Hall #Hbelow #Hcomplete |#H @H ] ] + |@le_S_S >itdef @len ] qed. -theorem bertrand_n : +theorem bertrand : ∀n. O < n → bertrand n. #n #posn elim (decidable_le n 256) - [@le_to_bertrand // + [@bertrand_down // |#len @le_to_bertrand2 @lt_to_le @not_le_to_lt @len] qed. -(* test -theorem mod_exp: eqb (mod (exp 2 8) 13) O = false. -reflexivity. -*) diff --git a/matita/matita/lib/arithmetics/chebyshev/chebyshev.ma b/matita/matita/lib/arithmetics/chebyshev/chebyshev.ma index 4195de34b..50fb09fd7 100644 --- a/matita/matita/lib/arithmetics/chebyshev/chebyshev.ma +++ b/matita/matita/lib/arithmetics/chebyshev/chebyshev.ma @@ -90,24 +90,24 @@ theorem le_prim_n3: ∀n. 15 ≤ n → qed. (* This is chebishev psi function *) -definition A: nat → nat ≝ +definition Psi: nat → nat ≝ λn.∏_{p < S n | primeb p} (exp p (log p n)). definition psi_def : ∀n. - A n = ∏_{p < S n | primeb p} (exp p (log p n)). + Psi n = ∏_{p < S n | primeb p} (exp p (log p n)). // qed. -theorem le_Al1: ∀n. - A n ≤ ∏_{p < S n | primeb p} n. +theorem le_Psil1: ∀n. + Psi n ≤ ∏_{p < S n | primeb p} n. #n cases n [@le_n |#m @le_pi #i #_ #_ @le_exp_log //] qed. -theorem le_Al: ∀n. A n ≤ exp n (prim n). -#n (exp_ord p ? lt1p posn) in ⊢ (??(??%)); diff --git a/matita/matita/lib/arithmetics/log.ma b/matita/matita/lib/arithmetics/log.ma index 733720ce3..bbd65be96 100644 --- a/matita/matita/lib/arithmetics/log.ma +++ b/matita/matita/lib/arithmetics/log.ma @@ -140,7 +140,7 @@ theorem log_exp: ∀p,n,m. 1 < p → O < m → |#i #Hi #Hm @lt_to_leb_false @(lt_to_le_to_lt ? ((exp p n)*(exp p (S(log p m))))) [@monotonic_lt_times_r [@lt_O_exp @lt_to_le // |@lt_exp_log //] - |ext normalize in Hind; >Hind // -#i #ltim @ext /2/ +#i #ltim @ext @le_S // qed. theorem le_max_f_max_g: ∀f,g,n. (∀i. i < n → f i = true → g i =true) → @@ -131,7 +131,7 @@ max n f ≤ max n g. #f #g #n (elim n) // #m #Hind #ext normalize (cases (true_or_false (f m))) #Heq >Heq [>ext // - |(cases (g m)) normalize [@le_max_n] @Hind #i #ltim @ext /2/ + |(cases (g m)) normalize [@le_max_n] @Hind #i #ltim @ext @le_S // qed. theorem f_max_true : ∀ f.∀n. @@ -173,6 +173,17 @@ cases (exists_forall_lt f n) ] qed. + +theorem false_to_lt_max: ∀f,n,m.O < n → + f n = false → max m f ≤ n → max m f < n. +#f #n #m #posn #Hfn #Hmax cases (le_to_or_lt_eq ?? Hmax) -Hmax #Hmax + [// + |cases (exists_max_forall_false f m) + [* #_ #Hfmax @False_ind @(absurd ?? not_eq_true_false) // + |* // + ] + ] +qed. (* minimization *) (* min k b f is the minimun i, b ≤ i < b + k s.t. f i; @@ -318,7 +329,7 @@ theorem min_f_g: ∀f,g,n,b.(∀i. b ≤ i → i < n + b → f i = g i) → min n b f = min n b g. #f #g #n (elim n) // #m #Hind #b #ext normalize >(ext b (le_n b) ?) // >Hind // -#i #ltib #ltim @ext /2/ +#i #ltib #ltim @ext // @lt_to_le // qed. theorem le_min_f_min_g: ∀f,g,n,b. (∀i. b ≤ i → i < n +b → f i = true → g i =true) → @@ -326,7 +337,7 @@ min n b g ≤ min n b f. #f #g #n (elim n) // #m #Hind #b #ext normalize (cases (true_or_false (f b))) #Heq >Heq [>ext // - |(cases (g b)) normalize /2/ @Hind #i #ltb #ltim #fi + |(cases (g b)) normalize /2 by lt_to_le/ @Hind #i #ltb #ltim #fi @ext /2/ ] qed. diff --git a/matita/matita/lib/arithmetics/ord.ma b/matita/matita/lib/arithmetics/ord.ma index 452106f78..bd1a17161 100644 --- a/matita/matita/lib/arithmetics/ord.ma +++ b/matita/matita/lib/arithmetics/ord.ma @@ -13,10 +13,6 @@ include "arithmetics/exp.ma". include "basics/types.ma". include "arithmetics/primes.ma". include "arithmetics/gcd.ma". -(* -include "arithmetics/nth_prime.ma". -(* for some properties of divides *) -*) let rec p_ord_aux p n m ≝ match n \mod m with @@ -54,8 +50,7 @@ qed. lemma p_ord_degenerate: ∀p,n. p_ord_aux p n 1 = 〈p,n〉. #p elim p // #p1 #Hind #n cut (mod n 1 = 0) [@divides_to_mod_O //] #Hmod ->(p_ord_aux_Strue … (Hind … ) ) // >(div_mod n 1) in ⊢ (???%); ->Hmod (p_ord_aux_Strue … (Hind … ) ) // >(div_mod n 1) in ⊢ (???%); // qed. theorem p_ord_aux_to_exp: ∀p,n,m,q,r. O < m → @@ -170,7 +165,7 @@ elim (p_ord_to_exp1 ???? Hp1 posb pordb) -posb -pordb #Hdivb #Hb [@lt_to_le // |% #Hdiv cases (divides_times_to_divides ? ? ? Hprime Hdiv) #Habs @absurd /2/ - |>Ha >Hb -Ha -Hb Ha >Hb -Ha -Hb // ] qed. @@ -221,7 +216,7 @@ cases (p_ord_to_exp1 ? ? ? ? Hposp posm ordm) #divm #eqm % >commutative_gcd @eq_gcd_times_1 [@lt_O_exp @lt_to_le // |@lt_to_le // - |>commutative_gcd // + |/2/ |>commutative_gcd @prime_to_gcd_1 // ] ] diff --git a/matita/matita/lib/arithmetics/sqrt.ma b/matita/matita/lib/arithmetics/sqrt.ma index 7bb9282f0..eb243605c 100644 --- a/matita/matita/lib/arithmetics/sqrt.ma +++ b/matita/matita/lib/arithmetics/sqrt.ma @@ -84,7 +84,7 @@ lemma le_sqrt_n1: ∀n. n - 2*sqrt n ≤ exp (sqrt n) 2. #n @le_plus_to_minus @le_S_S_to_le cut (S ((sqrt n)\sup 2+2*sqrt n) = (exp (S(sqrt n)) 2)) [2:#Hcut >Hcut @lt_sqrt] ->exp_2 >exp_2 generalize in match (sqrt n); #a +>exp_2 >exp_2 generalize in match (sqrt n); #a normalize // qed. @@ -146,6 +146,70 @@ lemma le_sqrt_log_n : ∀n,b. 2 < b → sqrt n * log b n ≤ n. @monotonic_le_times_r @le_sqrt_log // qed. +theorem le_square_exp:∀n. 3 < n → exp n 2 ≤ exp 2 n. +#n #lt3n elim lt3n + [@le_n + |#m #le4m #Hind normalize commutative_times + normalize <(commutative_times 2) normalize commutative_plus >plus_n_Sm @le_plus + [commutative_times normalize + (plus_n_O (S(m1+m1))) >plus_n_Sm >plus_n_Sm + @le_plus [@Hind1 |>(exp_n_1 2) in ⊢ (?%?); @le_exp + [@lt_O_S |@(transitive_le … lem1) @leb_true_to_le //] + ] + ] + ] +qed. + +lemma le_log2_sqrt: ∀n. 2^4 ≤ n→ log 2 n ≤ sqrt n. +#n #le_n >sqrt_def +@true_to_le_max + [@le_S_S @le_log_n_n // + |@le_to_leb_true + cut (0commutative_times normalize // +qed. + +theorem le_squareS_exp:∀n. 5 < n → exp (S n) 2 ≤ exp 2 n. +#n #lt4n elim lt4n + [@leb_true_to_le // + |#m #le4m #Hind >square_S whd in ⊢(??%); >commutative_times in ⊢(??%); + normalize in ⊢(??%); associative_plus @le_plus [@Hind] + elim le4m [@leb_true_to_le //] #a #lea #Hinda + @(transitive_le ? (2*(2*(S a)+1))) + [@lt_to_le whd >plus_n_Sm >(times_n_1 2) in ⊢ (?(??%)?); + commutative_times in ⊢(??%); @monotonic_le_times_r @Hinda + ] + ] +qed. + + +lemma lt_log2_sqrt: ∀n. 2^6 ≤ n→ log 2 n < sqrt n. +#n #le_n >sqrt_def +cut (0sqrt_def @true_to_le_max -- 2.39.2