author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47244  a7f85074c169 
child 50326  b5afeccab2db 
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 

23114  25 
lemma exp_bound: "0 <= (x::real) ==> x <= 1 ==> exp x <= 1 + x + x^2" 
16959  26 
proof  
27 
assume a: "0 <= x" 

28 
assume b: "x <= 1" 

47244  29 
{ fix n :: nat 
30 
have "2 * 2 ^ n \<le> fact (n + 2)" 

31 
by (induct n, simp, simp) 

32 
hence "real ((2::nat) * 2 ^ n) \<le> real (fact (n + 2))" 

33 
by (simp only: real_of_nat_le_iff) 

34 
hence "2 * 2 ^ n \<le> real (fact (n + 2))" 

35 
by simp 

36 
hence "inverse (fact (n + 2)) \<le> inverse (2 * 2 ^ n)" 

37 
by (rule le_imp_inverse_le) simp 

38 
hence "inverse (fact (n + 2)) \<le> 1/2 * (1/2)^n" 

39 
by (simp add: inverse_mult_distrib power_inverse) 

40 
hence "inverse (fact (n + 2)) * (x^n * x\<twosuperior>) \<le> 1/2 * (1/2)^n * (1 * x\<twosuperior>)" 

41 
by (rule mult_mono) 

42 
(rule mult_mono, simp_all add: power_le_one a b mult_nonneg_nonneg) 

43 
hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<twosuperior>/2) * ((1/2)^n)" 

44 
unfolding power_add by (simp add: mult_ac del: fact_Suc) } 

45 
note aux1 = this 

46 
have "(\<lambda>n. x\<twosuperior> / 2 * (1 / 2) ^ n) sums (x\<twosuperior> / 2 * (1 / (1  1 / 2)))" 

47 
by (intro sums_mult geometric_sums, simp) 

48 
hence aux2: "(\<lambda>n. (x::real) ^ 2 / 2 * (1 / 2) ^ n) sums x^2" 

49 
by simp 

50 
have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= x^2" 

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

52 
have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= 
16959  53 
suminf (%n. (x^2/2) * ((1/2)^n))" 
54 
apply (rule summable_le) 

47244  55 
apply (rule allI, rule aux1) 
56 
apply (rule summable_exp [THEN summable_ignore_initial_segment]) 

57 
by (rule sums_summable, rule aux2) 

16959  58 
also have "... = x^2" 
59 
by (rule sums_unique [THEN sym], rule aux2) 

60 
finally show ?thesis . 

61 
qed 

47244  62 
thus ?thesis unfolding exp_first_two_terms by auto 
16959  63 
qed 
64 

47244  65 
lemma ln_one_plus_pos_lower_bound: "0 <= x ==> x <= 1 ==> 
66 
x  x^2 <= ln (1 + x)" 

16959  67 
proof  
68 
assume a: "0 <= x" and b: "x <= 1" 

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

70 
by (rule exp_diff) 

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

72 
apply (rule divide_right_mono) 

73 
apply (rule exp_bound) 

74 
apply (rule a, rule b) 

75 
apply simp 

76 
done 

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

78 
apply (rule divide_left_mono) 

47244  79 
apply (simp add: exp_ge_add_one_self_aux) 
80 
apply (simp add: a) 

81 
apply (simp add: mult_pos_pos add_pos_nonneg) 

16959  82 
done 
83 
also from a have "... <= 1 + x" 

44289  84 
by (simp add: field_simps add_strict_increasing zero_le_mult_iff) 
47244  85 
finally have "exp (x  x^2) <= 1 + x" . 
16959  86 
also have "... = exp (ln (1 + x))" 
87 
proof  

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

89 
thus ?thesis 

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

91 
qed 

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

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

94 
qed 

95 

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

97 
proof  

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

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

29667  100 
by (simp add: algebra_simps power2_eq_square power3_eq_cube) 
16959  101 
also have "... <= 1" 
25875  102 
by (auto simp add: a) 
16959  103 
finally have "(1  x) * (1 + x + x ^ 2) <= 1" . 
47244  104 
moreover have c: "0 < 1 + x + x\<twosuperior>" 
105 
by (simp add: add_pos_nonneg a) 

16959  106 
ultimately have "1  x <= 1 / (1 + x + x^2)" 
107 
by (elim mult_imp_le_div_pos) 

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

109 
apply (rule divide_left_mono) 

110 
apply (rule exp_bound, rule a) 

47244  111 
apply (rule b [THEN less_imp_le]) 
112 
apply simp 

16959  113 
apply (rule mult_pos_pos) 
47244  114 
apply (rule c) 
115 
apply simp 

16959  116 
done 
117 
also have "... = exp (x)" 

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

118 
by (auto simp add: exp_minus divide_inverse) 
16959  119 
finally have "1  x <= exp ( x)" . 
120 
also have "1  x = exp (ln (1  x))" 

121 
proof  

122 
have "0 < 1  x" 

123 
by (insert b, auto) 

124 
thus ?thesis 

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

126 
qed 

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

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

129 
qed 

130 

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

132 
proof  

133 
assume a: "x < 1" 

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

135 
proof  

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

137 
by auto 

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

139 
by simp 

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

141 
apply (rule ln_div [THEN sym]) 

142 
by (insert a, auto) 

143 
finally show ?thesis . 

144 
qed 

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

148 

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

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

151 
proof  

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

153 
from b have c: "x < 1" 

154 
by auto 

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

156 
by (rule aux5) 

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

158 
proof  

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

160 
apply (rule ln_add_one_self_le_self) 

161 
apply (rule divide_nonneg_pos) 

162 
by (insert a c, auto) 

163 
thus ?thesis 

164 
by auto 

165 
qed 

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

167 
by auto 

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

41550  169 
have "0 < 1  x" using a b by simp 
23482  170 
hence e: "x  2 * x^2 <=  x / (1  x)" 
41550  171 
using mult_right_le_one_le[of "x*x" "2*x"] a b 
172 
by (simp add:field_simps power2_eq_square) 

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

175 
qed 

176 

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

179 
apply (erule exp_ge_add_one_self_aux) 
16959  180 
apply (case_tac "x <= 1") 
181 
apply (subgoal_tac "1 + x <= 0") 

182 
apply (erule order_trans) 

183 
apply simp 

184 
apply simp 

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

186 
apply (erule ssubst) 

187 
apply (subst exp_le_cancel_iff) 

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

189 
apply simp 

190 
apply (rule ln_one_minus_pos_upper_bound) 

191 
apply auto 

192 
done 

193 

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

47244  195 
apply (subgoal_tac "ln (1 + x) \<le> ln (exp x)", simp) 
16959  196 
apply (subst ln_le_cancel_iff) 
197 
apply auto 

198 
done 

199 

200 
lemma abs_ln_one_plus_x_minus_x_bound_nonneg: 

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

202 
proof  

23441  203 
assume x: "0 <= x" 
41550  204 
assume x1: "x <= 1" 
23441  205 
from x have "ln (1 + x) <= x" 
16959  206 
by (rule ln_add_one_self_le_self) 
207 
then have "ln (1 + x)  x <= 0" 

208 
by simp 

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

210 
by (rule abs_of_nonpos) 

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

212 
by simp 

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

214 
proof  

41550  215 
from x x1 have "x  x^2 <= ln (1 + x)" 
16959  216 
by (intro ln_one_plus_pos_lower_bound) 
217 
thus ?thesis 

218 
by simp 

219 
qed 

220 
finally show ?thesis . 

221 
qed 

222 

223 
lemma abs_ln_one_plus_x_minus_x_bound_nonpos: 

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

225 
proof  

41550  226 
assume a: "(1 / 2) <= x" 
227 
assume b: "x <= 0" 

16959  228 
have "abs(ln (1 + x)  x) = x  ln(1  (x))" 
229 
apply (subst abs_of_nonpos) 

230 
apply simp 

231 
apply (rule ln_add_one_self_le_self2) 

41550  232 
using a apply auto 
16959  233 
done 
234 
also have "... <= 2 * x^2" 

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

29667  236 
apply (simp add: algebra_simps) 
16959  237 
apply (rule ln_one_minus_pos_lower_bound) 
41550  238 
using a b apply auto 
29667  239 
done 
16959  240 
finally show ?thesis . 
241 
qed 

242 

243 
lemma abs_ln_one_plus_x_minus_x_bound: 

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

245 
apply (case_tac "0 <= x") 

246 
apply (rule order_trans) 

247 
apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg) 

248 
apply auto 

249 
apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos) 

250 
apply auto 

251 
done 

252 

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

254 
proof  

41550  255 
assume x: "exp 1 <= x" "x <= y" 
44289  256 
moreover have "0 < exp (1::real)" by simp 
257 
ultimately have a: "0 < x" and b: "0 < y" 

258 
by (fast intro: less_le_trans order_trans)+ 

16959  259 
have "x * ln y  x * ln x = x * (ln y  ln x)" 
29667  260 
by (simp add: algebra_simps) 
16959  261 
also have "... = x * ln(y / x)" 
44289  262 
by (simp only: ln_div a b) 
16959  263 
also have "y / x = (x + (y  x)) / x" 
264 
by simp 

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

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

269 
apply (rule ln_add_one_self_le_self) 

270 
apply (rule divide_nonneg_pos) 

41550  271 
using x a apply simp_all 
16959  272 
done 
23482  273 
also have "... = y  x" using a by simp 
274 
also have "... = (y  x) * ln (exp 1)" by simp 

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

277 
apply (subst ln_le_cancel_iff) 

44289  278 
apply fact 
16959  279 
apply (rule a) 
41550  280 
apply (rule x) 
281 
using x apply simp 

16959  282 
done 
283 
also have "... = y * ln x  x * ln x" 

284 
by (rule left_diff_distrib) 

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

286 
by arith 

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

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

16959  290 
qed 
291 

43336  292 
lemma ln_le_minus_one: 
293 
"0 < x \<Longrightarrow> ln x \<le> x  1" 

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

295 

296 
lemma ln_eq_minus_one: 

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

298 
proof  

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

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

301 
by (auto intro!: DERIV_intros) 

302 

303 
show ?thesis 

304 
proof (cases rule: linorder_cases) 

305 
assume "x < 1" 

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

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

308 
proof (rule DERIV_pos_imp_increasing, safe) 

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

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

311 
by (auto simp: field_simps) 

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

313 
by auto 

314 
qed 

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

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

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

318 
next 

319 
assume "1 < x" 

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

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

322 
proof (rule DERIV_neg_imp_decreasing, safe) 

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

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

325 
by (auto simp: field_simps) 

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

327 
by blast 

328 
qed 

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

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

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

332 
qed simp 

333 
qed 

334 

16959  335 
end 