author | eberlm <eberlm@in.tum.de> |
Fri, 13 Jan 2017 17:45:51 +0100 | |
changeset 64888 | eb019ab30bdc |
child 64891 | d047004c1109 |
permissions | -rw-r--r-- |
64888
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
1 |
(* |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
2 |
File: Circle_Area.thy |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
3 |
Author: Manuel Eberl <eberlm@in.tum.de> |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
4 |
|
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
5 |
An proof that the area of a circle with radius R is R²\<pi>. |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
6 |
*) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
7 |
section {* The area of a circle *} |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
8 |
theory Circle_Area |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
9 |
imports Complex_Main Interval_Integral |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
10 |
begin |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
11 |
|
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
12 |
lemma plus_emeasure': |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
13 |
assumes "A \<in> sets M" "B \<in> sets M" "A \<inter> B \<in> null_sets M" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
14 |
shows "emeasure M A + emeasure M B = emeasure M (A \<union> B)" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
15 |
proof- |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
16 |
let ?C = "A \<inter> B" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
17 |
have "A \<union> B = A \<union> (B - ?C)" by blast |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
18 |
with assms have "emeasure M (A \<union> B) = emeasure M A + emeasure M (B - ?C)" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
19 |
by (subst plus_emeasure) auto |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
20 |
also from assms(3,2) have "emeasure M (B - ?C) = emeasure M B" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
21 |
by (rule emeasure_Diff_null_set) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
22 |
finally show ?thesis .. |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
23 |
qed |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
24 |
|
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
25 |
lemma real_sqrt_square: |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
26 |
"x \<ge> 0 \<Longrightarrow> sqrt (x^2) = (x::real)" by simp |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
27 |
|
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
28 |
lemma unit_circle_area_aux: |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
29 |
"LBINT x=-1..1. 2 * sqrt (1 - x^2) = pi" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
30 |
proof- |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
31 |
have "LBINT x=-1..1. 2 * sqrt (1 - x^2) = |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
32 |
LBINT x=ereal (sin (-pi/2))..ereal (sin (pi/2)). 2 * sqrt (1 - x^2)" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
33 |
by (simp_all add: one_ereal_def) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
34 |
also have "... = LBINT x=-pi/2..pi/2. cos x *\<^sub>R (2 * sqrt (1 - (sin x)\<^sup>2))" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
35 |
by (rule interval_integral_substitution_finite[symmetric]) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
36 |
(auto intro: DERIV_subset[OF DERIV_sin] intro!: continuous_intros) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
37 |
also have "... = LBINT x=-pi/2..pi/2. 2 * cos x * sqrt ((cos x)^2)" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
38 |
by (simp add: cos_squared_eq field_simps) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
39 |
also { |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
40 |
fix x assume "x \<in> {-pi/2<..<pi/2}" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
41 |
hence "cos x \<ge> 0" by (intro cos_ge_zero) simp_all |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
42 |
hence "sqrt ((cos x)^2) = cos x" by simp |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
43 |
} note A = this |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
44 |
have "LBINT x=-pi/2..pi/2. 2 * cos x * sqrt ((cos x)^2) = LBINT x=-pi/2..pi/2. 2 * (cos x)^2" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
45 |
by (intro interval_integral_cong, subst A) (simp_all add: min_def max_def power2_eq_square) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
46 |
also let ?F = "\<lambda>x. x + sin x * cos x" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
47 |
{ |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
48 |
fix x A |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
49 |
have "(?F has_real_derivative 1 - (sin x)^2 + (cos x)^2) (at x)" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
50 |
by (auto simp: power2_eq_square intro!: derivative_eq_intros) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
51 |
also have "1 - (sin x)^2 + (cos x)^2 = 2 * (cos x)^2" by (simp add: cos_squared_eq) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
52 |
finally have "(?F has_real_derivative 2 * (cos x)^2) (at x within A)" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
53 |
by (rule DERIV_subset) simp |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
54 |
} |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
55 |
hence "LBINT x=-pi/2..pi/2. 2 * (cos x)^2 = ?F (pi/2) - ?F (-pi/2)" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
56 |
by (intro interval_integral_FTC_finite) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
57 |
(auto simp: has_field_derivative_iff_has_vector_derivative intro!: continuous_intros) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
58 |
also have "... = pi" by simp |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
59 |
finally show ?thesis . |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
60 |
qed |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
61 |
|
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
62 |
lemma unit_circle_area: |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
63 |
"emeasure lborel {z::real\<times>real. norm z \<le> 1} = pi" (is "emeasure _ ?A = _") |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
64 |
proof- |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
65 |
let ?A1 = "{(x,y)\<in>?A. y \<ge> 0}" and ?A2 = "{(x,y)\<in>?A. y \<le> 0}" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
66 |
have [measurable]: "(\<lambda>x. snd (x :: real \<times> real)) \<in> measurable borel borel" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
67 |
by (simp add: borel_prod[symmetric]) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
68 |
|
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
69 |
have "?A1 = ?A \<inter> {x\<in>space lborel. snd x \<ge> 0}" by auto |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
70 |
also have "?A \<inter> {x\<in>space lborel. snd x \<ge> 0} \<in> sets borel" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
71 |
by (intro sets.Int pred_Collect_borel) simp_all |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
72 |
finally have A1_in_sets: "?A1 \<in> sets lborel" by (subst sets_lborel) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
73 |
|
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
74 |
have "?A2 = ?A \<inter> {x\<in>space lborel. snd x \<le> 0}" by auto |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
75 |
also have "... \<in> sets borel" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
76 |
by (intro sets.Int pred_Collect_borel) simp_all |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
77 |
finally have A2_in_sets: "?A2 \<in> sets lborel" by (subst sets_lborel) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
78 |
|
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
79 |
have A12: "?A = ?A1 \<union> ?A2" by auto |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
80 |
have sq_le_1_iff: "\<And>x. x\<^sup>2 \<le> 1 \<longleftrightarrow> abs (x::real) \<le> 1" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
81 |
by (simp add: abs_square_le_1) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
82 |
have "?A1 \<inter> ?A2 = {x. abs x \<le> 1} \<times> {0}" by (auto simp: norm_Pair field_simps sq_le_1_iff) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
83 |
also have "... \<in> null_sets lborel" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
84 |
by (subst lborel_prod[symmetric]) (auto simp: lborel.emeasure_pair_measure_Times) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
85 |
finally have "emeasure lborel ?A = emeasure lborel ?A1 + emeasure lborel ?A2" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
86 |
by (subst A12, rule plus_emeasure'[OF A1_in_sets A2_in_sets, symmetric]) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
87 |
|
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
88 |
also have "emeasure lborel ?A1 = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel \<partial>lborel" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
89 |
by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
90 |
(simp_all only: lborel_prod A1_in_sets) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
91 |
also have "emeasure lborel ?A2 = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A2 (x,y) \<partial>lborel \<partial>lborel" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
92 |
by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
93 |
(simp_all only: lborel_prod A2_in_sets) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
94 |
also have "distr lborel lborel uminus = (lborel :: real measure)" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
95 |
by (subst (3) lborel_real_affine[of "-1" 0]) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
96 |
(simp_all add: one_ereal_def[symmetric] density_1 cong: distr_cong) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
97 |
hence "(\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A2 (x,y) \<partial>lborel \<partial>lborel) = |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
98 |
\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A2 (x,y) \<partial>distr lborel lborel uminus \<partial>lborel" by simp |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
99 |
also have "... = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A2 (x,-y) \<partial>lborel \<partial>lborel" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
100 |
apply (intro nn_integral_cong nn_integral_distr, simp) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
101 |
apply (intro measurable_compose[OF _ borel_measurable_indicator[OF A2_in_sets]], simp) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
102 |
done |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
103 |
also have "... = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel \<partial>lborel" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
104 |
by (intro nn_integral_cong) (auto split: split_indicator simp: norm_Pair) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
105 |
also have "... + ... = (1+1) * ..." by (subst ring_distribs) simp_all |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
106 |
also have "... = \<integral>\<^sup>+x. 2 * \<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel \<partial>lborel" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
107 |
by (subst nn_integral_cmult) simp_all |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
108 |
also { |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
109 |
fix x y :: real assume "x \<notin> {-1..1}" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
110 |
hence "abs x > 1" by auto |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
111 |
also have "norm (x,y) \<ge> abs x" by (simp add: norm_Pair) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
112 |
finally have "(x,y) \<notin> ?A1" by auto |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
113 |
} |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
114 |
hence "... = \<integral>\<^sup>+x. 2 * (\<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel) * indicator {-1..1} x \<partial>lborel" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
115 |
by (intro nn_integral_cong) (auto split: split_indicator) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
116 |
also { |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
117 |
fix x :: real assume "x \<in> {-1..1}" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
118 |
hence x: "1 - x\<^sup>2 \<ge> 0" by (simp add: field_simps sq_le_1_iff abs_real_def) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
119 |
have "\<And>y. (y::real) \<ge> 0 \<Longrightarrow> norm (x,y) \<le> 1 \<longleftrightarrow> y \<le> sqrt (1-x\<^sup>2)" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
120 |
by (subst (5) real_sqrt_square[symmetric], simp, subst real_sqrt_le_iff) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
121 |
(simp_all add: norm_Pair field_simps) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
122 |
hence "(\<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel) = (\<integral>\<^sup>+y. indicator {0..sqrt (1-x\<^sup>2)} y \<partial>lborel)" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
123 |
by (intro nn_integral_cong) (auto split: split_indicator) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
124 |
also from x have "... = sqrt (1-x\<^sup>2)" using x by simp |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
125 |
finally have "(\<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel) = sqrt (1-x\<^sup>2)" . |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
126 |
} |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
127 |
hence "(\<integral>\<^sup>+x. 2 * (\<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel) * indicator {-1..1} x \<partial>lborel) = |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
128 |
\<integral>\<^sup>+x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1} x \<partial>lborel" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
129 |
by (intro nn_integral_cong) (simp split: split_indicator add: ennreal_mult') |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
130 |
also have A: "\<And>x. -1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> \<not>x^2 > (1::real)" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
131 |
by (subst not_less, subst sq_le_1_iff) (simp add: abs_real_def) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
132 |
have "integrable lborel (\<lambda>x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1::real} x)" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
133 |
by (intro borel_integrable_atLeastAtMost continuous_intros) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
134 |
hence "(\<integral>\<^sup>+x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1} x \<partial>lborel) = |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
135 |
ennreal (\<integral>x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1} x \<partial>lborel)" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
136 |
by (intro nn_integral_eq_integral AE_I2) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
137 |
(auto split: split_indicator simp: field_simps sq_le_1_iff) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
138 |
also have "(\<integral>x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1} x \<partial>lborel) = |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
139 |
LBINT x:{-1..1}. 2 * sqrt (1-x\<^sup>2)" by (simp add: field_simps) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
140 |
also have "... = LBINT x=-1..1. 2 * sqrt (1-x\<^sup>2)" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
141 |
by (subst interval_integral_Icc[symmetric]) (simp_all add: one_ereal_def) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
142 |
also have "... = pi" by (rule unit_circle_area_aux) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
143 |
finally show ?thesis . |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
144 |
qed |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
145 |
|
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
146 |
lemma circle_area: |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
147 |
assumes "R \<ge> 0" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
148 |
shows "emeasure lborel {z::real\<times>real. norm z \<le> R} = R^2 * pi" (is "emeasure _ ?A = _") |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
149 |
proof (cases "R = 0") |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
150 |
assume "R \<noteq> 0" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
151 |
with assms have R: "R > 0" by simp |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
152 |
let ?A' = "{z::real\<times>real. norm z \<le> 1}" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
153 |
have "emeasure lborel ?A = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (x,y) \<partial>lborel \<partial>lborel" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
154 |
by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure, subst lborel_prod) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
155 |
simp_all |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
156 |
also have "... = \<integral>\<^sup>+x. R * \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
157 |
proof (rule nn_integral_cong) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
158 |
fix x from R show "(\<integral>\<^sup>+y. indicator ?A (x,y) \<partial>lborel) = R * \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
159 |
by (subst nn_integral_real_affine[OF _ `R \<noteq> 0`, of _ 0]) simp_all |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
160 |
qed |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
161 |
also have "... = R * \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
162 |
using R by (intro nn_integral_cmult) simp_all |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
163 |
also from R have "(\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel) = |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
164 |
R * \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (R*x,R*y) \<partial>lborel \<partial>lborel" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
165 |
by (subst nn_integral_real_affine[OF _ `R \<noteq> 0`, of _ 0]) simp_all |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
166 |
also { |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
167 |
fix x y |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
168 |
have A: "(R*x, R*y) = R *\<^sub>R (x,y)" by simp |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
169 |
from R have "norm (R*x, R*y) = R * norm (x,y)" by (subst A, subst norm_scaleR) simp_all |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
170 |
with R have "(R*x, R*y) \<in> ?A \<longleftrightarrow> (x, y) \<in> ?A'" by (auto simp: field_simps) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
171 |
} |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
172 |
hence "(\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (R*x,R*y) \<partial>lborel \<partial>lborel) = |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
173 |
\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A' (x,y) \<partial>lborel \<partial>lborel" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
174 |
by (intro nn_integral_cong) (simp split: split_indicator) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
175 |
also have "... = emeasure lborel ?A'" |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
176 |
by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure, subst lborel_prod) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
177 |
simp_all |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
178 |
also have "... = pi" by (rule unit_circle_area) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
179 |
finally show ?thesis using assms by (simp add: power2_eq_square ennreal_mult mult_ac) |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
180 |
qed simp |
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
181 |
|
eb019ab30bdc
Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset
|
182 |
end |