author hoelzl Thu Jun 09 11:50:16 2011 +0200 (2011-06-09) changeset 43336 05aa7380f7fc parent 43335 9f8766a8ebe0 child 43337 57a1c19f8e3b
lemmas relating ln x and x - 1
 src/HOL/Ln.thy file | annotate | diff | revisions
1.1 --- a/src/HOL/Ln.thy	Tue May 31 21:33:49 2011 +0200
1.2 +++ b/src/HOL/Ln.thy	Thu Jun 09 11:50:16 2011 +0200
1.3 @@ -387,4 +387,47 @@
1.4    finally show ?thesis using b by (simp add: field_simps)
1.5  qed
1.7 +lemma ln_le_minus_one:
1.8 +  "0 < x \<Longrightarrow> ln x \<le> x - 1"
1.9 +  using exp_ge_add_one_self[of "ln x"] by simp
1.10 +
1.11 +lemma ln_eq_minus_one:
1.12 +  assumes "0 < x" "ln x = x - 1" shows "x = 1"
1.13 +proof -
1.14 +  let "?l y" = "ln y - y + 1"
1.15 +  have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
1.16 +    by (auto intro!: DERIV_intros)
1.17 +
1.18 +  show ?thesis
1.19 +  proof (cases rule: linorder_cases)
1.20 +    assume "x < 1"
1.21 +    from dense[OF `x < 1`] obtain a where "x < a" "a < 1" by blast
1.22 +    from `x < a` have "?l x < ?l a"
1.23 +    proof (rule DERIV_pos_imp_increasing, safe)
1.24 +      fix y assume "x \<le> y" "y \<le> a"
1.25 +      with `0 < x` `a < 1` have "0 < 1 / y - 1" "0 < y"
1.26 +        by (auto simp: field_simps)
1.27 +      with D show "\<exists>z. DERIV ?l y :> z \<and> 0 < z"
1.28 +        by auto
1.29 +    qed
1.30 +    also have "\<dots> \<le> 0"
1.31 +      using ln_le_minus_one `0 < x` `x < a` by (auto simp: field_simps)
1.32 +    finally show "x = 1" using assms by auto
1.33 +  next
1.34 +    assume "1 < x"
1.35 +    from dense[OF `1 < x`] obtain a where "1 < a" "a < x" by blast
1.36 +    from `a < x` have "?l x < ?l a"
1.37 +    proof (rule DERIV_neg_imp_decreasing, safe)
1.38 +      fix y assume "a \<le> y" "y \<le> x"
1.39 +      with `1 < a` have "1 / y - 1 < 0" "0 < y"
1.40 +        by (auto simp: field_simps)
1.41 +      with D show "\<exists>z. DERIV ?l y :> z \<and> z < 0"
1.42 +        by blast
1.43 +    qed
1.44 +    also have "\<dots> \<le> 0"
1.45 +      using ln_le_minus_one `1 < a` by (auto simp: field_simps)
1.46 +    finally show "x = 1" using assms by auto
1.47 +  qed simp
1.48 +qed
1.49 +
1.50  end