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