src/HOL/Ln.thy
 author hoelzl Fri Mar 22 10:41:43 2013 +0100 (2013-03-22) changeset 51474 1e9e68247ad1 parent 50326 b5afeccab2db permissions -rw-r--r--
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
```     1 (*  Title:      HOL/Ln.thy
```
```     2     Author:     Jeremy Avigad
```
```     3 *)
```
```     4
```
```     5 header {* Properties of ln *}
```
```     6
```
```     7 theory Ln
```
```     8 imports Transcendental
```
```     9 begin
```
```    10
```
```    11 lemma ln_one_plus_pos_lower_bound: "0 <= x ==> x <= 1 ==>
```
```    12     x - x^2 <= ln (1 + x)"
```
```    13 proof -
```
```    14   assume a: "0 <= x" and b: "x <= 1"
```
```    15   have "exp (x - x^2) = exp x / exp (x^2)"
```
```    16     by (rule exp_diff)
```
```    17   also have "... <= (1 + x + x^2) / exp (x ^2)"
```
```    18     apply (rule divide_right_mono)
```
```    19     apply (rule exp_bound)
```
```    20     apply (rule a, rule b)
```
```    21     apply simp
```
```    22     done
```
```    23   also have "... <= (1 + x + x^2) / (1 + x^2)"
```
```    24     apply (rule divide_left_mono)
```
```    25     apply (simp add: exp_ge_add_one_self_aux)
```
```    26     apply (simp add: a)
```
```    27     apply (simp add: mult_pos_pos add_pos_nonneg)
```
```    28     done
```
```    29   also from a have "... <= 1 + x"
```
```    30     by (simp add: field_simps add_strict_increasing zero_le_mult_iff)
```
```    31   finally have "exp (x - x^2) <= 1 + x" .
```
```    32   also have "... = exp (ln (1 + x))"
```
```    33   proof -
```
```    34     from a have "0 < 1 + x" by auto
```
```    35     thus ?thesis
```
```    36       by (auto simp only: exp_ln_iff [THEN sym])
```
```    37   qed
```
```    38   finally have "exp (x - x ^ 2) <= exp (ln (1 + x))" .
```
```    39   thus ?thesis by (auto simp only: exp_le_cancel_iff)
```
```    40 qed
```
```    41
```
```    42 lemma aux5: "x < 1 ==> ln(1 - x) = - ln(1 + x / (1 - x))"
```
```    43 proof -
```
```    44   assume a: "x < 1"
```
```    45   have "ln(1 - x) = - ln(1 / (1 - x))"
```
```    46   proof -
```
```    47     have "ln(1 - x) = - (- ln (1 - x))"
```
```    48       by auto
```
```    49     also have "- ln(1 - x) = ln 1 - ln(1 - x)"
```
```    50       by simp
```
```    51     also have "... = ln(1 / (1 - x))"
```
```    52       apply (rule ln_div [THEN sym])
```
```    53       by (insert a, auto)
```
```    54     finally show ?thesis .
```
```    55   qed
```
```    56   also have " 1 / (1 - x) = 1 + x / (1 - x)" using a by(simp add:field_simps)
```
```    57   finally show ?thesis .
```
```    58 qed
```
```    59
```
```    60 lemma ln_one_minus_pos_lower_bound: "0 <= x ==> x <= (1 / 2) ==>
```
```    61     - x - 2 * x^2 <= ln (1 - x)"
```
```    62 proof -
```
```    63   assume a: "0 <= x" and b: "x <= (1 / 2)"
```
```    64   from b have c: "x < 1"
```
```    65     by auto
```
```    66   then have "ln (1 - x) = - ln (1 + x / (1 - x))"
```
```    67     by (rule aux5)
```
```    68   also have "- (x / (1 - x)) <= ..."
```
```    69   proof -
```
```    70     have "ln (1 + x / (1 - x)) <= x / (1 - x)"
```
```    71       apply (rule ln_add_one_self_le_self)
```
```    72       apply (rule divide_nonneg_pos)
```
```    73       by (insert a c, auto)
```
```    74     thus ?thesis
```
```    75       by auto
```
```    76   qed
```
```    77   also have "- (x / (1 - x)) = -x / (1 - x)"
```
```    78     by auto
```
```    79   finally have d: "- x / (1 - x) <= ln (1 - x)" .
```
```    80   have "0 < 1 - x" using a b by simp
```
```    81   hence e: "-x - 2 * x^2 <= - x / (1 - x)"
```
```    82     using mult_right_le_one_le[of "x*x" "2*x"] a b
```
```    83     by (simp add:field_simps power2_eq_square)
```
```    84   from e d show "- x - 2 * x^2 <= ln (1 - x)"
```
```    85     by (rule order_trans)
```
```    86 qed
```
```    87
```
```    88 lemma ln_add_one_self_le_self2: "-1 < x ==> ln(1 + x) <= x"
```
```    89   apply (subgoal_tac "ln (1 + x) \<le> ln (exp x)", simp)
```
```    90   apply (subst ln_le_cancel_iff)
```
```    91   apply auto
```
```    92 done
```
```    93
```
```    94 lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
```
```    95     "0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x^2"
```
```    96 proof -
```
```    97   assume x: "0 <= x"
```
```    98   assume x1: "x <= 1"
```
```    99   from x have "ln (1 + x) <= x"
```
```   100     by (rule ln_add_one_self_le_self)
```
```   101   then have "ln (1 + x) - x <= 0"
```
```   102     by simp
```
```   103   then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)"
```
```   104     by (rule abs_of_nonpos)
```
```   105   also have "... = x - ln (1 + x)"
```
```   106     by simp
```
```   107   also have "... <= x^2"
```
```   108   proof -
```
```   109     from x x1 have "x - x^2 <= ln (1 + x)"
```
```   110       by (intro ln_one_plus_pos_lower_bound)
```
```   111     thus ?thesis
```
```   112       by simp
```
```   113   qed
```
```   114   finally show ?thesis .
```
```   115 qed
```
```   116
```
```   117 lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
```
```   118     "-(1 / 2) <= x ==> x <= 0 ==> abs(ln (1 + x) - x) <= 2 * x^2"
```
```   119 proof -
```
```   120   assume a: "-(1 / 2) <= x"
```
```   121   assume b: "x <= 0"
```
```   122   have "abs(ln (1 + x) - x) = x - ln(1 - (-x))"
```
```   123     apply (subst abs_of_nonpos)
```
```   124     apply simp
```
```   125     apply (rule ln_add_one_self_le_self2)
```
```   126     using a apply auto
```
```   127     done
```
```   128   also have "... <= 2 * x^2"
```
```   129     apply (subgoal_tac "- (-x) - 2 * (-x)^2 <= ln (1 - (-x))")
```
```   130     apply (simp add: algebra_simps)
```
```   131     apply (rule ln_one_minus_pos_lower_bound)
```
```   132     using a b apply auto
```
```   133     done
```
```   134   finally show ?thesis .
```
```   135 qed
```
```   136
```
```   137 lemma abs_ln_one_plus_x_minus_x_bound:
```
```   138     "abs x <= 1 / 2 ==> abs(ln (1 + x) - x) <= 2 * x^2"
```
```   139   apply (case_tac "0 <= x")
```
```   140   apply (rule order_trans)
```
```   141   apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)
```
```   142   apply auto
```
```   143   apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos)
```
```   144   apply auto
```
```   145 done
```
```   146
```
```   147 lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"
```
```   148 proof -
```
```   149   assume x: "exp 1 <= x" "x <= y"
```
```   150   moreover have "0 < exp (1::real)" by simp
```
```   151   ultimately have a: "0 < x" and b: "0 < y"
```
```   152     by (fast intro: less_le_trans order_trans)+
```
```   153   have "x * ln y - x * ln x = x * (ln y - ln x)"
```
```   154     by (simp add: algebra_simps)
```
```   155   also have "... = x * ln(y / x)"
```
```   156     by (simp only: ln_div a b)
```
```   157   also have "y / x = (x + (y - x)) / x"
```
```   158     by simp
```
```   159   also have "... = 1 + (y - x) / x"
```
```   160     using x a by (simp add: field_simps)
```
```   161   also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
```
```   162     apply (rule mult_left_mono)
```
```   163     apply (rule ln_add_one_self_le_self)
```
```   164     apply (rule divide_nonneg_pos)
```
```   165     using x a apply simp_all
```
```   166     done
```
```   167   also have "... = y - x" using a by simp
```
```   168   also have "... = (y - x) * ln (exp 1)" by simp
```
```   169   also have "... <= (y - x) * ln x"
```
```   170     apply (rule mult_left_mono)
```
```   171     apply (subst ln_le_cancel_iff)
```
```   172     apply fact
```
```   173     apply (rule a)
```
```   174     apply (rule x)
```
```   175     using x apply simp
```
```   176     done
```
```   177   also have "... = y * ln x - x * ln x"
```
```   178     by (rule left_diff_distrib)
```
```   179   finally have "x * ln y <= y * ln x"
```
```   180     by arith
```
```   181   then have "ln y <= (y * ln x) / x" using a by (simp add: field_simps)
```
```   182   also have "... = y * (ln x / x)" by simp
```
```   183   finally show ?thesis using b by (simp add: field_simps)
```
```   184 qed
```
```   185
```
```   186 lemma ln_le_minus_one:
```
```   187   "0 < x \<Longrightarrow> ln x \<le> x - 1"
```
```   188   using exp_ge_add_one_self[of "ln x"] by simp
```
```   189
```
```   190 lemma ln_eq_minus_one:
```
```   191   assumes "0 < x" "ln x = x - 1" shows "x = 1"
```
```   192 proof -
```
```   193   let "?l y" = "ln y - y + 1"
```
```   194   have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
```
```   195     by (auto intro!: DERIV_intros)
```
```   196
```
```   197   show ?thesis
```
```   198   proof (cases rule: linorder_cases)
```
```   199     assume "x < 1"
```
```   200     from dense[OF `x < 1`] obtain a where "x < a" "a < 1" by blast
```
```   201     from `x < a` have "?l x < ?l a"
```
```   202     proof (rule DERIV_pos_imp_increasing, safe)
```
```   203       fix y assume "x \<le> y" "y \<le> a"
```
```   204       with `0 < x` `a < 1` have "0 < 1 / y - 1" "0 < y"
```
```   205         by (auto simp: field_simps)
```
```   206       with D show "\<exists>z. DERIV ?l y :> z \<and> 0 < z"
```
```   207         by auto
```
```   208     qed
```
```   209     also have "\<dots> \<le> 0"
```
```   210       using ln_le_minus_one `0 < x` `x < a` by (auto simp: field_simps)
```
```   211     finally show "x = 1" using assms by auto
```
```   212   next
```
```   213     assume "1 < x"
```
```   214     from dense[OF `1 < x`] obtain a where "1 < a" "a < x" by blast
```
```   215     from `a < x` have "?l x < ?l a"
```
```   216     proof (rule DERIV_neg_imp_decreasing, safe)
```
```   217       fix y assume "a \<le> y" "y \<le> x"
```
```   218       with `1 < a` have "1 / y - 1 < 0" "0 < y"
```
```   219         by (auto simp: field_simps)
```
```   220       with D show "\<exists>z. DERIV ?l y :> z \<and> z < 0"
```
```   221         by blast
```
```   222     qed
```
```   223     also have "\<dots> \<le> 0"
```
```   224       using ln_le_minus_one `1 < a` by (auto simp: field_simps)
```
```   225     finally show "x = 1" using assms by auto
```
```   226   qed simp
```
```   227 qed
```
```   228
```
```   229 end
```