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