16959

1 
(* Title: Ln.thy


2 
Author: Jeremy Avigad


3 
*)


4 


5 
header {* Properties of ln *}


6 


7 
theory Ln


8 


9 
imports Transcendental


10 
begin


11 


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


13 
inverse(real (fact (n+2))) * (x ^ (n+2)))"


14 
proof 


15 
have "exp x = suminf (%n. inverse(real (fact n)) * (x ^ n))"


16 
by (unfold exp_def, simp)


17 
also from summable_exp have "... = (SUM n : {0..<2}.


18 
inverse(real (fact n)) * (x ^ n)) + suminf (%n.


19 
inverse(real (fact (n+2))) * (x ^ (n+2)))" (is "_ = ?a + _")


20 
by (rule suminf_split_initial_segment)


21 
also have "?a = 1 + x"


22 
by (simp add: numerals)


23 
finally show ?thesis .


24 
qed


25 


26 
lemma exp_tail_after_first_two_terms_summable:


27 
"summable (%n. inverse(real (fact (n+2))) * (x ^ (n+2)))"


28 
proof 


29 
note summable_exp


30 
thus ?thesis


31 
by (frule summable_ignore_initial_segment)


32 
qed


33 


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


35 
shows "inverse (real (fact (n + 2))) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"


36 
proof (induct n)


37 
show "inverse (real (fact (0 + 2))) * x ^ (0 + 2) <=


38 
x ^ 2 / 2 * (1 / 2) ^ 0"


39 
apply (simp add: power2_eq_square)


40 
apply (subgoal_tac "real (Suc (Suc 0)) = 2")


41 
apply (erule ssubst)


42 
apply simp


43 
apply simp


44 
done


45 
next


46 
fix n


47 
assume c: "inverse (real (fact (n + 2))) * x ^ (n + 2)


48 
<= x ^ 2 / 2 * (1 / 2) ^ n"


49 
show "inverse (real (fact (Suc n + 2))) * x ^ (Suc n + 2)


50 
<= x ^ 2 / 2 * (1 / 2) ^ Suc n"


51 
proof 


52 
have "inverse(real (fact (Suc n + 2))) <=


53 
(1 / 2) *inverse (real (fact (n+2)))"


54 
proof 


55 
have "Suc n + 2 = Suc (n + 2)" by simp


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


57 
by simp


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


59 
apply (rule subst)


60 
apply (rule refl)


61 
done


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


63 
by (rule real_of_nat_mult)


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


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


66 
then have "inverse(real (fact (Suc n + 2))) =


67 
inverse(real (Suc (n + 2))) * inverse(real (fact (n + 2)))"


68 
apply (rule ssubst)


69 
apply (rule inverse_mult_distrib)


70 
done


71 
also have "... <= (1/2) * inverse(real (fact (n + 2)))"


72 
apply (rule mult_right_mono)


73 
apply (subst inverse_eq_divide)


74 
apply simp


75 
apply (rule inv_real_of_nat_fact_ge_zero)


76 
done


77 
finally show ?thesis .


78 
qed


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


80 
apply (simp add: mult_compare_simps)


81 
apply (simp add: prems)


82 
apply (subgoal_tac "0 <= x * (x * x^n)")


83 
apply force


84 
apply (rule mult_nonneg_nonneg, rule a)+


85 
apply (rule zero_le_power, rule a)


86 
done


87 
ultimately have "inverse (real (fact (Suc n + 2))) * x ^ (Suc n + 2) <=


88 
(1 / 2 * inverse (real (fact (n + 2)))) * x ^ (n + 2)"


89 
apply (rule mult_mono)


90 
apply (rule mult_nonneg_nonneg)


91 
apply simp


92 
apply (subst inverse_nonnegative_iff_nonnegative)


93 
apply (rule real_of_nat_fact_ge_zero)


94 
apply (rule zero_le_power)


95 
apply assumption


96 
done


97 
also have "... = 1 / 2 * (inverse (real (fact (n + 2))) * x ^ (n + 2))"


98 
by simp


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


100 
apply (rule mult_left_mono)


101 
apply (rule prems)


102 
apply simp


103 
done


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


105 
by auto


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


107 
by (rule realpow_Suc [THEN sym])


108 
finally show ?thesis .


109 
qed


110 
qed


111 


112 
lemma aux2: "(%n. x ^ 2 / 2 * (1 / 2) ^ n) sums x^2"


113 
proof 


114 
have "(%n. (1 / 2)^n) sums (1 / (1  (1/2)))"


115 
apply (rule geometric_sums)


116 
by (simp add: abs_interval_iff)


117 
also have "(1::real) / (1  1/2) = 2"


118 
by simp


119 
finally have "(%n. (1 / 2)^n) sums 2" .


120 
then have "(%n. x ^ 2 / 2 * (1 / 2) ^ n) sums (x^2 / 2 * 2)"


121 
by (rule sums_mult)


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


123 
by simp


124 
finally show ?thesis .


125 
qed


126 


127 
lemma exp_bound: "0 <= x ==> x <= 1 ==> exp x <= 1 + x + x^2"


128 
proof 


129 
assume a: "0 <= x"


130 
assume b: "x <= 1"


131 
have c: "exp x = 1 + x + suminf (%n. inverse(real (fact (n+2))) *


132 
(x ^ (n+2)))"


133 
by (rule exp_first_two_terms)


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


135 
proof 


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


137 
suminf (%n. (x^2/2) * ((1/2)^n))"


138 
apply (rule summable_le)


139 
apply (auto simp only: aux1 prems)


140 
apply (rule exp_tail_after_first_two_terms_summable)


141 
by (rule sums_summable, rule aux2)


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


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


144 
finally show ?thesis .


145 
qed


146 
ultimately show ?thesis


147 
by auto


148 
qed


149 


150 
lemma aux3: "(0::real) <= x ==> (1 + x + x^2)/(1 + x^2) <= 1 + x"


151 
apply (subst pos_divide_le_eq)


152 
apply (simp add: zero_compare_simps)


153 
apply (simp add: ring_eq_simps zero_compare_simps)


154 
done


155 


156 
lemma aux4: "0 <= x ==> x <= 1 ==> exp (x  x^2) <= 1 + x"


157 
proof 


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


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


160 
by (rule exp_diff)


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


162 
apply (rule divide_right_mono)


163 
apply (rule exp_bound)


164 
apply (rule a, rule b)


165 
apply simp


166 
done


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


168 
apply (rule divide_left_mono)


169 
apply auto


170 
apply (rule add_nonneg_nonneg)


171 
apply (insert prems, auto)


172 
apply (rule mult_pos_pos)


173 
apply auto


174 
apply (rule add_pos_nonneg)


175 
apply auto


176 
done


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


178 
by (rule aux3)


179 
finally show ?thesis .


180 
qed


181 


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


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


184 
proof 


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


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


187 
by (rule aux4)


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


189 
proof 


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


191 
thus ?thesis


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


193 
qed


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


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


196 
qed


197 


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


199 
proof 


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


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


202 
by (simp add: ring_eq_simps power2_eq_square power3_eq_cube)


203 
also have "... <= 1"


204 
by (auto intro: zero_le_power simp add: a)


205 
finally have "(1  x) * (1 + x + x ^ 2) <= 1" .


206 
moreover have "0 < 1 + x + x^2"


207 
apply (rule add_pos_nonneg)


208 
apply (insert a, auto)


209 
done


210 
ultimately have "1  x <= 1 / (1 + x + x^2)"


211 
by (elim mult_imp_le_div_pos)


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


213 
apply (rule divide_left_mono)


214 
apply (rule exp_bound, rule a)


215 
apply (insert prems, auto)


216 
apply (rule mult_pos_pos)


217 
apply (rule add_pos_nonneg)


218 
apply auto


219 
done


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


221 
by (auto simp add: exp_minus real_divide_def)


222 
finally have "1  x <= exp ( x)" .


223 
also have "1  x = exp (ln (1  x))"


224 
proof 


225 
have "0 < 1  x"


226 
by (insert b, auto)


227 
thus ?thesis


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


229 
qed


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


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


232 
qed


233 


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


235 
proof 


236 
assume a: "x < 1"


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


238 
proof 


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


240 
by auto


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


242 
by simp


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


244 
apply (rule ln_div [THEN sym])


245 
by (insert a, auto)


246 
finally show ?thesis .


247 
qed


248 
also have " 1 / (1  x) = 1 + x / (1  x)"


249 
proof 


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


251 
by auto


252 
also have "... = (1  x) / (1  x) + x / (1  x)"


253 
by (rule add_divide_distrib)


254 
also have "... = 1 + x / (1x)"


255 
apply (subst add_right_cancel)


256 
apply (insert a, simp)


257 
done


258 
finally show ?thesis .


259 
qed


260 
finally show ?thesis .


261 
qed


262 


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


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


265 
proof 


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


267 
from b have c: "x < 1"


268 
by auto


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


270 
by (rule aux5)


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


272 
proof 


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


274 
apply (rule ln_add_one_self_le_self)


275 
apply (rule divide_nonneg_pos)


276 
by (insert a c, auto)


277 
thus ?thesis


278 
by auto


279 
qed


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


281 
by auto


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


283 
have e: "x  2 * x^2 <=  x / (1  x)"


284 
apply (rule mult_imp_le_div_pos)


285 
apply (insert prems, force)


286 
apply (auto simp add: ring_eq_simps power2_eq_square)


287 
apply (subgoal_tac " (x * x) + x * (x * (x * 2)) = x^2 * (2 * x  1)")


288 
apply (erule ssubst)


289 
apply (rule mult_nonneg_nonpos)


290 
apply auto


291 
apply (auto simp add: ring_eq_simps power2_eq_square)


292 
done


293 
from e d show " x  2 * x^2 <= ln (1  x)"


294 
by (rule order_trans)


295 
qed


296 


297 
lemma exp_ge_add_one_self2: "1 + x <= exp x"


298 
apply (case_tac "0 <= x")


299 
apply (erule exp_ge_add_one_self)


300 
apply (case_tac "x <= 1")


301 
apply (subgoal_tac "1 + x <= 0")


302 
apply (erule order_trans)


303 
apply simp


304 
apply simp


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


306 
apply (erule ssubst)


307 
apply (subst exp_le_cancel_iff)


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


309 
apply simp


310 
apply (rule ln_one_minus_pos_upper_bound)


311 
apply auto


312 
apply (rule sym)


313 
apply (subst exp_ln_iff)


314 
apply auto


315 
done


316 


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


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


319 
apply (erule ssubst)back


320 
apply (subst ln_le_cancel_iff)


321 
apply auto


322 
apply (rule exp_ge_add_one_self2)


323 
done


324 


325 
lemma abs_ln_one_plus_x_minus_x_bound_nonneg:


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


327 
proof 


328 
assume "0 <= x"


329 
assume "x <= 1"


330 
have "ln (1 + x) <= x"


331 
by (rule ln_add_one_self_le_self)


332 
then have "ln (1 + x)  x <= 0"


333 
by simp


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


335 
by (rule abs_of_nonpos)


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


337 
by simp


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


339 
proof 


340 
from prems have "x  x^2 <= ln (1 + x)"


341 
by (intro ln_one_plus_pos_lower_bound)


342 
thus ?thesis


343 
by simp


344 
qed


345 
finally show ?thesis .


346 
qed


347 


348 
lemma abs_ln_one_plus_x_minus_x_bound_nonpos:


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


350 
proof 


351 
assume "(1 / 2) <= x"


352 
assume "x <= 0"


353 
have "abs(ln (1 + x)  x) = x  ln(1  (x))"


354 
apply (subst abs_of_nonpos)


355 
apply simp


356 
apply (rule ln_add_one_self_le_self2)


357 
apply (insert prems, auto)


358 
done


359 
also have "... <= 2 * x^2"


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


361 
apply (simp add: compare_rls)


362 
apply (rule ln_one_minus_pos_lower_bound)


363 
apply (insert prems, auto)


364 
done


365 
finally show ?thesis .


366 
qed


367 


368 
lemma abs_ln_one_plus_x_minus_x_bound:


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


370 
apply (case_tac "0 <= x")


371 
apply (rule order_trans)


372 
apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)


373 
apply auto


374 
apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos)


375 
apply auto


376 
done


377 


378 
lemma DERIV_ln: "0 < x ==> DERIV ln x :> 1 / x"


379 
apply (unfold deriv_def, unfold LIM_def, clarsimp)


380 
apply (rule exI)


381 
apply (rule conjI)


382 
prefer 2


383 
apply clarsimp


384 
apply (subgoal_tac "(ln (x + xa) +  ln x) / xa +  (1 / x) =


385 
(ln (1 + xa / x)  xa / x) / xa")


386 
apply (erule ssubst)


387 
apply (subst abs_divide)


388 
apply (rule mult_imp_div_pos_less)


389 
apply force


390 
apply (rule order_le_less_trans)


391 
apply (rule abs_ln_one_plus_x_minus_x_bound)


392 
apply (subst abs_divide)


393 
apply (subst abs_of_pos, assumption)


394 
apply (erule mult_imp_div_pos_le)


395 
apply (subgoal_tac "abs xa < min (x / 2) (r * x^2 / 2)")


396 
apply force


397 
apply assumption


398 
apply (simp add: power2_eq_square mult_compare_simps)


399 
apply (rule mult_imp_div_pos_less)


400 
apply (rule mult_pos_pos, assumption, assumption)


401 
apply (subgoal_tac "xa * xa = abs xa * abs xa")


402 
apply (erule ssubst)


403 
apply (subgoal_tac "abs xa * (abs xa * 2) < abs xa * (r * (x * x))")


404 
apply (simp only: mult_ac)


405 
apply (rule mult_strict_left_mono)


406 
apply (erule conjE, assumption)


407 
apply force


408 
apply simp


409 
apply (subst diff_minus [THEN sym])+


410 
apply (subst ln_div [THEN sym])


411 
apply arith


412 
apply (auto simp add: ring_eq_simps add_frac_eq frac_eq_eq


413 
add_divide_distrib power2_eq_square)


414 
apply (rule mult_pos_pos, assumption)+


415 
apply assumption


416 
done


417 


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


419 
proof 


420 
assume "exp 1 <= x" and "x <= y"


421 
have a: "0 < x" and b: "0 < y"


422 
apply (insert prems)


423 
apply (subgoal_tac "0 < exp 1")


424 
apply arith


425 
apply auto


426 
apply (subgoal_tac "0 < exp 1")


427 
apply arith


428 
apply auto


429 
done


430 
have "x * ln y  x * ln x = x * (ln y  ln x)"


431 
by (simp add: ring_eq_simps)


432 
also have "... = x * ln(y / x)"


433 
apply (subst ln_div)


434 
apply (rule b, rule a, rule refl)


435 
done


436 
also have "y / x = (x + (y  x)) / x"


437 
by simp


438 
also have "... = 1 + (y  x) / x"


439 
apply (simp only: add_divide_distrib)


440 
apply (simp add: prems)


441 
apply (insert a, arith)


442 
done


443 
also have "x * ln(1 + (y  x) / x) <= x * ((y  x) / x)"


444 
apply (rule mult_left_mono)


445 
apply (rule ln_add_one_self_le_self)


446 
apply (rule divide_nonneg_pos)


447 
apply (insert prems a, simp_all)


448 
done


449 
also have "... = y  x"


450 
by (insert a, simp)


451 
also have "... = (y  x) * ln (exp 1)"


452 
by simp


453 
also have "... <= (y  x) * ln x"


454 
apply (rule mult_left_mono)


455 
apply (subst ln_le_cancel_iff)


456 
apply force


457 
apply (rule a)


458 
apply (rule prems)


459 
apply (insert prems, simp)


460 
done


461 
also have "... = y * ln x  x * ln x"


462 
by (rule left_diff_distrib)


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


464 
by arith


465 
then have "ln y <= (y * ln x) / x"


466 
apply (subst pos_le_divide_eq)


467 
apply (rule a)


468 
apply (simp add: mult_ac)


469 
done


470 
also have "... = y * (ln x / x)"


471 
by simp


472 
finally show ?thesis


473 
apply (subst pos_divide_le_eq)


474 
apply (rule b)


475 
apply (simp add: mult_ac)


476 
done


477 
qed


478 


479 
end


480 
