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/exp.ma".
13 include "arithmetics/div_and_mod.ma".
14 include "arithmetics/minimization.ma".
16 definition log ≝ λp,n.
17 max n (λx.leb (exp p x) n).
19 lemma tech_log : ∀p,n. 1<p → 0 < n →
20 log p n = max (S n) (λx.leb (exp p x) n).
21 #p #n #lt1p #posn whd in ⊢ (???%);
22 cut (leb (exp p n) n = false)
23 [@not_le_to_leb_false @lt_to_not_le /2/
28 theorem le_exp_log: ∀p,n. O < n →
30 #a #n #posn @leb_true_to_le
31 (* whd in match (log ??); *)
32 @(f_max_true (λx.leb (exp a x) n)) %{0} % //
36 theorem log_SO: ∀n. 1 < n → log n 1 = O.
37 #n #lt1n @sym_eq @le_n_O_to_eq @(le_exp_to_le n) //
40 theorem lt_to_log_O: ∀n,m. O < m → m < n → log n m = O.
41 #n #m #posm #ltnm @sym_eq @le_n_O_to_eq @le_S_S_to_le @(lt_exp_to_lt n)
42 [@(le_to_lt_to_lt ? m) //
43 |normalize in ⊢ (??%); <plus_n_O @(le_to_lt_to_lt ? m) //
48 theorem lt_log_n_n: ∀p, n. 1 < p → O < n → log p n < n.
51 [whd in match (log ??); @le_max_n
52 |#Hcut elim (le_to_or_lt_eq ? ? Hcut) //
53 #Hn @False_ind @(absurd … (exp p n ≤ n))
54 [<Hn in ⊢ (?(??%)?); @le_exp_log //
55 |@lt_to_not_le @lt_m_exp_nm //
60 theorem lt_O_log: ∀p, n. 1 < n → p ≤ n → O < log p n.
61 #p #n #lt1p #lepn whd in match (log ??);
62 @not_lt_to_le % #H lapply (lt_max_to_false ??? lt1p H)
63 <exp_n_1 >(le_to_leb_true … lepn) #H destruct
66 theorem le_log_n_n: ∀p,n. 1 < p → log p n ≤ n.
67 #p #n #lt1p cases n [@le_n |#m @lt_to_le @lt_log_n_n //]
70 theorem lt_exp_log: ∀p,n. 1 < p → n < exp p (S (log p n)).
72 [normalize <plus_n_O @lt_to_le //
73 |#m @not_le_to_lt @leb_false_to_not_le
74 @(lt_max_to_false ? (S(S m)) (S (log p (S m))))
75 [@le_S_S @lt_log_n_n //
81 theorem log_times1: ∀p,n,m. 1 < p → O < n → O < m →
82 log p (n*m) ≤ S(log p n+log p m).
83 #p #n #m #lt1p #posn #posm
84 whd in ⊢ (?(%??)?); @f_false_to_le_max
86 [>(times_n_O 0) in ⊢ (?%%); @lt_times //
87 |@le_to_leb_true normalize >(times_n_O 0) in ⊢ (?%%); @lt_times //
89 |#i #Hm @lt_to_leb_false
90 @(lt_to_le_to_lt ? ((exp p (S(log p n)))*(exp p (S(log p m)))))
91 [@lt_times @lt_exp_log //
92 |<exp_plus_times @le_exp [@lt_to_le //]
93 normalize <plus_n_Sm //
98 theorem log_times: ∀p,n,m. 1 < p →
99 log p (n*m) ≤ S(log p n+log p m).
100 #p #n #m #lt1p cases n // -n #n cases m
101 [<times_n_O @le_O_n |-m #m @log_times1 //]
104 theorem log_times_l: ∀p,n,m.O < n → O < m → 1 < p →
105 log p n+log p m ≤ log p (n*m).
106 #p #n #m #posn #posm #lt1p whd in ⊢ (??(%??));
109 [>(log_SO … lt1p) >commutative_times <times_n_1 @lt_log_n_n //
110 |-n #n #posn cases posm
111 [>(log_SO … lt1p) < plus_n_O <times_n_1 @lt_log_n_n //
112 |#m1 #lem1 @(transitive_le ? (S n + S m1))
113 [@le_S_S @le_plus // @le_S_S_to_le @lt_log_n_n //
114 |@le_S_S >commutative_plus normalize >plus_n_Sm
115 @monotonic_le_plus_r >(times_n_1 n) in ⊢ (?%?);
116 @monotonic_lt_times_r // @le_S_S //
120 |@le_to_leb_true >exp_plus_times @le_times @le_exp_log //
124 theorem log_exp: ∀p,n,m. 1 < p → O < m →
125 log p ((exp p n)*m)=n+log p m.
126 #p #n #m #lt1p #posm whd in ⊢ (??(%??)?);
129 [<(exp_n_O p) >commutative_times <times_n_1
131 |#a #Hind whd in ⊢ (?%?);
132 @(lt_to_le_to_lt ? (S((p^a) *m))) [@le_S_S @Hind]
133 whd in match (exp ? (S a)); >(commutative_times ? p)
134 >associative_times >(times_n_1 (p^a * m)) in ⊢ (?%?);
135 >commutative_times in ⊢ (?%?); @monotonic_lt_times_l //
136 >(times_n_O 0) @lt_times // @lt_O_exp @lt_to_le //
138 |@le_to_leb_true >exp_plus_times
139 @monotonic_le_times_r @le_exp_log //
140 |#i #Hi #Hm @lt_to_leb_false
141 @(lt_to_le_to_lt ? ((exp p n)*(exp p (S(log p m)))))
142 [@monotonic_lt_times_r [@lt_O_exp @lt_to_le // |@lt_exp_log //]
143 |<exp_plus_times @le_exp [@lt_to_le // | //]
148 theorem eq_log_exp: ∀p,n. 1< p →
150 #p #n #lt1p >(times_n_1 (p^n)) in ⊢ (??(??%)?); >log_exp // >log_SO //
153 theorem log_exp1: ∀p,n,m. 1 < p →
154 log p (exp n m) ≤ m*S(log p n).
155 #p #n #m #lt1p elim m // -m #m #Hind
156 @(transitive_le ? (S (log p n+log p (n\sup m))))
157 [whd in match (exp ??); >commutative_times @log_times //
158 |@le_S_S @monotonic_le_plus_r //
162 theorem log_exp2: ∀p,n,m. 1 < p → 0 < n →
163 m*(log p n) ≤ log p (exp n m).
164 #p #n #m #ltp1 #posn @le_S_S_to_le @(lt_exp_to_lt p)
166 |>commutative_times <exp_exp_times @(le_to_lt_to_lt ? (exp n m))
167 [elim m // -m #m #Hind whd in match (exp ??); @le_times // @le_exp_log //
173 lemma le_log_S: ∀p,n.1 < p →
174 log p n ≤ log p (S n).
175 #p #n #lt1p normalize cases (leb (exp p n) (S n)) normalize //
176 @le_max_f_max_g #i #ltin #H @le_to_leb_true @le_S @leb_true_to_le //
179 theorem le_log: ∀p,n,m. 1 < p → n ≤ m →
181 #p #n #m #lt1p #lenm elim lenm // -m #m #lenm #Hind
182 @(transitive_le … Hind) @le_log_S //
185 theorem log_div: ∀p,n,m. 1 < p → O < m → m ≤ n →
186 log p (n/m) ≤ log p n -log p m.
187 #p #n #m #lt1p #posn #lemn
188 @le_plus_to_minus_r @(transitive_le ? (log p ((n/m)*m)))
189 [@log_times_l // @le_times_to_le_div //
194 theorem log_n_n: ∀n. 1 < n → log n n = 1.
195 #n #lt1n >(exp_n_1 n) in ⊢ (??(??%)?);
196 >(times_n_1 (n^1)) in ⊢ (??(??%)?); >log_exp //
199 theorem log_i_2n: ∀n,i. 1 < n → n < i → i ≤ 2*n →
201 #n #i #lt1n #ltni #lei
202 cut (∀a,b. a≤b → b≤a → a=b)
203 [#a #b #leab #leba cases (le_to_or_lt_eq … leab)
204 [#ltab @False_ind @(absurd ? ltab) @le_to_not_lt // | //]] #Hcut
207 @(absurd ?? (lt_to_not_le (2 * n) (exp i 2) ?))
208 [@(transitive_le ? (exp i (log i (2*n))))
209 [@le_exp // @(ltn_to_ltO ? ? ltni)
210 |@le_exp_log >(times_n_O O) in ⊢ (?%?); @lt_times // @lt_to_le //
212 |>exp_2 @lt_times @(le_to_lt_to_lt ? n) //
214 |@(transitive_le ? (log i i))
215 [<(log_n_n i) in ⊢ (?%?); // @(transitive_lt … lt1n) //
216 |@le_log // @(transitive_lt … lt1n) //
221 theorem exp_n_O: ∀n. O < n → exp O n = O.
222 #n #posn @(lt_O_n_elim ? posn) normalize //