qed.
lemma plus_minus1: ∀a,b,c. c ≤ b → a + (b -c) = a + b -c.
-#a #b #c #lecb @sym_eq @plus_to_minus >(commutative_plus c)
+#a #b #c #lecb @sym_eq @plus_to_minus >(commutative_plus c)
>associative_plus <plus_minus_m_m //
qed.
]
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. *)
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.
]
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 <times_pi
+theorem eq_Bk_B1_B2: ∀n.
+ Bk n = B1 n * B2 n.
+#n >Bk_def >B1_def >B2_def <times_pi
@same_bigop
[//
|#p #ltp #primebp cases (true_or_false (leb (k n p) 1)) #Hc >Hc
]
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 //
]
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}
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.
]
qed.
-theorem le_to_bertrand2:
+theorem bertrand_up:
∀n. 2^8 ≤ n → bertrand n.
#n #len @not_not_bertrand_to_bertrand % #notBn
@(absurd (2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n))))
#n @lprim_invariant //
qed.
-let rec checker l ≝
- match l with
- [ nil ⇒ true
- | cons h1 t1 => 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 //
]
|<Hp1 >(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 //|//]|//]
]
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_Sm @le_S_S <plus_n_Sm <plus_n_O @lep]
- |#p #memp #lt2p @(check_list_spec (tail ? (list_of_primes it)) 2 (list_of_primes it))
+ |>(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] *
|#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.
-*)
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_sigma @le_Al1
+theorem le_Psil: ∀n. Psi n ≤ exp n (prim n).
+#n <exp_sigma @le_Psil1
qed.
-theorem leA_r2: ∀n.
- exp n (prim n) ≤ A n * A n.
+theorem lePsi_r2: ∀n.
+ exp n (prim n) ≤ Psi n * Psi n.
#n elim (le_to_or_lt_eq ?? (le_O_n n)) #Hn
[<(exp_sigma (S n) n primeb) <times_pi
@le_pi #i #lti #primei
qed.
(* an equivalent formulation for psi *)
-definition A': nat → nat ≝
+definition Psi': nat → nat ≝
λn. ∏_{p < S n | primeb p} (∏_{i < log p n} p).
-lemma Adef: ∀n. A' n = ∏_{p < S n | primeb p} (∏_{i < log p n} p).
+lemma Psidef: ∀n. Psi' n = ∏_{p < S n | primeb p} (∏_{i < log p n} p).
// qed-.
-theorem eq_A_A': ∀n.A n = A' n.
+theorem eq_Psi_Psi': ∀n.Psi n = Psi' n.
#n @same_bigop // #i #lti #primebi
@(trans_eq ? ? (exp i (∑_{x < log i n} 1)))
[@eq_f @sym_eq @sigma_const
#n #posn <eq_pi_p_primeb_divides_b @pi_p_primeb_dividesb //
qed.
+(* more result on order functions *)
theorem le_ord_log: ∀n,p. O < n → 1 < p →
ord n p ≤ log p n.
#n #p #posn #lt1p >(exp_ord p ? lt1p posn) in ⊢ (??(??%));
|#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 //]
- |<exp_plus_times @le_exp [@lt_to_le // |<plus_n_Sm //]
+ |<exp_plus_times @le_exp [@lt_to_le // | //]
]
]
qed.
max n f = max n g.
#f #g #n (elim n) //
#m #Hind #ext normalize >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) →
#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.
]
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;
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) →
#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.
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
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 <plus_n_O <times_n_1 //
+>(p_ord_aux_Strue … (Hind … ) ) // >(div_mod n 1) in ⊢ (???%); //
qed.
theorem p_ord_aux_to_exp: ∀p,n,m,q,r. O < m →
[@lt_to_le //
|% #Hdiv cases (divides_times_to_divides ? ? ? Hprime Hdiv)
#Habs @absurd /2/
- |>Ha >Hb -Ha -Hb <associative_times <associative_times //
+ |>Ha >Hb -Ha -Hb //
]
qed.
>commutative_gcd @eq_gcd_times_1
[@lt_O_exp @lt_to_le //
|@lt_to_le //
- |>commutative_gcd //
+ |/2/
|>commutative_gcd @prime_to_gcd_1 //
]
]
#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.
@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 <plus_n_O >commutative_times
+ normalize <(commutative_times 2) normalize <associative_plus
+ <plus_n_O >commutative_plus >plus_n_Sm @le_plus
+ [<exp_2 @Hind
+ |elim le4m [@leb_true_to_le //]
+ #m1 #lem1 #Hind1 normalize >commutative_times normalize
+ <plus_n_O <plus_n_Sm >(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 (0<n) [@(transitive_lt … le_n) @lt_O_S] #posn
+ @(transitive_le … (le_exp_log 2 n posn))
+ <exp_2 @le_square_exp @true_to_le_max
+ [@(lt_to_le_to_lt … le_n) @leb_true_to_le // |@le_to_leb_true //]
+ ]
+qed.
+
+lemma square_S: ∀a. (S a)^2 = a^2 + 2*a +1.
+#a normalize >commutative_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 ⊢(??%); <plus_n_O >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 ⊢ (?(??%)?);
+ <distributive_times_plus @monotonic_le_times_r @le_plus [2://]
+ normalize //
+ |whd 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 (0<n) [@(transitive_lt … le_n) @lt_O_S] #posn
+@true_to_le_max
+ [@le_S_S @lt_log_n_n //
+ |@le_to_leb_true
+ cut (0<n) [@(transitive_lt … le_n) @lt_O_S] #posn
+ @(transitive_le … (le_exp_log 2 n posn))
+ <exp_2 @le_squareS_exp @true_to_le_max
+ [@(lt_to_le_to_lt … le_n) @leb_true_to_le //
+ |@le_to_leb_true //
+ ]
+ ]
+qed.
+
(* monotonicity *)
theorem monotonic_sqrt: monotonic nat le sqrt.
#n #m #lenm >sqrt_def @true_to_le_max
projects / helm.git / commitdiff