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 //
150 theorem monotonic_sqrt: monotonic nat le sqrt.
151 #n #m #lenm >sqrt_def @true_to_le_max
152 [@le_S_S @(transitive_le … lenm) @le_sqrt_n
153 |@le_to_leb_true @(transitive_le … lenm) @leq_sqrt_n