src/HOL/Ln.thy
changeset 28952 15a4b2cf8c34
parent 27483 7c58324cd418
child 29667 53103fc8ffa3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Ln.thy	Wed Dec 03 15:58:44 2008 +0100
     1.3 @@ -0,0 +1,430 @@
     1.4 +(*  Title:      Ln.thy
     1.5 +    Author:     Jeremy Avigad
     1.6 +*)
     1.7 +
     1.8 +header {* Properties of ln *}
     1.9 +
    1.10 +theory Ln
    1.11 +imports Transcendental
    1.12 +begin
    1.13 +
    1.14 +lemma exp_first_two_terms: "exp x = 1 + x + suminf (%n. 
    1.15 +  inverse(real (fact (n+2))) * (x ^ (n+2)))"
    1.16 +proof -
    1.17 +  have "exp x = suminf (%n. inverse(real (fact n)) * (x ^ n))"
    1.18 +    by (simp add: exp_def)
    1.19 +  also from summable_exp have "... = (SUM n : {0..<2}. 
    1.20 +      inverse(real (fact n)) * (x ^ n)) + suminf (%n.
    1.21 +      inverse(real (fact (n+2))) * (x ^ (n+2)))" (is "_ = ?a + _")
    1.22 +    by (rule suminf_split_initial_segment)
    1.23 +  also have "?a = 1 + x"
    1.24 +    by (simp add: numerals)
    1.25 +  finally show ?thesis .
    1.26 +qed
    1.27 +
    1.28 +lemma exp_tail_after_first_two_terms_summable: 
    1.29 +  "summable (%n. inverse(real (fact (n+2))) * (x ^ (n+2)))"
    1.30 +proof -
    1.31 +  note summable_exp
    1.32 +  thus ?thesis
    1.33 +    by (frule summable_ignore_initial_segment)
    1.34 +qed
    1.35 +
    1.36 +lemma aux1: assumes a: "0 <= x" and b: "x <= 1"
    1.37 +    shows "inverse (real (fact (n + 2))) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"
    1.38 +proof (induct n)
    1.39 +  show "inverse (real (fact (0 + 2))) * x ^ (0 + 2) <= 
    1.40 +      x ^ 2 / 2 * (1 / 2) ^ 0"
    1.41 +    by (simp add: real_of_nat_Suc power2_eq_square)
    1.42 +next
    1.43 +  fix n
    1.44 +  assume c: "inverse (real (fact (n + 2))) * x ^ (n + 2)
    1.45 +       <= x ^ 2 / 2 * (1 / 2) ^ n"
    1.46 +  show "inverse (real (fact (Suc n + 2))) * x ^ (Suc n + 2)
    1.47 +           <= x ^ 2 / 2 * (1 / 2) ^ Suc n"
    1.48 +  proof -
    1.49 +    have "inverse(real (fact (Suc n + 2))) <= 
    1.50 +        (1 / 2) *inverse (real (fact (n+2)))"
    1.51 +    proof -
    1.52 +      have "Suc n + 2 = Suc (n + 2)" by simp
    1.53 +      then have "fact (Suc n + 2) = Suc (n + 2) * fact (n + 2)" 
    1.54 +        by simp
    1.55 +      then have "real(fact (Suc n + 2)) = real(Suc (n + 2) * fact (n + 2))" 
    1.56 +        apply (rule subst)
    1.57 +        apply (rule refl)
    1.58 +        done
    1.59 +      also have "... = real(Suc (n + 2)) * real(fact (n + 2))"
    1.60 +        by (rule real_of_nat_mult)
    1.61 +      finally have "real (fact (Suc n + 2)) = 
    1.62 +         real (Suc (n + 2)) * real (fact (n + 2))" .
    1.63 +      then have "inverse(real (fact (Suc n + 2))) = 
    1.64 +         inverse(real (Suc (n + 2))) * inverse(real (fact (n + 2)))"
    1.65 +        apply (rule ssubst)
    1.66 +        apply (rule inverse_mult_distrib)
    1.67 +        done
    1.68 +      also have "... <= (1/2) * inverse(real (fact (n + 2)))"
    1.69 +        apply (rule mult_right_mono)
    1.70 +        apply (subst inverse_eq_divide)
    1.71 +        apply simp
    1.72 +        apply (rule inv_real_of_nat_fact_ge_zero)
    1.73 +        done
    1.74 +      finally show ?thesis .
    1.75 +    qed
    1.76 +    moreover have "x ^ (Suc n + 2) <= x ^ (n + 2)"
    1.77 +      apply (simp add: mult_compare_simps)
    1.78 +      apply (simp add: prems)
    1.79 +      apply (subgoal_tac "0 <= x * (x * x^n)")
    1.80 +      apply force
    1.81 +      apply (rule mult_nonneg_nonneg, rule a)+
    1.82 +      apply (rule zero_le_power, rule a)
    1.83 +      done
    1.84 +    ultimately have "inverse (real (fact (Suc n + 2))) *  x ^ (Suc n + 2) <=
    1.85 +        (1 / 2 * inverse (real (fact (n + 2)))) * x ^ (n + 2)"
    1.86 +      apply (rule mult_mono)
    1.87 +      apply (rule mult_nonneg_nonneg)
    1.88 +      apply simp
    1.89 +      apply (subst inverse_nonnegative_iff_nonnegative)
    1.90 +      apply (rule real_of_nat_ge_zero)
    1.91 +      apply (rule zero_le_power)
    1.92 +      apply (rule a)
    1.93 +      done
    1.94 +    also have "... = 1 / 2 * (inverse (real (fact (n + 2))) * x ^ (n + 2))"
    1.95 +      by simp
    1.96 +    also have "... <= 1 / 2 * (x ^ 2 / 2 * (1 / 2) ^ n)"
    1.97 +      apply (rule mult_left_mono)
    1.98 +      apply (rule prems)
    1.99 +      apply simp
   1.100 +      done
   1.101 +    also have "... = x ^ 2 / 2 * (1 / 2 * (1 / 2) ^ n)"
   1.102 +      by auto
   1.103 +    also have "(1::real) / 2 * (1 / 2) ^ n = (1 / 2) ^ (Suc n)"
   1.104 +      by (rule realpow_Suc [THEN sym])
   1.105 +    finally show ?thesis .
   1.106 +  qed
   1.107 +qed
   1.108 +
   1.109 +lemma aux2: "(%n. (x::real) ^ 2 / 2 * (1 / 2) ^ n) sums x^2"
   1.110 +proof -
   1.111 +  have "(%n. (1 / 2::real)^n) sums (1 / (1 - (1/2)))"
   1.112 +    apply (rule geometric_sums)
   1.113 +    by (simp add: abs_less_iff)
   1.114 +  also have "(1::real) / (1 - 1/2) = 2"
   1.115 +    by simp
   1.116 +  finally have "(%n. (1 / 2::real)^n) sums 2" .
   1.117 +  then have "(%n. x ^ 2 / 2 * (1 / 2) ^ n) sums (x^2 / 2 * 2)"
   1.118 +    by (rule sums_mult)
   1.119 +  also have "x^2 / 2 * 2 = x^2"
   1.120 +    by simp
   1.121 +  finally show ?thesis .
   1.122 +qed
   1.123 +
   1.124 +lemma exp_bound: "0 <= (x::real) ==> x <= 1 ==> exp x <= 1 + x + x^2"
   1.125 +proof -
   1.126 +  assume a: "0 <= x"
   1.127 +  assume b: "x <= 1"
   1.128 +  have c: "exp x = 1 + x + suminf (%n. inverse(real (fact (n+2))) * 
   1.129 +      (x ^ (n+2)))"
   1.130 +    by (rule exp_first_two_terms)
   1.131 +  moreover have "suminf (%n. inverse(real (fact (n+2))) * (x ^ (n+2))) <= x^2"
   1.132 +  proof -
   1.133 +    have "suminf (%n. inverse(real (fact (n+2))) * (x ^ (n+2))) <=
   1.134 +        suminf (%n. (x^2/2) * ((1/2)^n))"
   1.135 +      apply (rule summable_le)
   1.136 +      apply (auto simp only: aux1 prems)
   1.137 +      apply (rule exp_tail_after_first_two_terms_summable)
   1.138 +      by (rule sums_summable, rule aux2)  
   1.139 +    also have "... = x^2"
   1.140 +      by (rule sums_unique [THEN sym], rule aux2)
   1.141 +    finally show ?thesis .
   1.142 +  qed
   1.143 +  ultimately show ?thesis
   1.144 +    by auto
   1.145 +qed
   1.146 +
   1.147 +lemma aux4: "0 <= (x::real) ==> x <= 1 ==> exp (x - x^2) <= 1 + x" 
   1.148 +proof -
   1.149 +  assume a: "0 <= x" and b: "x <= 1"
   1.150 +  have "exp (x - x^2) = exp x / exp (x^2)"
   1.151 +    by (rule exp_diff)
   1.152 +  also have "... <= (1 + x + x^2) / exp (x ^2)"
   1.153 +    apply (rule divide_right_mono) 
   1.154 +    apply (rule exp_bound)
   1.155 +    apply (rule a, rule b)
   1.156 +    apply simp
   1.157 +    done
   1.158 +  also have "... <= (1 + x + x^2) / (1 + x^2)"
   1.159 +    apply (rule divide_left_mono)
   1.160 +    apply (auto simp add: exp_ge_add_one_self_aux)
   1.161 +    apply (rule add_nonneg_nonneg)
   1.162 +    apply (insert prems, auto)
   1.163 +    apply (rule mult_pos_pos)
   1.164 +    apply auto
   1.165 +    apply (rule add_pos_nonneg)
   1.166 +    apply auto
   1.167 +    done
   1.168 +  also from a have "... <= 1 + x"
   1.169 +    by(simp add:field_simps zero_compare_simps)
   1.170 +  finally show ?thesis .
   1.171 +qed
   1.172 +
   1.173 +lemma ln_one_plus_pos_lower_bound: "0 <= x ==> x <= 1 ==> 
   1.174 +    x - x^2 <= ln (1 + x)"
   1.175 +proof -
   1.176 +  assume a: "0 <= x" and b: "x <= 1"
   1.177 +  then have "exp (x - x^2) <= 1 + x"
   1.178 +    by (rule aux4)
   1.179 +  also have "... = exp (ln (1 + x))"
   1.180 +  proof -
   1.181 +    from a have "0 < 1 + x" by auto
   1.182 +    thus ?thesis
   1.183 +      by (auto simp only: exp_ln_iff [THEN sym])
   1.184 +  qed
   1.185 +  finally have "exp (x - x ^ 2) <= exp (ln (1 + x))" .
   1.186 +  thus ?thesis by (auto simp only: exp_le_cancel_iff)
   1.187 +qed
   1.188 +
   1.189 +lemma ln_one_minus_pos_upper_bound: "0 <= x ==> x < 1 ==> ln (1 - x) <= - x"
   1.190 +proof -
   1.191 +  assume a: "0 <= (x::real)" and b: "x < 1"
   1.192 +  have "(1 - x) * (1 + x + x^2) = (1 - x^3)"
   1.193 +    by (simp add: ring_simps power2_eq_square power3_eq_cube)
   1.194 +  also have "... <= 1"
   1.195 +    by (auto simp add: a)
   1.196 +  finally have "(1 - x) * (1 + x + x ^ 2) <= 1" .
   1.197 +  moreover have "0 < 1 + x + x^2"
   1.198 +    apply (rule add_pos_nonneg)
   1.199 +    apply (insert a, auto)
   1.200 +    done
   1.201 +  ultimately have "1 - x <= 1 / (1 + x + x^2)"
   1.202 +    by (elim mult_imp_le_div_pos)
   1.203 +  also have "... <= 1 / exp x"
   1.204 +    apply (rule divide_left_mono)
   1.205 +    apply (rule exp_bound, rule a)
   1.206 +    apply (insert prems, auto)
   1.207 +    apply (rule mult_pos_pos)
   1.208 +    apply (rule add_pos_nonneg)
   1.209 +    apply auto
   1.210 +    done
   1.211 +  also have "... = exp (-x)"
   1.212 +    by (auto simp add: exp_minus real_divide_def)
   1.213 +  finally have "1 - x <= exp (- x)" .
   1.214 +  also have "1 - x = exp (ln (1 - x))"
   1.215 +  proof -
   1.216 +    have "0 < 1 - x"
   1.217 +      by (insert b, auto)
   1.218 +    thus ?thesis
   1.219 +      by (auto simp only: exp_ln_iff [THEN sym])
   1.220 +  qed
   1.221 +  finally have "exp (ln (1 - x)) <= exp (- x)" .
   1.222 +  thus ?thesis by (auto simp only: exp_le_cancel_iff)
   1.223 +qed
   1.224 +
   1.225 +lemma aux5: "x < 1 ==> ln(1 - x) = - ln(1 + x / (1 - x))"
   1.226 +proof -
   1.227 +  assume a: "x < 1"
   1.228 +  have "ln(1 - x) = - ln(1 / (1 - x))"
   1.229 +  proof -
   1.230 +    have "ln(1 - x) = - (- ln (1 - x))"
   1.231 +      by auto
   1.232 +    also have "- ln(1 - x) = ln 1 - ln(1 - x)"
   1.233 +      by simp
   1.234 +    also have "... = ln(1 / (1 - x))"
   1.235 +      apply (rule ln_div [THEN sym])
   1.236 +      by (insert a, auto)
   1.237 +    finally show ?thesis .
   1.238 +  qed
   1.239 +  also have " 1 / (1 - x) = 1 + x / (1 - x)" using a by(simp add:field_simps)
   1.240 +  finally show ?thesis .
   1.241 +qed
   1.242 +
   1.243 +lemma ln_one_minus_pos_lower_bound: "0 <= x ==> x <= (1 / 2) ==> 
   1.244 +    - x - 2 * x^2 <= ln (1 - x)"
   1.245 +proof -
   1.246 +  assume a: "0 <= x" and b: "x <= (1 / 2)"
   1.247 +  from b have c: "x < 1"
   1.248 +    by auto
   1.249 +  then have "ln (1 - x) = - ln (1 + x / (1 - x))"
   1.250 +    by (rule aux5)
   1.251 +  also have "- (x / (1 - x)) <= ..."
   1.252 +  proof - 
   1.253 +    have "ln (1 + x / (1 - x)) <= x / (1 - x)"
   1.254 +      apply (rule ln_add_one_self_le_self)
   1.255 +      apply (rule divide_nonneg_pos)
   1.256 +      by (insert a c, auto) 
   1.257 +    thus ?thesis
   1.258 +      by auto
   1.259 +  qed
   1.260 +  also have "- (x / (1 - x)) = -x / (1 - x)"
   1.261 +    by auto
   1.262 +  finally have d: "- x / (1 - x) <= ln (1 - x)" .
   1.263 +  have "0 < 1 - x" using prems by simp
   1.264 +  hence e: "-x - 2 * x^2 <= - x / (1 - x)"
   1.265 +    using mult_right_le_one_le[of "x*x" "2*x"] prems
   1.266 +    by(simp add:field_simps power2_eq_square)
   1.267 +  from e d show "- x - 2 * x^2 <= ln (1 - x)"
   1.268 +    by (rule order_trans)
   1.269 +qed
   1.270 +
   1.271 +lemma exp_ge_add_one_self [simp]: "1 + (x::real) <= exp x"
   1.272 +  apply (case_tac "0 <= x")
   1.273 +  apply (erule exp_ge_add_one_self_aux)
   1.274 +  apply (case_tac "x <= -1")
   1.275 +  apply (subgoal_tac "1 + x <= 0")
   1.276 +  apply (erule order_trans)
   1.277 +  apply simp
   1.278 +  apply simp
   1.279 +  apply (subgoal_tac "1 + x = exp(ln (1 + x))")
   1.280 +  apply (erule ssubst)
   1.281 +  apply (subst exp_le_cancel_iff)
   1.282 +  apply (subgoal_tac "ln (1 - (- x)) <= - (- x)")
   1.283 +  apply simp
   1.284 +  apply (rule ln_one_minus_pos_upper_bound) 
   1.285 +  apply auto
   1.286 +done
   1.287 +
   1.288 +lemma ln_add_one_self_le_self2: "-1 < x ==> ln(1 + x) <= x"
   1.289 +  apply (subgoal_tac "x = ln (exp x)")
   1.290 +  apply (erule ssubst)back
   1.291 +  apply (subst ln_le_cancel_iff)
   1.292 +  apply auto
   1.293 +done
   1.294 +
   1.295 +lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
   1.296 +    "0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x^2"
   1.297 +proof -
   1.298 +  assume x: "0 <= x"
   1.299 +  assume "x <= 1"
   1.300 +  from x have "ln (1 + x) <= x"
   1.301 +    by (rule ln_add_one_self_le_self)
   1.302 +  then have "ln (1 + x) - x <= 0" 
   1.303 +    by simp
   1.304 +  then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)"
   1.305 +    by (rule abs_of_nonpos)
   1.306 +  also have "... = x - ln (1 + x)" 
   1.307 +    by simp
   1.308 +  also have "... <= x^2"
   1.309 +  proof -
   1.310 +    from prems have "x - x^2 <= ln (1 + x)"
   1.311 +      by (intro ln_one_plus_pos_lower_bound)
   1.312 +    thus ?thesis
   1.313 +      by simp
   1.314 +  qed
   1.315 +  finally show ?thesis .
   1.316 +qed
   1.317 +
   1.318 +lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
   1.319 +    "-(1 / 2) <= x ==> x <= 0 ==> abs(ln (1 + x) - x) <= 2 * x^2"
   1.320 +proof -
   1.321 +  assume "-(1 / 2) <= x"
   1.322 +  assume "x <= 0"
   1.323 +  have "abs(ln (1 + x) - x) = x - ln(1 - (-x))" 
   1.324 +    apply (subst abs_of_nonpos)
   1.325 +    apply simp
   1.326 +    apply (rule ln_add_one_self_le_self2)
   1.327 +    apply (insert prems, auto)
   1.328 +    done
   1.329 +  also have "... <= 2 * x^2"
   1.330 +    apply (subgoal_tac "- (-x) - 2 * (-x)^2 <= ln (1 - (-x))")
   1.331 +    apply (simp add: compare_rls)
   1.332 +    apply (rule ln_one_minus_pos_lower_bound)
   1.333 +    apply (insert prems, auto)
   1.334 +    done 
   1.335 +  finally show ?thesis .
   1.336 +qed
   1.337 +
   1.338 +lemma abs_ln_one_plus_x_minus_x_bound:
   1.339 +    "abs x <= 1 / 2 ==> abs(ln (1 + x) - x) <= 2 * x^2"
   1.340 +  apply (case_tac "0 <= x")
   1.341 +  apply (rule order_trans)
   1.342 +  apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)
   1.343 +  apply auto
   1.344 +  apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos)
   1.345 +  apply auto
   1.346 +done
   1.347 +
   1.348 +lemma DERIV_ln: "0 < x ==> DERIV ln x :> 1 / x"
   1.349 +  apply (unfold deriv_def, unfold LIM_def, clarsimp)
   1.350 +  apply (rule exI)
   1.351 +  apply (rule conjI)
   1.352 +  prefer 2
   1.353 +  apply clarsimp
   1.354 +  apply (subgoal_tac "(ln (x + xa) - ln x) / xa - (1 / x) = 
   1.355 +      (ln (1 + xa / x) - xa / x) / xa")
   1.356 +  apply (erule ssubst)
   1.357 +  apply (subst abs_divide)
   1.358 +  apply (rule mult_imp_div_pos_less)
   1.359 +  apply force
   1.360 +  apply (rule order_le_less_trans)
   1.361 +  apply (rule abs_ln_one_plus_x_minus_x_bound)
   1.362 +  apply (subst abs_divide)
   1.363 +  apply (subst abs_of_pos, assumption)
   1.364 +  apply (erule mult_imp_div_pos_le)
   1.365 +  apply (subgoal_tac "abs xa < min (x / 2) (r * x^2 / 2)")
   1.366 +  apply force
   1.367 +  apply assumption
   1.368 +  apply (simp add: power2_eq_square mult_compare_simps)
   1.369 +  apply (rule mult_imp_div_pos_less)
   1.370 +  apply (rule mult_pos_pos, assumption, assumption)
   1.371 +  apply (subgoal_tac "xa * xa = abs xa * abs xa")
   1.372 +  apply (erule ssubst)
   1.373 +  apply (subgoal_tac "abs xa * (abs xa * 2) < abs xa * (r * (x * x))")
   1.374 +  apply (simp only: mult_ac)
   1.375 +  apply (rule mult_strict_left_mono)
   1.376 +  apply (erule conjE, assumption)
   1.377 +  apply force
   1.378 +  apply simp
   1.379 +  apply (subst ln_div [THEN sym])
   1.380 +  apply arith
   1.381 +  apply (auto simp add: ring_simps add_frac_eq frac_eq_eq 
   1.382 +    add_divide_distrib power2_eq_square)
   1.383 +  apply (rule mult_pos_pos, assumption)+
   1.384 +  apply assumption
   1.385 +done
   1.386 +
   1.387 +lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"  
   1.388 +proof -
   1.389 +  assume "exp 1 <= x" and "x <= y"
   1.390 +  have a: "0 < x" and b: "0 < y"
   1.391 +    apply (insert prems)
   1.392 +    apply (subgoal_tac "0 < exp (1::real)")
   1.393 +    apply arith
   1.394 +    apply auto
   1.395 +    apply (subgoal_tac "0 < exp (1::real)")
   1.396 +    apply arith
   1.397 +    apply auto
   1.398 +    done
   1.399 +  have "x * ln y - x * ln x = x * (ln y - ln x)"
   1.400 +    by (simp add: ring_simps)
   1.401 +  also have "... = x * ln(y / x)"
   1.402 +    apply (subst ln_div)
   1.403 +    apply (rule b, rule a, rule refl)
   1.404 +    done
   1.405 +  also have "y / x = (x + (y - x)) / x"
   1.406 +    by simp
   1.407 +  also have "... = 1 + (y - x) / x" using a prems by(simp add:field_simps)
   1.408 +  also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
   1.409 +    apply (rule mult_left_mono)
   1.410 +    apply (rule ln_add_one_self_le_self)
   1.411 +    apply (rule divide_nonneg_pos)
   1.412 +    apply (insert prems a, simp_all) 
   1.413 +    done
   1.414 +  also have "... = y - x" using a by simp
   1.415 +  also have "... = (y - x) * ln (exp 1)" by simp
   1.416 +  also have "... <= (y - x) * ln x"
   1.417 +    apply (rule mult_left_mono)
   1.418 +    apply (subst ln_le_cancel_iff)
   1.419 +    apply force
   1.420 +    apply (rule a)
   1.421 +    apply (rule prems)
   1.422 +    apply (insert prems, simp)
   1.423 +    done
   1.424 +  also have "... = y * ln x - x * ln x"
   1.425 +    by (rule left_diff_distrib)
   1.426 +  finally have "x * ln y <= y * ln x"
   1.427 +    by arith
   1.428 +  then have "ln y <= (y * ln x) / x" using a by(simp add:field_simps)
   1.429 +  also have "... = y * (ln x / x)"  by simp
   1.430 +  finally show ?thesis using b by(simp add:field_simps)
   1.431 +qed
   1.432 +
   1.433 +end