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