author  wenzelm 
Sat, 14 Jan 2017 21:29:21 +0100  
changeset 64892  662de910a96b 
parent 64891  d047004c1109 
child 64911  f0e07600de47 
permissions  rwrr 
64891  1 
(* Title: HOL/Analysis/ex/Circle_Area.thy 
2 
Author: Manuel Eberl, TU Muenchen 

64888
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

3 

64892  4 
A proof that the area of a circle with radius R is R\<^sup>2\<pi>. 
64888
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

5 
*) 
64891  6 

64888
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

7 
section {* The area of a circle *} 
64891  8 

64888
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

9 
theory Circle_Area 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

10 
imports Complex_Main Interval_Integral 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

11 
begin 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

12 

eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

13 
lemma plus_emeasure': 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

14 
assumes "A \<in> sets M" "B \<in> sets M" "A \<inter> B \<in> null_sets M" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

15 
shows "emeasure M A + emeasure M B = emeasure M (A \<union> B)" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

16 
proof 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

17 
let ?C = "A \<inter> B" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

18 
have "A \<union> B = A \<union> (B  ?C)" by blast 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

19 
with assms have "emeasure M (A \<union> B) = emeasure M A + emeasure M (B  ?C)" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

20 
by (subst plus_emeasure) auto 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

21 
also from assms(3,2) have "emeasure M (B  ?C) = emeasure M B" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

22 
by (rule emeasure_Diff_null_set) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

23 
finally show ?thesis .. 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

24 
qed 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

25 

eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

26 
lemma real_sqrt_square: 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

27 
"x \<ge> 0 \<Longrightarrow> sqrt (x^2) = (x::real)" by simp 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

28 

eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

29 
lemma unit_circle_area_aux: 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

30 
"LBINT x=1..1. 2 * sqrt (1  x^2) = pi" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

31 
proof 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

32 
have "LBINT x=1..1. 2 * sqrt (1  x^2) = 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

33 
LBINT x=ereal (sin (pi/2))..ereal (sin (pi/2)). 2 * sqrt (1  x^2)" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

34 
by (simp_all add: one_ereal_def) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

35 
also have "... = LBINT x=pi/2..pi/2. cos x *\<^sub>R (2 * sqrt (1  (sin x)\<^sup>2))" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

36 
by (rule interval_integral_substitution_finite[symmetric]) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

37 
(auto intro: DERIV_subset[OF DERIV_sin] intro!: continuous_intros) 
64891  38 
also have "... = LBINT x=pi/2..pi/2. 2 * cos x * sqrt ((cos x)^2)" 
64888
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

39 
by (simp add: cos_squared_eq field_simps) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

40 
also { 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

41 
fix x assume "x \<in> {pi/2<..<pi/2}" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

42 
hence "cos x \<ge> 0" by (intro cos_ge_zero) simp_all 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

43 
hence "sqrt ((cos x)^2) = cos x" by simp 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

44 
} note A = this 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

45 
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 HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

46 
by (intro interval_integral_cong, subst A) (simp_all add: min_def max_def power2_eq_square) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

47 
also let ?F = "\<lambda>x. x + sin x * cos x" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

48 
{ 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

49 
fix x A 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

50 
have "(?F has_real_derivative 1  (sin x)^2 + (cos x)^2) (at x)" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

51 
by (auto simp: power2_eq_square intro!: derivative_eq_intros) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

52 
also have "1  (sin x)^2 + (cos x)^2 = 2 * (cos x)^2" by (simp add: cos_squared_eq) 
64891  53 
finally have "(?F has_real_derivative 2 * (cos x)^2) (at x within A)" 
64888
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

54 
by (rule DERIV_subset) simp 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

55 
} 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

56 
hence "LBINT x=pi/2..pi/2. 2 * (cos x)^2 = ?F (pi/2)  ?F (pi/2)" 
64891  57 
by (intro interval_integral_FTC_finite) 
64888
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

58 
(auto simp: has_field_derivative_iff_has_vector_derivative intro!: continuous_intros) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

59 
also have "... = pi" by simp 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

60 
finally show ?thesis . 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

61 
qed 
64891  62 

64888
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

63 
lemma unit_circle_area: 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

64 
"emeasure lborel {z::real\<times>real. norm z \<le> 1} = pi" (is "emeasure _ ?A = _") 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

65 
proof 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

66 
let ?A1 = "{(x,y)\<in>?A. y \<ge> 0}" and ?A2 = "{(x,y)\<in>?A. y \<le> 0}" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

67 
have [measurable]: "(\<lambda>x. snd (x :: real \<times> real)) \<in> measurable borel borel" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

68 
by (simp add: borel_prod[symmetric]) 
64891  69 

64888
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

70 
have "?A1 = ?A \<inter> {x\<in>space lborel. snd x \<ge> 0}" by auto 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

71 
also have "?A \<inter> {x\<in>space lborel. snd x \<ge> 0} \<in> sets borel" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

72 
by (intro sets.Int pred_Collect_borel) simp_all 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

73 
finally have A1_in_sets: "?A1 \<in> sets lborel" by (subst sets_lborel) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

74 

eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

75 
have "?A2 = ?A \<inter> {x\<in>space lborel. snd x \<le> 0}" by auto 
64891  76 
also have "... \<in> sets borel" 
64888
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

77 
by (intro sets.Int pred_Collect_borel) simp_all 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

78 
finally have A2_in_sets: "?A2 \<in> sets lborel" by (subst sets_lborel) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

79 

eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

80 
have A12: "?A = ?A1 \<union> ?A2" by auto 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

81 
have sq_le_1_iff: "\<And>x. x\<^sup>2 \<le> 1 \<longleftrightarrow> abs (x::real) \<le> 1" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

82 
by (simp add: abs_square_le_1) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

83 
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 HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

84 
also have "... \<in> null_sets lborel" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

85 
by (subst lborel_prod[symmetric]) (auto simp: lborel.emeasure_pair_measure_Times) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

86 
finally have "emeasure lborel ?A = emeasure lborel ?A1 + emeasure lborel ?A2" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

87 
by (subst A12, rule plus_emeasure'[OF A1_in_sets A2_in_sets, symmetric]) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

88 

eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

89 
also have "emeasure lborel ?A1 = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel \<partial>lborel" 
64891  90 
by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure) 
64888
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

91 
(simp_all only: lborel_prod A1_in_sets) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

92 
also have "emeasure lborel ?A2 = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A2 (x,y) \<partial>lborel \<partial>lborel" 
64891  93 
by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure) 
64888
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

94 
(simp_all only: lborel_prod A2_in_sets) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

95 
also have "distr lborel lborel uminus = (lborel :: real measure)" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

96 
by (subst (3) lborel_real_affine[of "1" 0]) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

97 
(simp_all add: one_ereal_def[symmetric] density_1 cong: distr_cong) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

98 
hence "(\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A2 (x,y) \<partial>lborel \<partial>lborel) = 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

99 
\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A2 (x,y) \<partial>distr lborel lborel uminus \<partial>lborel" by simp 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

100 
also have "... = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A2 (x,y) \<partial>lborel \<partial>lborel" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

101 
apply (intro nn_integral_cong nn_integral_distr, simp) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

102 
apply (intro measurable_compose[OF _ borel_measurable_indicator[OF A2_in_sets]], simp) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

103 
done 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

104 
also have "... = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel \<partial>lborel" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

105 
by (intro nn_integral_cong) (auto split: split_indicator simp: norm_Pair) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

106 
also have "... + ... = (1+1) * ..." by (subst ring_distribs) simp_all 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

107 
also have "... = \<integral>\<^sup>+x. 2 * \<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel \<partial>lborel" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

108 
by (subst nn_integral_cmult) simp_all 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

109 
also { 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

110 
fix x y :: real assume "x \<notin> {1..1}" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

111 
hence "abs x > 1" by auto 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

112 
also have "norm (x,y) \<ge> abs x" by (simp add: norm_Pair) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

113 
finally have "(x,y) \<notin> ?A1" by auto 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

114 
} 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

115 
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 HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

116 
by (intro nn_integral_cong) (auto split: split_indicator) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

117 
also { 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

118 
fix x :: real assume "x \<in> {1..1}" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

119 
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 HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

120 
have "\<And>y. (y::real) \<ge> 0 \<Longrightarrow> norm (x,y) \<le> 1 \<longleftrightarrow> y \<le> sqrt (1x\<^sup>2)" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

121 
by (subst (5) real_sqrt_square[symmetric], simp, subst real_sqrt_le_iff) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

122 
(simp_all add: norm_Pair field_simps) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

123 
hence "(\<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel) = (\<integral>\<^sup>+y. indicator {0..sqrt (1x\<^sup>2)} y \<partial>lborel)" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

124 
by (intro nn_integral_cong) (auto split: split_indicator) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

125 
also from x have "... = sqrt (1x\<^sup>2)" using x by simp 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

126 
finally have "(\<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel) = sqrt (1x\<^sup>2)" . 
64891  127 
} 
64888
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

128 
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 HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

129 
\<integral>\<^sup>+x. 2 * sqrt (1x\<^sup>2) * indicator {1..1} x \<partial>lborel" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

130 
by (intro nn_integral_cong) (simp split: split_indicator add: ennreal_mult') 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

131 
also have A: "\<And>x. 1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> \<not>x^2 > (1::real)" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

132 
by (subst not_less, subst sq_le_1_iff) (simp add: abs_real_def) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

133 
have "integrable lborel (\<lambda>x. 2 * sqrt (1x\<^sup>2) * indicator {1..1::real} x)" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

134 
by (intro borel_integrable_atLeastAtMost continuous_intros) 
64891  135 
hence "(\<integral>\<^sup>+x. 2 * sqrt (1x\<^sup>2) * indicator {1..1} x \<partial>lborel) = 
64888
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

136 
ennreal (\<integral>x. 2 * sqrt (1x\<^sup>2) * indicator {1..1} x \<partial>lborel)" 
64891  137 
by (intro nn_integral_eq_integral AE_I2) 
64888
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

138 
(auto split: split_indicator simp: field_simps sq_le_1_iff) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

139 
also have "(\<integral>x. 2 * sqrt (1x\<^sup>2) * indicator {1..1} x \<partial>lborel) = 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

140 
LBINT x:{1..1}. 2 * sqrt (1x\<^sup>2)" by (simp add: field_simps) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

141 
also have "... = LBINT x=1..1. 2 * sqrt (1x\<^sup>2)" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

142 
by (subst interval_integral_Icc[symmetric]) (simp_all add: one_ereal_def) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

143 
also have "... = pi" by (rule unit_circle_area_aux) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

144 
finally show ?thesis . 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

145 
qed 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

146 

eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

147 
lemma circle_area: 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

148 
assumes "R \<ge> 0" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

149 
shows "emeasure lborel {z::real\<times>real. norm z \<le> R} = R^2 * pi" (is "emeasure _ ?A = _") 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

150 
proof (cases "R = 0") 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

151 
assume "R \<noteq> 0" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

152 
with assms have R: "R > 0" by simp 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

153 
let ?A' = "{z::real\<times>real. norm z \<le> 1}" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

154 
have "emeasure lborel ?A = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (x,y) \<partial>lborel \<partial>lborel" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

155 
by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure, subst lborel_prod) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

156 
simp_all 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

157 
also have "... = \<integral>\<^sup>+x. R * \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

158 
proof (rule nn_integral_cong) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

159 
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 HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

160 
by (subst nn_integral_real_affine[OF _ `R \<noteq> 0`, of _ 0]) simp_all 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

161 
qed 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

162 
also have "... = R * \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

163 
using R by (intro nn_integral_cmult) simp_all 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

164 
also from R have "(\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel) = 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

165 
R * \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (R*x,R*y) \<partial>lborel \<partial>lborel" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

166 
by (subst nn_integral_real_affine[OF _ `R \<noteq> 0`, of _ 0]) simp_all 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

167 
also { 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

168 
fix x y 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

169 
have A: "(R*x, R*y) = R *\<^sub>R (x,y)" by simp 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

170 
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 HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

171 
with R have "(R*x, R*y) \<in> ?A \<longleftrightarrow> (x, y) \<in> ?A'" by (auto simp: field_simps) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

172 
} 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

173 
hence "(\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (R*x,R*y) \<partial>lborel \<partial>lborel) = 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

174 
\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A' (x,y) \<partial>lborel \<partial>lborel" 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

175 
by (intro nn_integral_cong) (simp split: split_indicator) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

176 
also have "... = emeasure lborel ?A'" 
64891  177 
by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure, subst lborel_prod) 
178 
simp_all 

64888
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

179 
also have "... = pi" by (rule unit_circle_area) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

180 
finally show ?thesis using assms by (simp add: power2_eq_square ennreal_mult mult_ac) 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

181 
qed simp 
eb019ab30bdc
Added Circle_Area to HOLAnalysis examples
eberlm <eberlm@in.tum.de>
parents:
diff
changeset

182 

64891  183 
end 