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/log.ma".
15 λn.max (S n) (λx.leb (x*x) n).
17 lemma sqrt_def : ∀n.sqrt n = max (S n) (λx.leb (x*x) n).
20 theorem eq_sqrt: ∀n. sqrt (n*n) = n.
21 #n >sqrt_def @max_spec_to_max %
23 |@le_to_leb_true @le_n
24 |#i #ltin #li @lt_to_leb_false @lt_times //
28 theorem le_sqrt_to_le_times_l : ∀m,n.n ≤ sqrt m → n*n ≤ m.
29 #m #n #len @(transitive_le ? (sqrt m * sqrt m))
31 |@leb_true_to_le @(f_max_true (λx:nat.leb (x*x) m) (S m))
36 theorem lt_sqrt_to_lt_times_l : ∀m,n.
38 #m #n #ltn @(transitive_le ? (sqrt m * sqrt m))
39 [@(transitive_le ? (S n * S n))
40 [@le_S_S // |@le_times //]
41 |@le_sqrt_to_le_times_l @le_n]
44 theorem lt_sqrt_to_lt_times_r : ∀m,n.sqrt m < n → m < n*n.
45 #m #n #ltmn @not_le_to_lt % #H1
46 lapply (lt_max_to_false (\lambda x.leb (x*x) m) (S m) n ? ltmn)
47 [@le_S_S @(transitive_le … H1) //
48 |>(le_to_leb_true … H1) #H destruct (H)
52 lemma leq_sqrt_n : ∀n. sqrt n * sqrt n ≤ n.
53 #n @le_sqrt_to_le_times_l //
56 lemma le_sqrt_n : ∀n.sqrt n ≤ n.
57 #n @(transitive_le … (leq_sqrt_n n)) //
60 lemma lt_sqrt_n : ∀n.1 < n → sqrt n < n.
61 #n #lt1n cases (le_to_or_lt_eq ? ? (le_sqrt_n n)) #Hcase
63 |@False_ind @(absurd ?? (le_to_not_lt ? ? (leq_sqrt_n n)))
64 >Hcase >Hcase >(times_n_1 n) in ⊢ (?%?); @monotonic_lt_times_r
68 lemma lt_sqrt: ∀n.n < (S (sqrt n))^2.
73 |#n2 @not_le_to_lt @leb_false_to_not_le >exp_2
74 @(lt_max_to_false (λx.(leb (x*x) (S(S n2)))) (S(S(S n2))))
75 [@le_S_S @lt_sqrt_n @le_S_S @lt_O_S
83 lemma le_sqrt_n1: ∀n. n - 2*sqrt n ≤ exp (sqrt n) 2.
84 #n @le_plus_to_minus @le_S_S_to_le
85 cut (S ((sqrt n)\sup 2+2*sqrt n) = (exp (S(sqrt n)) 2))
86 [2:#Hcut >Hcut @lt_sqrt]
87 >exp_2 >exp_2 generalize in match (sqrt n); #a
91 (* falso per n=2, m=7 e n=3, m =15
92 a technical lemma used in Bertrand *)
93 lemma le_sqrt_nl: ∀n,m. 3 < n →
94 m*(pred m)*n ≤ exp (sqrt ((exp m 2)*n)) 2.
95 #n #m #lt3n >(minus_n_O m) in ⊢ (? (? (? ? (? %)) ?) ?);
96 <eq_minus_S_pred >distributive_times_minus <times_n_1
97 >commutative_times >distributive_times_minus
99 @(transitive_le ? (m*m*n -2*sqrt(m*m*n)))
100 [@monotonic_le_minus_r
101 @(le_exp_to_le1 ?? 2 (lt_O_S ?))
102 <times_exp @(transitive_le ? ((exp 2 2)*(m*m*n)))
103 [@monotonic_le_times_r >exp_2 @leq_sqrt_n
104 |<exp_2 <times_exp <associative_times
105 <commutative_times in ⊢ (?(?%?)?);
106 >associative_times >commutative_times
107 @le_times [2://] >exp_2 in ⊢ (??%); @le_times //
113 lemma le_sqrt_log: ∀n,b. 2 < b → log b n ≤ sqrt n.
114 #n #b #lt2b >sqrt_def
116 [@le_S_S @le_log_n_n @lt_to_le //
117 |@le_to_leb_true cases (le_to_or_lt_eq ? ? (le_O_n n)) #Hn
118 [@(transitive_le … (le_exp_log b n Hn))
121 |#n1 #Hind normalize in ⊢ (??%);
122 cases(le_to_or_lt_eq ?? (le_O_n n1)) #H0
123 [cases(le_to_or_lt_eq ? ? H0) #H1
124 [@(transitive_le ? (3*(n1*n1)))
125 [normalize in ⊢ (?%?); >commutative_times in ⊢ (?%?);
127 cut (S (n1+(S n1*n1)) = n1*n1 + ((S n1) + n1))
128 [normalize >commutative_plus in ⊢ (???%); normalize //] #Hcut
129 >Hcut @monotonic_le_plus_r normalize in ⊢ (??%); <plus_n_O @le_plus
130 [>(times_n_1 n1) in ⊢ (?%?); @monotonic_lt_times_r // |//]
131 |>commutative_times @le_times //
133 |<H1 normalize <plus_n_O
134 cut (4 = 2*2) [//] #H4 >H4 @lt_to_le @lt_times //
136 |<H0 normalize <plus_n_O @(transitive_le … lt2b) @leb_true_to_le //
144 lemma le_sqrt_log_n : ∀n,b. 2 < b → sqrt n * log b n ≤ n.
145 #n #b #lt2b @(transitive_le … (leq_sqrt_n ?))
146 @monotonic_le_times_r @le_sqrt_log //
149 theorem le_square_exp:∀n. 3 < n → exp n 2 ≤ exp 2 n.
152 |#m #le4m #Hind normalize <plus_n_O >commutative_times
153 normalize <(commutative_times 2) normalize <associative_plus
154 <plus_n_O >commutative_plus >plus_n_Sm @le_plus
156 |elim le4m [@leb_true_to_le //]
157 #m1 #lem1 #Hind1 normalize >commutative_times normalize
158 <plus_n_O <plus_n_Sm >(plus_n_O (S(m1+m1))) >plus_n_Sm >plus_n_Sm
159 @le_plus [@Hind1 |>(exp_n_1 2) in ⊢ (?%?); @le_exp
160 [@lt_O_S |@(transitive_le … lem1) @leb_true_to_le //]
166 lemma le_log2_sqrt: ∀n. 2^4 ≤ n→ log 2 n ≤ sqrt n.
169 [@le_S_S @le_log_n_n //
171 cut (0<n) [@(transitive_lt … le_n) @lt_O_S] #posn
172 @(transitive_le … (le_exp_log 2 n posn))
173 <exp_2 @le_square_exp @true_to_le_max
174 [@(lt_to_le_to_lt … le_n) @leb_true_to_le // |@le_to_leb_true //]
178 lemma square_S: ∀a. (S a)^2 = a^2 + 2*a +1.
179 #a normalize >commutative_times normalize //
182 theorem le_squareS_exp:∀n. 5 < n → exp (S n) 2 ≤ exp 2 n.
185 |#m #le4m #Hind >square_S whd in ⊢(??%); >commutative_times in ⊢(??%);
186 normalize in ⊢(??%); <plus_n_O >associative_plus @le_plus [@Hind]
187 elim le4m [@leb_true_to_le //] #a #lea #Hinda
188 @(transitive_le ? (2*(2*(S a)+1)))
189 [@lt_to_le whd >plus_n_Sm >(times_n_1 2) in ⊢ (?(??%)?);
190 <distributive_times_plus @monotonic_le_times_r @le_plus [2://]
192 |whd in ⊢ (??%); >commutative_times in ⊢(??%); @monotonic_le_times_r @Hinda
198 lemma lt_log2_sqrt: ∀n. 2^6 ≤ n→ log 2 n < sqrt n.
200 cut (0<n) [@(transitive_lt … le_n) @lt_O_S] #posn
202 [@le_S_S @lt_log_n_n //
204 cut (0<n) [@(transitive_lt … le_n) @lt_O_S] #posn
205 @(transitive_le … (le_exp_log 2 n posn))
206 <exp_2 @le_squareS_exp @true_to_le_max
207 [@(lt_to_le_to_lt … le_n) @leb_true_to_le //
214 theorem monotonic_sqrt: monotonic nat le sqrt.
215 #n #m #lenm >sqrt_def @true_to_le_max
216 [@le_S_S @(transitive_le … lenm) @le_sqrt_n
217 |@le_to_leb_true @(transitive_le … lenm) @leq_sqrt_n