author | huffman |
Fri, 19 Aug 2011 07:45:22 -0700 | |
changeset 45165 | 3bdc02eb1637 |
parent 45160 | d81d09cdab9c |
child 48113 | 1caeecc72aea |
permissions | -rw-r--r-- |
wenzelm@42830 | 1 |
(* Title: HOL/Ln.thy |
avigad@16959 | 2 |
Author: Jeremy Avigad |
avigad@16959 | 3 |
*) |
avigad@16959 | 4 |
|
avigad@16959 | 5 |
header {* Properties of ln *} |
avigad@16959 | 6 |
|
avigad@16959 | 7 |
theory Ln |
avigad@16959 | 8 |
imports Transcendental |
avigad@16959 | 9 |
begin |
avigad@16959 | 10 |
|
avigad@16959 | 11 |
lemma exp_first_two_terms: "exp x = 1 + x + suminf (%n. |
nipkow@41107 | 12 |
inverse(fact (n+2)) * (x ^ (n+2)))" |
avigad@16959 | 13 |
proof - |
nipkow@41107 | 14 |
have "exp x = suminf (%n. inverse(fact n) * (x ^ n))" |
wenzelm@19765 | 15 |
by (simp add: exp_def) |
nipkow@41107 | 16 |
also from summable_exp have "... = (SUM n::nat : {0..<2}. |
nipkow@41107 | 17 |
inverse(fact n) * (x ^ n)) + suminf (%n. |
nipkow@41107 | 18 |
inverse(fact(n+2)) * (x ^ (n+2)))" (is "_ = ?a + _") |
avigad@16959 | 19 |
by (rule suminf_split_initial_segment) |
avigad@16959 | 20 |
also have "?a = 1 + x" |
huffman@45160 | 21 |
by (simp add: numeral_2_eq_2) |
avigad@16959 | 22 |
finally show ?thesis . |
avigad@16959 | 23 |
qed |
avigad@16959 | 24 |
|
avigad@16959 | 25 |
lemma exp_tail_after_first_two_terms_summable: |
nipkow@41107 | 26 |
"summable (%n. inverse(fact (n+2)) * (x ^ (n+2)))" |
avigad@16959 | 27 |
proof - |
avigad@16959 | 28 |
note summable_exp |
avigad@16959 | 29 |
thus ?thesis |
avigad@16959 | 30 |
by (frule summable_ignore_initial_segment) |
avigad@16959 | 31 |
qed |
avigad@16959 | 32 |
|
avigad@16959 | 33 |
lemma aux1: assumes a: "0 <= x" and b: "x <= 1" |
nipkow@41107 | 34 |
shows "inverse (fact ((n::nat) + 2)) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)" |
avigad@16959 | 35 |
proof (induct n) |
nipkow@41107 | 36 |
show "inverse (fact ((0::nat) + 2)) * x ^ (0 + 2) <= |
avigad@16959 | 37 |
x ^ 2 / 2 * (1 / 2) ^ 0" |
nipkow@23482 | 38 |
by (simp add: real_of_nat_Suc power2_eq_square) |
avigad@16959 | 39 |
next |
avigad@32031 | 40 |
fix n :: nat |
nipkow@41107 | 41 |
assume c: "inverse (fact (n + 2)) * x ^ (n + 2) |
avigad@16959 | 42 |
<= x ^ 2 / 2 * (1 / 2) ^ n" |
nipkow@41107 | 43 |
show "inverse (fact (Suc n + 2)) * x ^ (Suc n + 2) |
avigad@16959 | 44 |
<= x ^ 2 / 2 * (1 / 2) ^ Suc n" |
avigad@16959 | 45 |
proof - |
nipkow@41107 | 46 |
have "inverse(fact (Suc n + 2)) <= (1/2) * inverse (fact (n+2))" |
avigad@16959 | 47 |
proof - |
avigad@16959 | 48 |
have "Suc n + 2 = Suc (n + 2)" by simp |
avigad@16959 | 49 |
then have "fact (Suc n + 2) = Suc (n + 2) * fact (n + 2)" |
avigad@16959 | 50 |
by simp |
avigad@16959 | 51 |
then have "real(fact (Suc n + 2)) = real(Suc (n + 2) * fact (n + 2))" |
avigad@16959 | 52 |
apply (rule subst) |
avigad@16959 | 53 |
apply (rule refl) |
avigad@16959 | 54 |
done |
avigad@16959 | 55 |
also have "... = real(Suc (n + 2)) * real(fact (n + 2))" |
avigad@16959 | 56 |
by (rule real_of_nat_mult) |
avigad@16959 | 57 |
finally have "real (fact (Suc n + 2)) = |
avigad@16959 | 58 |
real (Suc (n + 2)) * real (fact (n + 2))" . |
nipkow@41107 | 59 |
then have "inverse(fact (Suc n + 2)) = |
nipkow@41107 | 60 |
inverse(Suc (n + 2)) * inverse(fact (n + 2))" |
avigad@16959 | 61 |
apply (rule ssubst) |
avigad@16959 | 62 |
apply (rule inverse_mult_distrib) |
avigad@16959 | 63 |
done |
nipkow@41107 | 64 |
also have "... <= (1/2) * inverse(fact (n + 2))" |
avigad@16959 | 65 |
apply (rule mult_right_mono) |
avigad@16959 | 66 |
apply (subst inverse_eq_divide) |
avigad@16959 | 67 |
apply simp |
huffman@45165 | 68 |
apply (simp del: fact_Suc) |
avigad@16959 | 69 |
done |
avigad@16959 | 70 |
finally show ?thesis . |
avigad@16959 | 71 |
qed |
avigad@16959 | 72 |
moreover have "x ^ (Suc n + 2) <= x ^ (n + 2)" |
huffman@45160 | 73 |
by (simp add: mult_left_le_one_le mult_nonneg_nonneg a b) |
nipkow@41107 | 74 |
ultimately have "inverse (fact (Suc n + 2)) * x ^ (Suc n + 2) <= |
nipkow@41107 | 75 |
(1 / 2 * inverse (fact (n + 2))) * x ^ (n + 2)" |
avigad@16959 | 76 |
apply (rule mult_mono) |
avigad@16959 | 77 |
apply (rule mult_nonneg_nonneg) |
avigad@16959 | 78 |
apply simp |
avigad@16959 | 79 |
apply (subst inverse_nonnegative_iff_nonnegative) |
huffman@27483 | 80 |
apply (rule real_of_nat_ge_zero) |
avigad@16959 | 81 |
apply (rule zero_le_power) |
huffman@23441 | 82 |
apply (rule a) |
avigad@16959 | 83 |
done |
nipkow@41107 | 84 |
also have "... = 1 / 2 * (inverse (fact (n + 2)) * x ^ (n + 2))" |
avigad@16959 | 85 |
by simp |
avigad@16959 | 86 |
also have "... <= 1 / 2 * (x ^ 2 / 2 * (1 / 2) ^ n)" |
avigad@16959 | 87 |
apply (rule mult_left_mono) |
wenzelm@41798 | 88 |
apply (rule c) |
avigad@16959 | 89 |
apply simp |
avigad@16959 | 90 |
done |
avigad@16959 | 91 |
also have "... = x ^ 2 / 2 * (1 / 2 * (1 / 2) ^ n)" |
avigad@16959 | 92 |
by auto |
avigad@16959 | 93 |
also have "(1::real) / 2 * (1 / 2) ^ n = (1 / 2) ^ (Suc n)" |
huffman@30269 | 94 |
by (rule power_Suc [THEN sym]) |
avigad@16959 | 95 |
finally show ?thesis . |
avigad@16959 | 96 |
qed |
avigad@16959 | 97 |
qed |
avigad@16959 | 98 |
|
huffman@20692 | 99 |
lemma aux2: "(%n. (x::real) ^ 2 / 2 * (1 / 2) ^ n) sums x^2" |
avigad@16959 | 100 |
proof - |
huffman@20692 | 101 |
have "(%n. (1 / 2::real)^n) sums (1 / (1 - (1/2)))" |
avigad@16959 | 102 |
apply (rule geometric_sums) |
huffman@22998 | 103 |
by (simp add: abs_less_iff) |
avigad@16959 | 104 |
also have "(1::real) / (1 - 1/2) = 2" |
avigad@16959 | 105 |
by simp |
huffman@20692 | 106 |
finally have "(%n. (1 / 2::real)^n) sums 2" . |
avigad@16959 | 107 |
then have "(%n. x ^ 2 / 2 * (1 / 2) ^ n) sums (x^2 / 2 * 2)" |
avigad@16959 | 108 |
by (rule sums_mult) |
avigad@16959 | 109 |
also have "x^2 / 2 * 2 = x^2" |
avigad@16959 | 110 |
by simp |
avigad@16959 | 111 |
finally show ?thesis . |
avigad@16959 | 112 |
qed |
avigad@16959 | 113 |
|
huffman@23114 | 114 |
lemma exp_bound: "0 <= (x::real) ==> x <= 1 ==> exp x <= 1 + x + x^2" |
avigad@16959 | 115 |
proof - |
avigad@16959 | 116 |
assume a: "0 <= x" |
avigad@16959 | 117 |
assume b: "x <= 1" |
nipkow@41107 | 118 |
have c: "exp x = 1 + x + suminf (%n. inverse(fact (n+2)) * |
avigad@16959 | 119 |
(x ^ (n+2)))" |
avigad@16959 | 120 |
by (rule exp_first_two_terms) |
nipkow@41107 | 121 |
moreover have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= x^2" |
avigad@16959 | 122 |
proof - |
nipkow@41107 | 123 |
have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= |
avigad@16959 | 124 |
suminf (%n. (x^2/2) * ((1/2)^n))" |
avigad@16959 | 125 |
apply (rule summable_le) |
wenzelm@41798 | 126 |
apply (auto simp only: aux1 a b) |
avigad@16959 | 127 |
apply (rule exp_tail_after_first_two_terms_summable) |
avigad@16959 | 128 |
by (rule sums_summable, rule aux2) |
avigad@16959 | 129 |
also have "... = x^2" |
avigad@16959 | 130 |
by (rule sums_unique [THEN sym], rule aux2) |
avigad@16959 | 131 |
finally show ?thesis . |
avigad@16959 | 132 |
qed |
avigad@16959 | 133 |
ultimately show ?thesis |
avigad@16959 | 134 |
by auto |
avigad@16959 | 135 |
qed |
avigad@16959 | 136 |
|
huffman@23114 | 137 |
lemma aux4: "0 <= (x::real) ==> x <= 1 ==> exp (x - x^2) <= 1 + x" |
avigad@16959 | 138 |
proof - |
avigad@16959 | 139 |
assume a: "0 <= x" and b: "x <= 1" |
avigad@16959 | 140 |
have "exp (x - x^2) = exp x / exp (x^2)" |
avigad@16959 | 141 |
by (rule exp_diff) |
avigad@16959 | 142 |
also have "... <= (1 + x + x^2) / exp (x ^2)" |
avigad@16959 | 143 |
apply (rule divide_right_mono) |
avigad@16959 | 144 |
apply (rule exp_bound) |
avigad@16959 | 145 |
apply (rule a, rule b) |
avigad@16959 | 146 |
apply simp |
avigad@16959 | 147 |
done |
avigad@16959 | 148 |
also have "... <= (1 + x + x^2) / (1 + x^2)" |
avigad@16959 | 149 |
apply (rule divide_left_mono) |
avigad@17013 | 150 |
apply (auto simp add: exp_ge_add_one_self_aux) |
avigad@16959 | 151 |
apply (rule add_nonneg_nonneg) |
wenzelm@41798 | 152 |
using a apply auto |
avigad@16959 | 153 |
apply (rule mult_pos_pos) |
avigad@16959 | 154 |
apply auto |
avigad@16959 | 155 |
apply (rule add_pos_nonneg) |
avigad@16959 | 156 |
apply auto |
avigad@16959 | 157 |
done |
avigad@16959 | 158 |
also from a have "... <= 1 + x" |
huffman@45160 | 159 |
by (simp add: field_simps add_strict_increasing zero_le_mult_iff) |
avigad@16959 | 160 |
finally show ?thesis . |
avigad@16959 | 161 |
qed |
avigad@16959 | 162 |
|
avigad@16959 | 163 |
lemma ln_one_plus_pos_lower_bound: "0 <= x ==> x <= 1 ==> |
avigad@16959 | 164 |
x - x^2 <= ln (1 + x)" |
avigad@16959 | 165 |
proof - |
avigad@16959 | 166 |
assume a: "0 <= x" and b: "x <= 1" |
avigad@16959 | 167 |
then have "exp (x - x^2) <= 1 + x" |
avigad@16959 | 168 |
by (rule aux4) |
avigad@16959 | 169 |
also have "... = exp (ln (1 + x))" |
avigad@16959 | 170 |
proof - |
avigad@16959 | 171 |
from a have "0 < 1 + x" by auto |
avigad@16959 | 172 |
thus ?thesis |
avigad@16959 | 173 |
by (auto simp only: exp_ln_iff [THEN sym]) |
avigad@16959 | 174 |
qed |
avigad@16959 | 175 |
finally have "exp (x - x ^ 2) <= exp (ln (1 + x))" . |
avigad@16959 | 176 |
thus ?thesis by (auto simp only: exp_le_cancel_iff) |
avigad@16959 | 177 |
qed |
avigad@16959 | 178 |
|
avigad@16959 | 179 |
lemma ln_one_minus_pos_upper_bound: "0 <= x ==> x < 1 ==> ln (1 - x) <= - x" |
avigad@16959 | 180 |
proof - |
avigad@16959 | 181 |
assume a: "0 <= (x::real)" and b: "x < 1" |
avigad@16959 | 182 |
have "(1 - x) * (1 + x + x^2) = (1 - x^3)" |
nipkow@29667 | 183 |
by (simp add: algebra_simps power2_eq_square power3_eq_cube) |
avigad@16959 | 184 |
also have "... <= 1" |
nipkow@25875 | 185 |
by (auto simp add: a) |
avigad@16959 | 186 |
finally have "(1 - x) * (1 + x + x ^ 2) <= 1" . |
avigad@16959 | 187 |
moreover have "0 < 1 + x + x^2" |
avigad@16959 | 188 |
apply (rule add_pos_nonneg) |
wenzelm@41798 | 189 |
using a apply auto |
avigad@16959 | 190 |
done |
avigad@16959 | 191 |
ultimately have "1 - x <= 1 / (1 + x + x^2)" |
avigad@16959 | 192 |
by (elim mult_imp_le_div_pos) |
avigad@16959 | 193 |
also have "... <= 1 / exp x" |
avigad@16959 | 194 |
apply (rule divide_left_mono) |
avigad@16959 | 195 |
apply (rule exp_bound, rule a) |
wenzelm@41798 | 196 |
using a b apply auto |
avigad@16959 | 197 |
apply (rule mult_pos_pos) |
avigad@16959 | 198 |
apply (rule add_pos_nonneg) |
avigad@16959 | 199 |
apply auto |
avigad@16959 | 200 |
done |
avigad@16959 | 201 |
also have "... = exp (-x)" |
huffman@36769 | 202 |
by (auto simp add: exp_minus divide_inverse) |
avigad@16959 | 203 |
finally have "1 - x <= exp (- x)" . |
avigad@16959 | 204 |
also have "1 - x = exp (ln (1 - x))" |
avigad@16959 | 205 |
proof - |
avigad@16959 | 206 |
have "0 < 1 - x" |
avigad@16959 | 207 |
by (insert b, auto) |
avigad@16959 | 208 |
thus ?thesis |
avigad@16959 | 209 |
by (auto simp only: exp_ln_iff [THEN sym]) |
avigad@16959 | 210 |
qed |
avigad@16959 | 211 |
finally have "exp (ln (1 - x)) <= exp (- x)" . |
avigad@16959 | 212 |
thus ?thesis by (auto simp only: exp_le_cancel_iff) |
avigad@16959 | 213 |
qed |
avigad@16959 | 214 |
|
avigad@16959 | 215 |
lemma aux5: "x < 1 ==> ln(1 - x) = - ln(1 + x / (1 - x))" |
avigad@16959 | 216 |
proof - |
avigad@16959 | 217 |
assume a: "x < 1" |
avigad@16959 | 218 |
have "ln(1 - x) = - ln(1 / (1 - x))" |
avigad@16959 | 219 |
proof - |
avigad@16959 | 220 |
have "ln(1 - x) = - (- ln (1 - x))" |
avigad@16959 | 221 |
by auto |
avigad@16959 | 222 |
also have "- ln(1 - x) = ln 1 - ln(1 - x)" |
avigad@16959 | 223 |
by simp |
avigad@16959 | 224 |
also have "... = ln(1 / (1 - x))" |
avigad@16959 | 225 |
apply (rule ln_div [THEN sym]) |
avigad@16959 | 226 |
by (insert a, auto) |
avigad@16959 | 227 |
finally show ?thesis . |
avigad@16959 | 228 |
qed |
nipkow@23482 | 229 |
also have " 1 / (1 - x) = 1 + x / (1 - x)" using a by(simp add:field_simps) |
avigad@16959 | 230 |
finally show ?thesis . |
avigad@16959 | 231 |
qed |
avigad@16959 | 232 |
|
avigad@16959 | 233 |
lemma ln_one_minus_pos_lower_bound: "0 <= x ==> x <= (1 / 2) ==> |
avigad@16959 | 234 |
- x - 2 * x^2 <= ln (1 - x)" |
avigad@16959 | 235 |
proof - |
avigad@16959 | 236 |
assume a: "0 <= x" and b: "x <= (1 / 2)" |
avigad@16959 | 237 |
from b have c: "x < 1" |
avigad@16959 | 238 |
by auto |
avigad@16959 | 239 |
then have "ln (1 - x) = - ln (1 + x / (1 - x))" |
avigad@16959 | 240 |
by (rule aux5) |
avigad@16959 | 241 |
also have "- (x / (1 - x)) <= ..." |
avigad@16959 | 242 |
proof - |
avigad@16959 | 243 |
have "ln (1 + x / (1 - x)) <= x / (1 - x)" |
avigad@16959 | 244 |
apply (rule ln_add_one_self_le_self) |
avigad@16959 | 245 |
apply (rule divide_nonneg_pos) |
avigad@16959 | 246 |
by (insert a c, auto) |
avigad@16959 | 247 |
thus ?thesis |
avigad@16959 | 248 |
by auto |
avigad@16959 | 249 |
qed |
avigad@16959 | 250 |
also have "- (x / (1 - x)) = -x / (1 - x)" |
avigad@16959 | 251 |
by auto |
avigad@16959 | 252 |
finally have d: "- x / (1 - x) <= ln (1 - x)" . |
wenzelm@41798 | 253 |
have "0 < 1 - x" using a b by simp |
nipkow@23482 | 254 |
hence e: "-x - 2 * x^2 <= - x / (1 - x)" |
wenzelm@41798 | 255 |
using mult_right_le_one_le[of "x*x" "2*x"] a b |
wenzelm@41798 | 256 |
by (simp add:field_simps power2_eq_square) |
avigad@16959 | 257 |
from e d show "- x - 2 * x^2 <= ln (1 - x)" |
avigad@16959 | 258 |
by (rule order_trans) |
avigad@16959 | 259 |
qed |
avigad@16959 | 260 |
|
huffman@23114 | 261 |
lemma exp_ge_add_one_self [simp]: "1 + (x::real) <= exp x" |
avigad@16959 | 262 |
apply (case_tac "0 <= x") |
avigad@17013 | 263 |
apply (erule exp_ge_add_one_self_aux) |
avigad@16959 | 264 |
apply (case_tac "x <= -1") |
avigad@16959 | 265 |
apply (subgoal_tac "1 + x <= 0") |
avigad@16959 | 266 |
apply (erule order_trans) |
avigad@16959 | 267 |
apply simp |
avigad@16959 | 268 |
apply simp |
avigad@16959 | 269 |
apply (subgoal_tac "1 + x = exp(ln (1 + x))") |
avigad@16959 | 270 |
apply (erule ssubst) |
avigad@16959 | 271 |
apply (subst exp_le_cancel_iff) |
avigad@16959 | 272 |
apply (subgoal_tac "ln (1 - (- x)) <= - (- x)") |
avigad@16959 | 273 |
apply simp |
avigad@16959 | 274 |
apply (rule ln_one_minus_pos_upper_bound) |
avigad@16959 | 275 |
apply auto |
avigad@16959 | 276 |
done |
avigad@16959 | 277 |
|
avigad@16959 | 278 |
lemma ln_add_one_self_le_self2: "-1 < x ==> ln(1 + x) <= x" |
avigad@16959 | 279 |
apply (subgoal_tac "x = ln (exp x)") |
avigad@16959 | 280 |
apply (erule ssubst)back |
avigad@16959 | 281 |
apply (subst ln_le_cancel_iff) |
avigad@16959 | 282 |
apply auto |
avigad@16959 | 283 |
done |
avigad@16959 | 284 |
|
avigad@16959 | 285 |
lemma abs_ln_one_plus_x_minus_x_bound_nonneg: |
avigad@16959 | 286 |
"0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x^2" |
avigad@16959 | 287 |
proof - |
huffman@23441 | 288 |
assume x: "0 <= x" |
wenzelm@41798 | 289 |
assume x1: "x <= 1" |
huffman@23441 | 290 |
from x have "ln (1 + x) <= x" |
avigad@16959 | 291 |
by (rule ln_add_one_self_le_self) |
avigad@16959 | 292 |
then have "ln (1 + x) - x <= 0" |
avigad@16959 | 293 |
by simp |
avigad@16959 | 294 |
then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)" |
avigad@16959 | 295 |
by (rule abs_of_nonpos) |
avigad@16959 | 296 |
also have "... = x - ln (1 + x)" |
avigad@16959 | 297 |
by simp |
avigad@16959 | 298 |
also have "... <= x^2" |
avigad@16959 | 299 |
proof - |
wenzelm@41798 | 300 |
from x x1 have "x - x^2 <= ln (1 + x)" |
avigad@16959 | 301 |
by (intro ln_one_plus_pos_lower_bound) |
avigad@16959 | 302 |
thus ?thesis |
avigad@16959 | 303 |
by simp |
avigad@16959 | 304 |
qed |
avigad@16959 | 305 |
finally show ?thesis . |
avigad@16959 | 306 |
qed |
avigad@16959 | 307 |
|
avigad@16959 | 308 |
lemma abs_ln_one_plus_x_minus_x_bound_nonpos: |
avigad@16959 | 309 |
"-(1 / 2) <= x ==> x <= 0 ==> abs(ln (1 + x) - x) <= 2 * x^2" |
avigad@16959 | 310 |
proof - |
wenzelm@41798 | 311 |
assume a: "-(1 / 2) <= x" |
wenzelm@41798 | 312 |
assume b: "x <= 0" |
avigad@16959 | 313 |
have "abs(ln (1 + x) - x) = x - ln(1 - (-x))" |
avigad@16959 | 314 |
apply (subst abs_of_nonpos) |
avigad@16959 | 315 |
apply simp |
avigad@16959 | 316 |
apply (rule ln_add_one_self_le_self2) |
wenzelm@41798 | 317 |
using a apply auto |
avigad@16959 | 318 |
done |
avigad@16959 | 319 |
also have "... <= 2 * x^2" |
avigad@16959 | 320 |
apply (subgoal_tac "- (-x) - 2 * (-x)^2 <= ln (1 - (-x))") |
nipkow@29667 | 321 |
apply (simp add: algebra_simps) |
avigad@16959 | 322 |
apply (rule ln_one_minus_pos_lower_bound) |
wenzelm@41798 | 323 |
using a b apply auto |
nipkow@29667 | 324 |
done |
avigad@16959 | 325 |
finally show ?thesis . |
avigad@16959 | 326 |
qed |
avigad@16959 | 327 |
|
avigad@16959 | 328 |
lemma abs_ln_one_plus_x_minus_x_bound: |
avigad@16959 | 329 |
"abs x <= 1 / 2 ==> abs(ln (1 + x) - x) <= 2 * x^2" |
avigad@16959 | 330 |
apply (case_tac "0 <= x") |
avigad@16959 | 331 |
apply (rule order_trans) |
avigad@16959 | 332 |
apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg) |
avigad@16959 | 333 |
apply auto |
avigad@16959 | 334 |
apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos) |
avigad@16959 | 335 |
apply auto |
avigad@16959 | 336 |
done |
avigad@16959 | 337 |
|
avigad@16959 | 338 |
lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)" |
avigad@16959 | 339 |
proof - |
wenzelm@41798 | 340 |
assume x: "exp 1 <= x" "x <= y" |
huffman@45160 | 341 |
moreover have "0 < exp (1::real)" by simp |
huffman@45160 | 342 |
ultimately have a: "0 < x" and b: "0 < y" |
huffman@45160 | 343 |
by (fast intro: less_le_trans order_trans)+ |
avigad@16959 | 344 |
have "x * ln y - x * ln x = x * (ln y - ln x)" |
nipkow@29667 | 345 |
by (simp add: algebra_simps) |
avigad@16959 | 346 |
also have "... = x * ln(y / x)" |
huffman@45160 | 347 |
by (simp only: ln_div a b) |
avigad@16959 | 348 |
also have "y / x = (x + (y - x)) / x" |
avigad@16959 | 349 |
by simp |
huffman@45160 | 350 |
also have "... = 1 + (y - x) / x" |
huffman@45160 | 351 |
using x a by (simp add: field_simps) |
avigad@16959 | 352 |
also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)" |
avigad@16959 | 353 |
apply (rule mult_left_mono) |
avigad@16959 | 354 |
apply (rule ln_add_one_self_le_self) |
avigad@16959 | 355 |
apply (rule divide_nonneg_pos) |
wenzelm@41798 | 356 |
using x a apply simp_all |
avigad@16959 | 357 |
done |
nipkow@23482 | 358 |
also have "... = y - x" using a by simp |
nipkow@23482 | 359 |
also have "... = (y - x) * ln (exp 1)" by simp |
avigad@16959 | 360 |
also have "... <= (y - x) * ln x" |
avigad@16959 | 361 |
apply (rule mult_left_mono) |
avigad@16959 | 362 |
apply (subst ln_le_cancel_iff) |
huffman@45160 | 363 |
apply fact |
avigad@16959 | 364 |
apply (rule a) |
wenzelm@41798 | 365 |
apply (rule x) |
wenzelm@41798 | 366 |
using x apply simp |
avigad@16959 | 367 |
done |
avigad@16959 | 368 |
also have "... = y * ln x - x * ln x" |
avigad@16959 | 369 |
by (rule left_diff_distrib) |
avigad@16959 | 370 |
finally have "x * ln y <= y * ln x" |
avigad@16959 | 371 |
by arith |
wenzelm@41798 | 372 |
then have "ln y <= (y * ln x) / x" using a by (simp add: field_simps) |
wenzelm@41798 | 373 |
also have "... = y * (ln x / x)" by simp |
wenzelm@41798 | 374 |
finally show ?thesis using b by (simp add: field_simps) |
avigad@16959 | 375 |
qed |
avigad@16959 | 376 |
|
hoelzl@44193 | 377 |
lemma ln_le_minus_one: |
hoelzl@44193 | 378 |
"0 < x \<Longrightarrow> ln x \<le> x - 1" |
hoelzl@44193 | 379 |
using exp_ge_add_one_self[of "ln x"] by simp |
hoelzl@44193 | 380 |
|
hoelzl@44193 | 381 |
lemma ln_eq_minus_one: |
hoelzl@44193 | 382 |
assumes "0 < x" "ln x = x - 1" shows "x = 1" |
hoelzl@44193 | 383 |
proof - |
hoelzl@44193 | 384 |
let "?l y" = "ln y - y + 1" |
hoelzl@44193 | 385 |
have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)" |
hoelzl@44193 | 386 |
by (auto intro!: DERIV_intros) |
hoelzl@44193 | 387 |
|
hoelzl@44193 | 388 |
show ?thesis |
hoelzl@44193 | 389 |
proof (cases rule: linorder_cases) |
hoelzl@44193 | 390 |
assume "x < 1" |
hoelzl@44193 | 391 |
from dense[OF `x < 1`] obtain a where "x < a" "a < 1" by blast |
hoelzl@44193 | 392 |
from `x < a` have "?l x < ?l a" |
hoelzl@44193 | 393 |
proof (rule DERIV_pos_imp_increasing, safe) |
hoelzl@44193 | 394 |
fix y assume "x \<le> y" "y \<le> a" |
hoelzl@44193 | 395 |
with `0 < x` `a < 1` have "0 < 1 / y - 1" "0 < y" |
hoelzl@44193 | 396 |
by (auto simp: field_simps) |
hoelzl@44193 | 397 |
with D show "\<exists>z. DERIV ?l y :> z \<and> 0 < z" |
hoelzl@44193 | 398 |
by auto |
hoelzl@44193 | 399 |
qed |
hoelzl@44193 | 400 |
also have "\<dots> \<le> 0" |
hoelzl@44193 | 401 |
using ln_le_minus_one `0 < x` `x < a` by (auto simp: field_simps) |
hoelzl@44193 | 402 |
finally show "x = 1" using assms by auto |
hoelzl@44193 | 403 |
next |
hoelzl@44193 | 404 |
assume "1 < x" |
hoelzl@44193 | 405 |
from dense[OF `1 < x`] obtain a where "1 < a" "a < x" by blast |
hoelzl@44193 | 406 |
from `a < x` have "?l x < ?l a" |
hoelzl@44193 | 407 |
proof (rule DERIV_neg_imp_decreasing, safe) |
hoelzl@44193 | 408 |
fix y assume "a \<le> y" "y \<le> x" |
hoelzl@44193 | 409 |
with `1 < a` have "1 / y - 1 < 0" "0 < y" |
hoelzl@44193 | 410 |
by (auto simp: field_simps) |
hoelzl@44193 | 411 |
with D show "\<exists>z. DERIV ?l y :> z \<and> z < 0" |
hoelzl@44193 | 412 |
by blast |
hoelzl@44193 | 413 |
qed |
hoelzl@44193 | 414 |
also have "\<dots> \<le> 0" |
hoelzl@44193 | 415 |
using ln_le_minus_one `1 < a` by (auto simp: field_simps) |
hoelzl@44193 | 416 |
finally show "x = 1" using assms by auto |
hoelzl@44193 | 417 |
qed simp |
hoelzl@44193 | 418 |
qed |
hoelzl@44193 | 419 |
|
avigad@16959 | 420 |
end |