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