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/minimization.ma".
14 include "arithmetics/div_and_mod.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 axiom daemon : ∀P:Prop.P.
72 theorem lt_exp_log: ∀p,n. 1 < p → n < exp p (S (log p n)).
74 [normalize <plus_n_O @lt_to_le //
75 |#m @not_le_to_lt @leb_false_to_not_le
76 @(lt_max_to_false ? (S(S m)) (S (log p (S m))))
77 [@le_S_S @lt_log_n_n //
83 theorem log_times1: ∀p,n,m. 1 < p → O < n → O < m →
84 log p (n*m) ≤ S(log p n+log p m).
85 #p #n #m #lt1p #posn #posm
86 whd in ⊢ (?(%??)?); @f_false_to_le_max
88 [>(times_n_O 0) in ⊢ (?%%); @lt_times //
89 |@le_to_leb_true normalize >(times_n_O 0) in ⊢ (?%%); @lt_times //
91 |#i #Hm @lt_to_leb_false
92 @(lt_to_le_to_lt ? ((exp p (S(log p n)))*(exp p (S(log p m)))))
93 [@lt_times @lt_exp_log //
94 |<exp_plus_times @le_exp [@lt_to_le //]
95 normalize <plus_n_Sm //
100 theorem log_times: ∀p,n,m. 1 < p →
101 log p (n*m) ≤ S(log p n+log p m).
102 #p #n #m #lt1p cases n // -n #n cases m
103 [<times_n_O @le_O_n |-m #m @log_times1 //]
106 theorem log_times_l: ∀p,n,m.O < n → O < m → 1 < p →
107 log p n+log p m ≤ log p (n*m).
108 #p #n #m #posn #posm #lt1p whd in ⊢ (??(%??));
111 [>(log_SO … lt1p) >commutative_times <times_n_1 @lt_log_n_n //
112 |-n #n #posn cases posm
113 [>(log_SO … lt1p) < plus_n_O <times_n_1 @lt_log_n_n //
114 |#m1 #lem1 @(transitive_le ? (S n + S m1))
115 [@le_S_S @le_plus // @le_S_S_to_le @lt_log_n_n //
116 |@le_S_S >commutative_plus normalize >plus_n_Sm
117 @monotonic_le_plus_r >(times_n_1 n) in ⊢ (?%?);
118 @monotonic_lt_times_r // @le_S_S //
122 |@le_to_leb_true >exp_plus_times @le_times @le_exp_log //
126 theorem log_exp: ∀p,n,m. 1 < p → O < m →
127 log p ((exp p n)*m)=n+log p m.
128 #p #n #m #lt1p #posm whd in ⊢ (??(%??)?);
131 [<(exp_n_O p) >commutative_times <times_n_1
133 |#a #Hind whd in ⊢ (?%?);
134 @(lt_to_le_to_lt ? (S((p^a) *m))) [@le_S_S @Hind]
135 whd in match (exp ? (S a)); >(commutative_times ? p)
136 >associative_times >(times_n_1 (p^a * m)) in ⊢ (?%?);
137 >commutative_times in ⊢ (?%?); @monotonic_lt_times_l //
138 >(times_n_O 0) @lt_times // @lt_O_exp @lt_to_le //
140 |@le_to_leb_true >exp_plus_times
141 @monotonic_le_times_r @le_exp_log //
142 |#i #Hi #Hm @lt_to_leb_false
143 @(lt_to_le_to_lt ? ((exp p n)*(exp p (S(log p m)))))
144 [@monotonic_lt_times_r [@lt_O_exp @lt_to_le // |@lt_exp_log //]
145 |<exp_plus_times @le_exp [@lt_to_le // |<plus_n_Sm //]
150 theorem eq_log_exp: ∀p,n. 1< p →
152 #p #n #lt1p >(times_n_1 (p^n)) in ⊢ (??(??%)?); >log_exp // >log_SO //
155 theorem log_exp1: ∀p,n,m. 1 < p →
156 log p (exp n m) ≤ m*S(log p n).
157 #p #n #m #lt1p elim m // -m #m #Hind
158 @(transitive_le ? (S (log p n+log p (n\sup m))))
159 [whd in match (exp ??); >commutative_times @log_times //
160 |@le_S_S @monotonic_le_plus_r //
164 theorem log_exp2: ∀p,n,m. 1 < p → 0 < n →
165 m*(log p n) ≤ log p (exp n m).
166 #p #n #m #ltp1 #posn @le_S_S_to_le @(lt_exp_to_lt p)
168 |>commutative_times <exp_exp_times @(le_to_lt_to_lt ? (exp n m))
169 [elim m // -m #m #Hind whd in match (exp ??); @le_times // @le_exp_log //
175 lemma le_log_S: ∀p,n.1 < p →
176 log p n ≤ log p (S n).
177 #p #n #lt1p normalize cases (leb (exp p n) (S n)) normalize //
178 @le_max_f_max_g #i #ltin #H @le_to_leb_true @le_S @leb_true_to_le //
181 theorem le_log: ∀p,n,m. 1 < p → n ≤ m →
183 #p #n #m #lt1p #lenm elim lenm // -m #m #lenm #Hind
184 @(transitive_le … Hind) @le_log_S //
187 theorem log_div: ∀p,n,m. 1 < p → O < m → m ≤ n →
188 log p (n/m) ≤ log p n -log p m.
189 #p #n #m #lt1p #posn #lemn
190 @le_plus_to_minus_r @(transitive_le ? (log p ((n/m)*m)))
191 [@log_times_l // @le_times_to_le_div //
196 theorem log_n_n: ∀n. 1 < n → log n n = 1.
197 #n #lt1n >(exp_n_1 n) in ⊢ (??(??%)?);
198 >(times_n_1 (n^1)) in ⊢ (??(??%)?); >log_exp //
201 theorem log_i_2n: ∀n,i. 1 < n → n < i → i ≤ 2*n →
203 #n #i #lt1n #ltni #lei
204 cut (∀a,b. a≤b → b≤a → a=b)
205 [#a #b #leab #leba cases (le_to_or_lt_eq … leab)
206 [#ltab @False_ind @(absurd ? ltab) @le_to_not_lt // | //]] #Hcut
209 @(absurd ?? (lt_to_not_le (2 * n) (exp i 2) ?))
210 [@(transitive_le ? (exp i (log i (2*n))))
211 [@le_exp // @(ltn_to_ltO ? ? ltni)
212 |@le_exp_log >(times_n_O O) in ⊢ (?%?); @lt_times // @lt_to_le //
214 |>exp_2 @lt_times @(le_to_lt_to_lt ? n) //
216 |@(transitive_le ? (log i i))
217 [<(log_n_n i) in ⊢ (?%?); // @(transitive_lt … lt1n) //
218 |@le_log // @(transitive_lt … lt1n) //
223 theorem exp_n_O: ∀n. O < n → exp O n = O.
224 #n #posn @(lt_O_n_elim ? posn) normalize //