author  huffman 
Fri, 19 Aug 2011 07:45:22 0700  
changeset 44305  3bdc02eb1637 
parent 44289  d81d09cdab9c 
child 47242  1caeecc72aea 
permissions  rwrr 
41959  1 
(* Title: HOL/Ln.thy 
16959  2 
Author: Jeremy Avigad 
3 
*) 

4 

5 
header {* Properties of ln *} 

6 

7 
theory Ln 

8 
imports Transcendental 

9 
begin 

10 

11 
lemma exp_first_two_terms: "exp x = 1 + x + suminf (%n. 

40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

12 
inverse(fact (n+2)) * (x ^ (n+2)))" 
16959  13 
proof  
40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

14 
have "exp x = suminf (%n. inverse(fact n) * (x ^ n))" 
19765  15 
by (simp add: exp_def) 
40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

16 
also from summable_exp have "... = (SUM n::nat : {0..<2}. 
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

17 
inverse(fact n) * (x ^ n)) + suminf (%n. 
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

18 
inverse(fact(n+2)) * (x ^ (n+2)))" (is "_ = ?a + _") 
16959  19 
by (rule suminf_split_initial_segment) 
20 
also have "?a = 1 + x" 

44289  21 
by (simp add: numeral_2_eq_2) 
16959  22 
finally show ?thesis . 
23 
qed 

24 

25 
lemma exp_tail_after_first_two_terms_summable: 

40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

26 
"summable (%n. inverse(fact (n+2)) * (x ^ (n+2)))" 
16959  27 
proof  
28 
note summable_exp 

29 
thus ?thesis 

30 
by (frule summable_ignore_initial_segment) 

31 
qed 

32 

33 
lemma aux1: assumes a: "0 <= x" and b: "x <= 1" 

40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

34 
shows "inverse (fact ((n::nat) + 2)) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)" 
16959  35 
proof (induct n) 
40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

36 
show "inverse (fact ((0::nat) + 2)) * x ^ (0 + 2) <= 
16959  37 
x ^ 2 / 2 * (1 / 2) ^ 0" 
23482  38 
by (simp add: real_of_nat_Suc power2_eq_square) 
16959  39 
next 
32038  40 
fix n :: nat 
40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

41 
assume c: "inverse (fact (n + 2)) * x ^ (n + 2) 
16959  42 
<= x ^ 2 / 2 * (1 / 2) ^ n" 
40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

43 
show "inverse (fact (Suc n + 2)) * x ^ (Suc n + 2) 
16959  44 
<= x ^ 2 / 2 * (1 / 2) ^ Suc n" 
45 
proof  

40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

46 
have "inverse(fact (Suc n + 2)) <= (1/2) * inverse (fact (n+2))" 
16959  47 
proof  
48 
have "Suc n + 2 = Suc (n + 2)" by simp 

49 
then have "fact (Suc n + 2) = Suc (n + 2) * fact (n + 2)" 

50 
by simp 

51 
then have "real(fact (Suc n + 2)) = real(Suc (n + 2) * fact (n + 2))" 

52 
apply (rule subst) 

53 
apply (rule refl) 

54 
done 

55 
also have "... = real(Suc (n + 2)) * real(fact (n + 2))" 

56 
by (rule real_of_nat_mult) 

57 
finally have "real (fact (Suc n + 2)) = 

58 
real (Suc (n + 2)) * real (fact (n + 2))" . 

40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

59 
then have "inverse(fact (Suc n + 2)) = 
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

60 
inverse(Suc (n + 2)) * inverse(fact (n + 2))" 
16959  61 
apply (rule ssubst) 
62 
apply (rule inverse_mult_distrib) 

63 
done 

40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

64 
also have "... <= (1/2) * inverse(fact (n + 2))" 
16959  65 
apply (rule mult_right_mono) 
66 
apply (subst inverse_eq_divide) 

67 
apply simp 

44305  68 
apply (simp del: fact_Suc) 
16959  69 
done 
70 
finally show ?thesis . 

71 
qed 

72 
moreover have "x ^ (Suc n + 2) <= x ^ (n + 2)" 

44289  73 
by (simp add: mult_left_le_one_le mult_nonneg_nonneg a b) 
40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

74 
ultimately have "inverse (fact (Suc n + 2)) * x ^ (Suc n + 2) <= 
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

75 
(1 / 2 * inverse (fact (n + 2))) * x ^ (n + 2)" 
16959  76 
apply (rule mult_mono) 
77 
apply (rule mult_nonneg_nonneg) 

78 
apply simp 

79 
apply (subst inverse_nonnegative_iff_nonnegative) 

27483
7c58324cd418
use real_of_nat_ge_zero instead of real_of_nat_fact_ge_zero
huffman
parents:
25875
diff
changeset

80 
apply (rule real_of_nat_ge_zero) 
16959  81 
apply (rule zero_le_power) 
23441  82 
apply (rule a) 
16959  83 
done 
40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

84 
also have "... = 1 / 2 * (inverse (fact (n + 2)) * x ^ (n + 2))" 
16959  85 
by simp 
86 
also have "... <= 1 / 2 * (x ^ 2 / 2 * (1 / 2) ^ n)" 

87 
apply (rule mult_left_mono) 

41550  88 
apply (rule c) 
16959  89 
apply simp 
90 
done 

91 
also have "... = x ^ 2 / 2 * (1 / 2 * (1 / 2) ^ n)" 

92 
by auto 

93 
also have "(1::real) / 2 * (1 / 2) ^ n = (1 / 2) ^ (Suc n)" 

30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
29667
diff
changeset

94 
by (rule power_Suc [THEN sym]) 
16959  95 
finally show ?thesis . 
96 
qed 

97 
qed 

98 

20692  99 
lemma aux2: "(%n. (x::real) ^ 2 / 2 * (1 / 2) ^ n) sums x^2" 
16959  100 
proof  
20692  101 
have "(%n. (1 / 2::real)^n) sums (1 / (1  (1/2)))" 
16959  102 
apply (rule geometric_sums) 
22998  103 
by (simp add: abs_less_iff) 
16959  104 
also have "(1::real) / (1  1/2) = 2" 
105 
by simp 

20692  106 
finally have "(%n. (1 / 2::real)^n) sums 2" . 
16959  107 
then have "(%n. x ^ 2 / 2 * (1 / 2) ^ n) sums (x^2 / 2 * 2)" 
108 
by (rule sums_mult) 

109 
also have "x^2 / 2 * 2 = x^2" 

110 
by simp 

111 
finally show ?thesis . 

112 
qed 

113 

23114  114 
lemma exp_bound: "0 <= (x::real) ==> x <= 1 ==> exp x <= 1 + x + x^2" 
16959  115 
proof  
116 
assume a: "0 <= x" 

117 
assume b: "x <= 1" 

40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

118 
have c: "exp x = 1 + x + suminf (%n. inverse(fact (n+2)) * 
16959  119 
(x ^ (n+2)))" 
120 
by (rule exp_first_two_terms) 

40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

121 
moreover have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= x^2" 
16959  122 
proof  
40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

123 
have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= 
16959  124 
suminf (%n. (x^2/2) * ((1/2)^n))" 
125 
apply (rule summable_le) 

41550  126 
apply (auto simp only: aux1 a b) 
16959  127 
apply (rule exp_tail_after_first_two_terms_summable) 
128 
by (rule sums_summable, rule aux2) 

129 
also have "... = x^2" 

130 
by (rule sums_unique [THEN sym], rule aux2) 

131 
finally show ?thesis . 

132 
qed 

133 
ultimately show ?thesis 

134 
by auto 

135 
qed 

136 

23114  137 
lemma aux4: "0 <= (x::real) ==> x <= 1 ==> exp (x  x^2) <= 1 + x" 
16959  138 
proof  
139 
assume a: "0 <= x" and b: "x <= 1" 

140 
have "exp (x  x^2) = exp x / exp (x^2)" 

141 
by (rule exp_diff) 

142 
also have "... <= (1 + x + x^2) / exp (x ^2)" 

143 
apply (rule divide_right_mono) 

144 
apply (rule exp_bound) 

145 
apply (rule a, rule b) 

146 
apply simp 

147 
done 

148 
also have "... <= (1 + x + x^2) / (1 + x^2)" 

149 
apply (rule divide_left_mono) 

17013
74bc935273ea
renamed exp_ge_add_one_self2 to exp_ge_add_one_self
avigad
parents:
16963
diff
changeset

150 
apply (auto simp add: exp_ge_add_one_self_aux) 
16959  151 
apply (rule add_nonneg_nonneg) 
41550  152 
using a apply auto 
16959  153 
apply (rule mult_pos_pos) 
154 
apply auto 

155 
apply (rule add_pos_nonneg) 

156 
apply auto 

157 
done 

158 
also from a have "... <= 1 + x" 

44289  159 
by (simp add: field_simps add_strict_increasing zero_le_mult_iff) 
16959  160 
finally show ?thesis . 
161 
qed 

162 

163 
lemma ln_one_plus_pos_lower_bound: "0 <= x ==> x <= 1 ==> 

164 
x  x^2 <= ln (1 + x)" 

165 
proof  

166 
assume a: "0 <= x" and b: "x <= 1" 

167 
then have "exp (x  x^2) <= 1 + x" 

168 
by (rule aux4) 

169 
also have "... = exp (ln (1 + x))" 

170 
proof  

171 
from a have "0 < 1 + x" by auto 

172 
thus ?thesis 

173 
by (auto simp only: exp_ln_iff [THEN sym]) 

174 
qed 

175 
finally have "exp (x  x ^ 2) <= exp (ln (1 + x))" . 

176 
thus ?thesis by (auto simp only: exp_le_cancel_iff) 

177 
qed 

178 

179 
lemma ln_one_minus_pos_upper_bound: "0 <= x ==> x < 1 ==> ln (1  x) <=  x" 

180 
proof  

181 
assume a: "0 <= (x::real)" and b: "x < 1" 

182 
have "(1  x) * (1 + x + x^2) = (1  x^3)" 

29667  183 
by (simp add: algebra_simps power2_eq_square power3_eq_cube) 
16959  184 
also have "... <= 1" 
25875  185 
by (auto simp add: a) 
16959  186 
finally have "(1  x) * (1 + x + x ^ 2) <= 1" . 
187 
moreover have "0 < 1 + x + x^2" 

188 
apply (rule add_pos_nonneg) 

41550  189 
using a apply auto 
16959  190 
done 
191 
ultimately have "1  x <= 1 / (1 + x + x^2)" 

192 
by (elim mult_imp_le_div_pos) 

193 
also have "... <= 1 / exp x" 

194 
apply (rule divide_left_mono) 

195 
apply (rule exp_bound, rule a) 

41550  196 
using a b apply auto 
16959  197 
apply (rule mult_pos_pos) 
198 
apply (rule add_pos_nonneg) 

199 
apply auto 

200 
done 

201 
also have "... = exp (x)" 

36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
33667
diff
changeset

202 
by (auto simp add: exp_minus divide_inverse) 
16959  203 
finally have "1  x <= exp ( x)" . 
204 
also have "1  x = exp (ln (1  x))" 

205 
proof  

206 
have "0 < 1  x" 

207 
by (insert b, auto) 

208 
thus ?thesis 

209 
by (auto simp only: exp_ln_iff [THEN sym]) 

210 
qed 

211 
finally have "exp (ln (1  x)) <= exp ( x)" . 

212 
thus ?thesis by (auto simp only: exp_le_cancel_iff) 

213 
qed 

214 

215 
lemma aux5: "x < 1 ==> ln(1  x) =  ln(1 + x / (1  x))" 

216 
proof  

217 
assume a: "x < 1" 

218 
have "ln(1  x) =  ln(1 / (1  x))" 

219 
proof  

220 
have "ln(1  x) =  ( ln (1  x))" 

221 
by auto 

222 
also have " ln(1  x) = ln 1  ln(1  x)" 

223 
by simp 

224 
also have "... = ln(1 / (1  x))" 

225 
apply (rule ln_div [THEN sym]) 

226 
by (insert a, auto) 

227 
finally show ?thesis . 

228 
qed 

23482  229 
also have " 1 / (1  x) = 1 + x / (1  x)" using a by(simp add:field_simps) 
16959  230 
finally show ?thesis . 
231 
qed 

232 

233 
lemma ln_one_minus_pos_lower_bound: "0 <= x ==> x <= (1 / 2) ==> 

234 
 x  2 * x^2 <= ln (1  x)" 

235 
proof  

236 
assume a: "0 <= x" and b: "x <= (1 / 2)" 

237 
from b have c: "x < 1" 

238 
by auto 

239 
then have "ln (1  x) =  ln (1 + x / (1  x))" 

240 
by (rule aux5) 

241 
also have " (x / (1  x)) <= ..." 

242 
proof  

243 
have "ln (1 + x / (1  x)) <= x / (1  x)" 

244 
apply (rule ln_add_one_self_le_self) 

245 
apply (rule divide_nonneg_pos) 

246 
by (insert a c, auto) 

247 
thus ?thesis 

248 
by auto 

249 
qed 

250 
also have " (x / (1  x)) = x / (1  x)" 

251 
by auto 

252 
finally have d: " x / (1  x) <= ln (1  x)" . 

41550  253 
have "0 < 1  x" using a b by simp 
23482  254 
hence e: "x  2 * x^2 <=  x / (1  x)" 
41550  255 
using mult_right_le_one_le[of "x*x" "2*x"] a b 
256 
by (simp add:field_simps power2_eq_square) 

16959  257 
from e d show " x  2 * x^2 <= ln (1  x)" 
258 
by (rule order_trans) 

259 
qed 

260 

23114  261 
lemma exp_ge_add_one_self [simp]: "1 + (x::real) <= exp x" 
16959  262 
apply (case_tac "0 <= x") 
17013
74bc935273ea
renamed exp_ge_add_one_self2 to exp_ge_add_one_self
avigad
parents:
16963
diff
changeset

263 
apply (erule exp_ge_add_one_self_aux) 
16959  264 
apply (case_tac "x <= 1") 
265 
apply (subgoal_tac "1 + x <= 0") 

266 
apply (erule order_trans) 

267 
apply simp 

268 
apply simp 

269 
apply (subgoal_tac "1 + x = exp(ln (1 + x))") 

270 
apply (erule ssubst) 

271 
apply (subst exp_le_cancel_iff) 

272 
apply (subgoal_tac "ln (1  ( x)) <=  ( x)") 

273 
apply simp 

274 
apply (rule ln_one_minus_pos_upper_bound) 

275 
apply auto 

276 
done 

277 

278 
lemma ln_add_one_self_le_self2: "1 < x ==> ln(1 + x) <= x" 

279 
apply (subgoal_tac "x = ln (exp x)") 

280 
apply (erule ssubst)back 

281 
apply (subst ln_le_cancel_iff) 

282 
apply auto 

283 
done 

284 

285 
lemma abs_ln_one_plus_x_minus_x_bound_nonneg: 

286 
"0 <= x ==> x <= 1 ==> abs(ln (1 + x)  x) <= x^2" 

287 
proof  

23441  288 
assume x: "0 <= x" 
41550  289 
assume x1: "x <= 1" 
23441  290 
from x have "ln (1 + x) <= x" 
16959  291 
by (rule ln_add_one_self_le_self) 
292 
then have "ln (1 + x)  x <= 0" 

293 
by simp 

294 
then have "abs(ln(1 + x)  x) =  (ln(1 + x)  x)" 

295 
by (rule abs_of_nonpos) 

296 
also have "... = x  ln (1 + x)" 

297 
by simp 

298 
also have "... <= x^2" 

299 
proof  

41550  300 
from x x1 have "x  x^2 <= ln (1 + x)" 
16959  301 
by (intro ln_one_plus_pos_lower_bound) 
302 
thus ?thesis 

303 
by simp 

304 
qed 

305 
finally show ?thesis . 

306 
qed 

307 

308 
lemma abs_ln_one_plus_x_minus_x_bound_nonpos: 

309 
"(1 / 2) <= x ==> x <= 0 ==> abs(ln (1 + x)  x) <= 2 * x^2" 

310 
proof  

41550  311 
assume a: "(1 / 2) <= x" 
312 
assume b: "x <= 0" 

16959  313 
have "abs(ln (1 + x)  x) = x  ln(1  (x))" 
314 
apply (subst abs_of_nonpos) 

315 
apply simp 

316 
apply (rule ln_add_one_self_le_self2) 

41550  317 
using a apply auto 
16959  318 
done 
319 
also have "... <= 2 * x^2" 

320 
apply (subgoal_tac " (x)  2 * (x)^2 <= ln (1  (x))") 

29667  321 
apply (simp add: algebra_simps) 
16959  322 
apply (rule ln_one_minus_pos_lower_bound) 
41550  323 
using a b apply auto 
29667  324 
done 
16959  325 
finally show ?thesis . 
326 
qed 

327 

328 
lemma abs_ln_one_plus_x_minus_x_bound: 

329 
"abs x <= 1 / 2 ==> abs(ln (1 + x)  x) <= 2 * x^2" 

330 
apply (case_tac "0 <= x") 

331 
apply (rule order_trans) 

332 
apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg) 

333 
apply auto 

334 
apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos) 

335 
apply auto 

336 
done 

337 

338 
lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)" 

339 
proof  

41550  340 
assume x: "exp 1 <= x" "x <= y" 
44289  341 
moreover have "0 < exp (1::real)" by simp 
342 
ultimately have a: "0 < x" and b: "0 < y" 

343 
by (fast intro: less_le_trans order_trans)+ 

16959  344 
have "x * ln y  x * ln x = x * (ln y  ln x)" 
29667  345 
by (simp add: algebra_simps) 
16959  346 
also have "... = x * ln(y / x)" 
44289  347 
by (simp only: ln_div a b) 
16959  348 
also have "y / x = (x + (y  x)) / x" 
349 
by simp 

44289  350 
also have "... = 1 + (y  x) / x" 
351 
using x a by (simp add: field_simps) 

16959  352 
also have "x * ln(1 + (y  x) / x) <= x * ((y  x) / x)" 
353 
apply (rule mult_left_mono) 

354 
apply (rule ln_add_one_self_le_self) 

355 
apply (rule divide_nonneg_pos) 

41550  356 
using x a apply simp_all 
16959  357 
done 
23482  358 
also have "... = y  x" using a by simp 
359 
also have "... = (y  x) * ln (exp 1)" by simp 

16959  360 
also have "... <= (y  x) * ln x" 
361 
apply (rule mult_left_mono) 

362 
apply (subst ln_le_cancel_iff) 

44289  363 
apply fact 
16959  364 
apply (rule a) 
41550  365 
apply (rule x) 
366 
using x apply simp 

16959  367 
done 
368 
also have "... = y * ln x  x * ln x" 

369 
by (rule left_diff_distrib) 

370 
finally have "x * ln y <= y * ln x" 

371 
by arith 

41550  372 
then have "ln y <= (y * ln x) / x" using a by (simp add: field_simps) 
373 
also have "... = y * (ln x / x)" by simp 

374 
finally show ?thesis using b by (simp add: field_simps) 

16959  375 
qed 
376 

43336  377 
lemma ln_le_minus_one: 
378 
"0 < x \<Longrightarrow> ln x \<le> x  1" 

379 
using exp_ge_add_one_self[of "ln x"] by simp 

380 

381 
lemma ln_eq_minus_one: 

382 
assumes "0 < x" "ln x = x  1" shows "x = 1" 

383 
proof  

384 
let "?l y" = "ln y  y + 1" 

385 
have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x  1)" 

386 
by (auto intro!: DERIV_intros) 

387 

388 
show ?thesis 

389 
proof (cases rule: linorder_cases) 

390 
assume "x < 1" 

391 
from dense[OF `x < 1`] obtain a where "x < a" "a < 1" by blast 

392 
from `x < a` have "?l x < ?l a" 

393 
proof (rule DERIV_pos_imp_increasing, safe) 

394 
fix y assume "x \<le> y" "y \<le> a" 

395 
with `0 < x` `a < 1` have "0 < 1 / y  1" "0 < y" 

396 
by (auto simp: field_simps) 

397 
with D show "\<exists>z. DERIV ?l y :> z \<and> 0 < z" 

398 
by auto 

399 
qed 

400 
also have "\<dots> \<le> 0" 

401 
using ln_le_minus_one `0 < x` `x < a` by (auto simp: field_simps) 

402 
finally show "x = 1" using assms by auto 

403 
next 

404 
assume "1 < x" 

405 
from dense[OF `1 < x`] obtain a where "1 < a" "a < x" by blast 

406 
from `a < x` have "?l x < ?l a" 

407 
proof (rule DERIV_neg_imp_decreasing, safe) 

408 
fix y assume "a \<le> y" "y \<le> x" 

409 
with `1 < a` have "1 / y  1 < 0" "0 < y" 

410 
by (auto simp: field_simps) 

411 
with D show "\<exists>z. DERIV ?l y :> z \<and> z < 0" 

412 
by blast 

413 
qed 

414 
also have "\<dots> \<le> 0" 

415 
using ln_le_minus_one `1 < a` by (auto simp: field_simps) 

416 
finally show "x = 1" using assms by auto 

417 
qed simp 

418 
qed 

419 

16959  420 
end 