src/HOL/Ln.thy
 author huffman Sun May 09 17:47:43 2010 -0700 (2010-05-09) changeset 36777 be5461582d0f parent 33667 958dc9f03611 child 40864 4abaaadfdaf2 permissions -rw-r--r--
avoid using real-specific versions of generic lemmas
1 (*  Title:      Ln.thy
2     Author:     Jeremy Avigad
3 *)
5 header {* Properties of ln *}
7 theory Ln
8 imports Transcendental
9 begin
11 lemma exp_first_two_terms: "exp x = 1 + x + suminf (%n.
12   inverse(real (fact (n+2))) * (x ^ (n+2)))"
13 proof -
14   have "exp x = suminf (%n. inverse(real (fact n)) * (x ^ n))"
15     by (simp add: exp_def)
16   also from summable_exp have "... = (SUM n : {0..<2}.
17       inverse(real (fact n)) * (x ^ n)) + suminf (%n.
18       inverse(real (fact (n+2))) * (x ^ (n+2)))" (is "_ = ?a + _")
19     by (rule suminf_split_initial_segment)
20   also have "?a = 1 + x"
21     by (simp add: numerals)
22   finally show ?thesis .
23 qed
25 lemma exp_tail_after_first_two_terms_summable:
26   "summable (%n. inverse(real (fact (n+2))) * (x ^ (n+2)))"
27 proof -
28   note summable_exp
29   thus ?thesis
30     by (frule summable_ignore_initial_segment)
31 qed
33 lemma aux1: assumes a: "0 <= x" and b: "x <= 1"
34     shows "inverse (real (fact ((n::nat) + 2))) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)"
35 proof (induct n)
36   show "inverse (real (fact ((0::nat) + 2))) * x ^ (0 + 2) <=
37       x ^ 2 / 2 * (1 / 2) ^ 0"
38     by (simp add: real_of_nat_Suc power2_eq_square)
39 next
40   fix n :: nat
41   assume c: "inverse (real (fact (n + 2))) * x ^ (n + 2)
42        <= x ^ 2 / 2 * (1 / 2) ^ n"
43   show "inverse (real (fact (Suc n + 2))) * x ^ (Suc n + 2)
44            <= x ^ 2 / 2 * (1 / 2) ^ Suc n"
45   proof -
46     have "inverse(real (fact (Suc n + 2))) <=
47         (1 / 2) *inverse (real (fact (n+2)))"
48     proof -
49       have "Suc n + 2 = Suc (n + 2)" by simp
50       then have "fact (Suc n + 2) = Suc (n + 2) * fact (n + 2)"
51         by simp
52       then have "real(fact (Suc n + 2)) = real(Suc (n + 2) * fact (n + 2))"
53         apply (rule subst)
54         apply (rule refl)
55         done
56       also have "... = real(Suc (n + 2)) * real(fact (n + 2))"
57         by (rule real_of_nat_mult)
58       finally have "real (fact (Suc n + 2)) =
59          real (Suc (n + 2)) * real (fact (n + 2))" .
60       then have "inverse(real (fact (Suc n + 2))) =
61          inverse(real (Suc (n + 2))) * inverse(real (fact (n + 2)))"
62         apply (rule ssubst)
63         apply (rule inverse_mult_distrib)
64         done
65       also have "... <= (1/2) * inverse(real (fact (n + 2)))"
66         apply (rule mult_right_mono)
67         apply (subst inverse_eq_divide)
68         apply simp
69         apply (rule inv_real_of_nat_fact_ge_zero)
70         done
71       finally show ?thesis .
72     qed
73     moreover have "x ^ (Suc n + 2) <= x ^ (n + 2)"
74       apply (simp add: mult_compare_simps)
75       apply (simp add: prems)
76       apply (subgoal_tac "0 <= x * (x * x^n)")
77       apply force
78       apply (rule mult_nonneg_nonneg, rule a)+
79       apply (rule zero_le_power, rule a)
80       done
81     ultimately have "inverse (real (fact (Suc n + 2))) *  x ^ (Suc n + 2) <=
82         (1 / 2 * inverse (real (fact (n + 2)))) * x ^ (n + 2)"
83       apply (rule mult_mono)
84       apply (rule mult_nonneg_nonneg)
85       apply simp
86       apply (subst inverse_nonnegative_iff_nonnegative)
87       apply (rule real_of_nat_ge_zero)
88       apply (rule zero_le_power)
89       apply (rule a)
90       done
91     also have "... = 1 / 2 * (inverse (real (fact (n + 2))) * x ^ (n + 2))"
92       by simp
93     also have "... <= 1 / 2 * (x ^ 2 / 2 * (1 / 2) ^ n)"
94       apply (rule mult_left_mono)
95       apply (rule prems)
96       apply simp
97       done
98     also have "... = x ^ 2 / 2 * (1 / 2 * (1 / 2) ^ n)"
99       by auto
100     also have "(1::real) / 2 * (1 / 2) ^ n = (1 / 2) ^ (Suc n)"
101       by (rule power_Suc [THEN sym])
102     finally show ?thesis .
103   qed
104 qed
106 lemma aux2: "(%n. (x::real) ^ 2 / 2 * (1 / 2) ^ n) sums x^2"
107 proof -
108   have "(%n. (1 / 2::real)^n) sums (1 / (1 - (1/2)))"
109     apply (rule geometric_sums)
110     by (simp add: abs_less_iff)
111   also have "(1::real) / (1 - 1/2) = 2"
112     by simp
113   finally have "(%n. (1 / 2::real)^n) sums 2" .
114   then have "(%n. x ^ 2 / 2 * (1 / 2) ^ n) sums (x^2 / 2 * 2)"
115     by (rule sums_mult)
116   also have "x^2 / 2 * 2 = x^2"
117     by simp
118   finally show ?thesis .
119 qed
121 lemma exp_bound: "0 <= (x::real) ==> x <= 1 ==> exp x <= 1 + x + x^2"
122 proof -
123   assume a: "0 <= x"
124   assume b: "x <= 1"
125   have c: "exp x = 1 + x + suminf (%n. inverse(real (fact (n+2))) *
126       (x ^ (n+2)))"
127     by (rule exp_first_two_terms)
128   moreover have "suminf (%n. inverse(real (fact (n+2))) * (x ^ (n+2))) <= x^2"
129   proof -
130     have "suminf (%n. inverse(real (fact (n+2))) * (x ^ (n+2))) <=
131         suminf (%n. (x^2/2) * ((1/2)^n))"
132       apply (rule summable_le)
133       apply (auto simp only: aux1 prems)
134       apply (rule exp_tail_after_first_two_terms_summable)
135       by (rule sums_summable, rule aux2)
136     also have "... = x^2"
137       by (rule sums_unique [THEN sym], rule aux2)
138     finally show ?thesis .
139   qed
140   ultimately show ?thesis
141     by auto
142 qed
144 lemma aux4: "0 <= (x::real) ==> x <= 1 ==> exp (x - x^2) <= 1 + x"
145 proof -
146   assume a: "0 <= x" and b: "x <= 1"
147   have "exp (x - x^2) = exp x / exp (x^2)"
148     by (rule exp_diff)
149   also have "... <= (1 + x + x^2) / exp (x ^2)"
150     apply (rule divide_right_mono)
151     apply (rule exp_bound)
152     apply (rule a, rule b)
153     apply simp
154     done
155   also have "... <= (1 + x + x^2) / (1 + x^2)"
156     apply (rule divide_left_mono)
158     apply (rule add_nonneg_nonneg)
159     apply (insert prems, auto)
160     apply (rule mult_pos_pos)
161     apply auto
162     apply (rule add_pos_nonneg)
163     apply auto
164     done
165   also from a have "... <= 1 + x"
166     by(simp add:field_simps zero_compare_simps)
167   finally show ?thesis .
168 qed
170 lemma ln_one_plus_pos_lower_bound: "0 <= x ==> x <= 1 ==>
171     x - x^2 <= ln (1 + x)"
172 proof -
173   assume a: "0 <= x" and b: "x <= 1"
174   then have "exp (x - x^2) <= 1 + x"
175     by (rule aux4)
176   also have "... = exp (ln (1 + x))"
177   proof -
178     from a have "0 < 1 + x" by auto
179     thus ?thesis
180       by (auto simp only: exp_ln_iff [THEN sym])
181   qed
182   finally have "exp (x - x ^ 2) <= exp (ln (1 + x))" .
183   thus ?thesis by (auto simp only: exp_le_cancel_iff)
184 qed
186 lemma ln_one_minus_pos_upper_bound: "0 <= x ==> x < 1 ==> ln (1 - x) <= - x"
187 proof -
188   assume a: "0 <= (x::real)" and b: "x < 1"
189   have "(1 - x) * (1 + x + x^2) = (1 - x^3)"
190     by (simp add: algebra_simps power2_eq_square power3_eq_cube)
191   also have "... <= 1"
192     by (auto simp add: a)
193   finally have "(1 - x) * (1 + x + x ^ 2) <= 1" .
194   moreover have "0 < 1 + x + x^2"
195     apply (rule add_pos_nonneg)
196     apply (insert a, auto)
197     done
198   ultimately have "1 - x <= 1 / (1 + x + x^2)"
199     by (elim mult_imp_le_div_pos)
200   also have "... <= 1 / exp x"
201     apply (rule divide_left_mono)
202     apply (rule exp_bound, rule a)
203     apply (insert prems, auto)
204     apply (rule mult_pos_pos)
205     apply (rule add_pos_nonneg)
206     apply auto
207     done
208   also have "... = exp (-x)"
209     by (auto simp add: exp_minus divide_inverse)
210   finally have "1 - x <= exp (- x)" .
211   also have "1 - x = exp (ln (1 - x))"
212   proof -
213     have "0 < 1 - x"
214       by (insert b, auto)
215     thus ?thesis
216       by (auto simp only: exp_ln_iff [THEN sym])
217   qed
218   finally have "exp (ln (1 - x)) <= exp (- x)" .
219   thus ?thesis by (auto simp only: exp_le_cancel_iff)
220 qed
222 lemma aux5: "x < 1 ==> ln(1 - x) = - ln(1 + x / (1 - x))"
223 proof -
224   assume a: "x < 1"
225   have "ln(1 - x) = - ln(1 / (1 - x))"
226   proof -
227     have "ln(1 - x) = - (- ln (1 - x))"
228       by auto
229     also have "- ln(1 - x) = ln 1 - ln(1 - x)"
230       by simp
231     also have "... = ln(1 / (1 - x))"
232       apply (rule ln_div [THEN sym])
233       by (insert a, auto)
234     finally show ?thesis .
235   qed
236   also have " 1 / (1 - x) = 1 + x / (1 - x)" using a by(simp add:field_simps)
237   finally show ?thesis .
238 qed
240 lemma ln_one_minus_pos_lower_bound: "0 <= x ==> x <= (1 / 2) ==>
241     - x - 2 * x^2 <= ln (1 - x)"
242 proof -
243   assume a: "0 <= x" and b: "x <= (1 / 2)"
244   from b have c: "x < 1"
245     by auto
246   then have "ln (1 - x) = - ln (1 + x / (1 - x))"
247     by (rule aux5)
248   also have "- (x / (1 - x)) <= ..."
249   proof -
250     have "ln (1 + x / (1 - x)) <= x / (1 - x)"
251       apply (rule ln_add_one_self_le_self)
252       apply (rule divide_nonneg_pos)
253       by (insert a c, auto)
254     thus ?thesis
255       by auto
256   qed
257   also have "- (x / (1 - x)) = -x / (1 - x)"
258     by auto
259   finally have d: "- x / (1 - x) <= ln (1 - x)" .
260   have "0 < 1 - x" using prems by simp
261   hence e: "-x - 2 * x^2 <= - x / (1 - x)"
262     using mult_right_le_one_le[of "x*x" "2*x"] prems
263     by(simp add:field_simps power2_eq_square)
264   from e d show "- x - 2 * x^2 <= ln (1 - x)"
265     by (rule order_trans)
266 qed
268 lemma exp_ge_add_one_self [simp]: "1 + (x::real) <= exp x"
269   apply (case_tac "0 <= x")
270   apply (erule exp_ge_add_one_self_aux)
271   apply (case_tac "x <= -1")
272   apply (subgoal_tac "1 + x <= 0")
273   apply (erule order_trans)
274   apply simp
275   apply simp
276   apply (subgoal_tac "1 + x = exp(ln (1 + x))")
277   apply (erule ssubst)
278   apply (subst exp_le_cancel_iff)
279   apply (subgoal_tac "ln (1 - (- x)) <= - (- x)")
280   apply simp
281   apply (rule ln_one_minus_pos_upper_bound)
282   apply auto
283 done
285 lemma ln_add_one_self_le_self2: "-1 < x ==> ln(1 + x) <= x"
286   apply (subgoal_tac "x = ln (exp x)")
287   apply (erule ssubst)back
288   apply (subst ln_le_cancel_iff)
289   apply auto
290 done
292 lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
293     "0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x^2"
294 proof -
295   assume x: "0 <= x"
296   assume "x <= 1"
297   from x have "ln (1 + x) <= x"
298     by (rule ln_add_one_self_le_self)
299   then have "ln (1 + x) - x <= 0"
300     by simp
301   then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)"
302     by (rule abs_of_nonpos)
303   also have "... = x - ln (1 + x)"
304     by simp
305   also have "... <= x^2"
306   proof -
307     from prems have "x - x^2 <= ln (1 + x)"
308       by (intro ln_one_plus_pos_lower_bound)
309     thus ?thesis
310       by simp
311   qed
312   finally show ?thesis .
313 qed
315 lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
316     "-(1 / 2) <= x ==> x <= 0 ==> abs(ln (1 + x) - x) <= 2 * x^2"
317 proof -
318   assume "-(1 / 2) <= x"
319   assume "x <= 0"
320   have "abs(ln (1 + x) - x) = x - ln(1 - (-x))"
321     apply (subst abs_of_nonpos)
322     apply simp
323     apply (rule ln_add_one_self_le_self2)
324     apply (insert prems, auto)
325     done
326   also have "... <= 2 * x^2"
327     apply (subgoal_tac "- (-x) - 2 * (-x)^2 <= ln (1 - (-x))")
328     apply (simp add: algebra_simps)
329     apply (rule ln_one_minus_pos_lower_bound)
330     apply (insert prems, auto)
331     done
332   finally show ?thesis .
333 qed
335 lemma abs_ln_one_plus_x_minus_x_bound:
336     "abs x <= 1 / 2 ==> abs(ln (1 + x) - x) <= 2 * x^2"
337   apply (case_tac "0 <= x")
338   apply (rule order_trans)
339   apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)
340   apply auto
341   apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos)
342   apply auto
343 done
345 lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"
346 proof -
347   assume "exp 1 <= x" and "x <= y"
348   have a: "0 < x" and b: "0 < y"
349     apply (insert prems)
350     apply (subgoal_tac "0 < exp (1::real)")
351     apply arith
352     apply auto
353     apply (subgoal_tac "0 < exp (1::real)")
354     apply arith
355     apply auto
356     done
357   have "x * ln y - x * ln x = x * (ln y - ln x)"
358     by (simp add: algebra_simps)
359   also have "... = x * ln(y / x)"
360     apply (subst ln_div)
361     apply (rule b, rule a, rule refl)
362     done
363   also have "y / x = (x + (y - x)) / x"
364     by simp
365   also have "... = 1 + (y - x) / x" using a prems by(simp add:field_simps)
366   also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
367     apply (rule mult_left_mono)
368     apply (rule ln_add_one_self_le_self)
369     apply (rule divide_nonneg_pos)
370     apply (insert prems a, simp_all)
371     done
372   also have "... = y - x" using a by simp
373   also have "... = (y - x) * ln (exp 1)" by simp
374   also have "... <= (y - x) * ln x"
375     apply (rule mult_left_mono)
376     apply (subst ln_le_cancel_iff)
377     apply force
378     apply (rule a)
379     apply (rule prems)
380     apply (insert prems, simp)
381     done
382   also have "... = y * ln x - x * ln x"
383     by (rule left_diff_distrib)
384   finally have "x * ln y <= y * ln x"
385     by arith
386   then have "ln y <= (y * ln x) / x" using a by(simp add:field_simps)
387   also have "... = y * (ln x / x)"  by simp
388   finally show ?thesis using b by(simp add:field_simps)
389 qed
391 end