src/HOL/Analysis/ex/Circle_Area.thy
author wenzelm
Sat, 14 Jan 2017 21:29:21 +0100
changeset 64892 662de910a96b
parent 64891 d047004c1109
child 64911 f0e07600de47
permissions -rw-r--r--
do avoid suspicious Unicode;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64891
d047004c1109 more standard header;
wenzelm
parents: 64888
diff changeset
     1
(*  Title:      HOL/Analysis/ex/Circle_Area.thy
d047004c1109 more standard header;
wenzelm
parents: 64888
diff changeset
     2
    Author:     Manuel Eberl, TU Muenchen
64888
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     3
64892
662de910a96b do avoid suspicious Unicode;
wenzelm
parents: 64891
diff changeset
     4
A proof that the area of a circle with radius R is R\<^sup>2\<pi>.
64888
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     5
*)
64891
d047004c1109 more standard header;
wenzelm
parents: 64888
diff changeset
     6
64888
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     7
section {* The area of a circle *}
64891
d047004c1109 more standard header;
wenzelm
parents: 64888
diff changeset
     8
64888
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     9
theory Circle_Area
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    10
imports Complex_Main Interval_Integral
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    11
begin
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    12
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    13
lemma plus_emeasure':
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    16
proof-
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    17
  let ?C = "A \<inter> B"
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    20
    by (subst plus_emeasure) auto
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    22
    by (rule emeasure_Diff_null_set)
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    23
  finally show ?thesis ..
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    24
qed
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    25
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    26
lemma real_sqrt_square:
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    28
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    29
lemma unit_circle_area_aux:
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    31
proof-
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    34
    by (simp_all add: one_ereal_def)
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    36
    by (rule interval_integral_substitution_finite[symmetric])
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    37
       (auto intro: DERIV_subset[OF DERIV_sin] intro!: continuous_intros)
64891
d047004c1109 more standard header;
wenzelm
parents: 64888
diff changeset
    38
  also have "... = LBINT x=-pi/2..pi/2. 2 * cos x * sqrt ((cos x)^2)"
64888
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    39
    by (simp add: cos_squared_eq field_simps)
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    40
  also {
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    41
    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
    42
    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
    43
    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
    44
  } note A = this
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    48
   {
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    49
    fix x A
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis 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
d047004c1109 more standard header;
wenzelm
parents: 64888
diff changeset
    53
    finally have "(?F has_real_derivative 2 * (cos x)^2) (at x within A)"
64888
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    54
      by (rule DERIV_subset) simp
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    55
  }
eb019ab30bdc Added Circle_Area to HOL-Analysis 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
d047004c1109 more standard header;
wenzelm
parents: 64888
diff changeset
    57
    by (intro interval_integral_FTC_finite)
64888
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    59
  also have "... = pi" by simp
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    60
  finally show ?thesis .
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    61
qed
64891
d047004c1109 more standard header;
wenzelm
parents: 64888
diff changeset
    62
64888
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    63
lemma unit_circle_area:
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    65
proof-
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    68
    by (simp add: borel_prod[symmetric])
64891
d047004c1109 more standard header;
wenzelm
parents: 64888
diff changeset
    69
64888
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    72
    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
    73
  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
    74
eb019ab30bdc Added Circle_Area to HOL-Analysis 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
d047004c1109 more standard header;
wenzelm
parents: 64888
diff changeset
    76
  also have "... \<in> sets borel"
64888
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    77
    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
    78
  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
    79
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    80
  have A12: "?A = ?A1 \<union> ?A2" by auto
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    82
    by (simp add: abs_square_le_1)
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    84
  also have "... \<in> null_sets lborel"
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    88
eb019ab30bdc Added Circle_Area to HOL-Analysis 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
d047004c1109 more standard header;
wenzelm
parents: 64888
diff changeset
    90
    by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure)
64888
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    91
       (simp_all only: lborel_prod A1_in_sets)
eb019ab30bdc Added Circle_Area to HOL-Analysis 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
d047004c1109 more standard header;
wenzelm
parents: 64888
diff changeset
    93
    by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure)
64888
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    94
       (simp_all only: lborel_prod A2_in_sets)
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    95
  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
    96
    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
    97
       (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
    98
  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
    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 HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   101
    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
   102
    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
   103
    done
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   108
    by (subst nn_integral_cmult) simp_all
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   109
  also {
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   110
    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
   111
    hence "abs x > 1" by auto
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   113
    finally have "(x,y) \<notin> ?A1" by auto
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   114
  }
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   116
    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
   117
  also {
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   118
    fix x :: real assume "x \<in> {-1..1}"
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis 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 (1-x\<^sup>2)"
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   122
         (simp_all add: norm_Pair field_simps)
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 (1-x\<^sup>2)} y \<partial>lborel)"
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   124
      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
   125
    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
   126
    finally have "(\<integral>\<^sup>+y. indicator ?A1 (x,y) \<partial>lborel) = sqrt (1-x\<^sup>2)" .
64891
d047004c1109 more standard header;
wenzelm
parents: 64888
diff changeset
   127
  }
64888
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   129
            \<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
   130
    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
   131
  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
   132
    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
   133
  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
   134
    by (intro borel_integrable_atLeastAtMost continuous_intros)
64891
d047004c1109 more standard header;
wenzelm
parents: 64888
diff changeset
   135
  hence "(\<integral>\<^sup>+x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1} x \<partial>lborel) =
64888
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   136
             ennreal (\<integral>x. 2 * sqrt (1-x\<^sup>2) * indicator {-1..1} x \<partial>lborel)"
64891
d047004c1109 more standard header;
wenzelm
parents: 64888
diff changeset
   137
    by (intro nn_integral_eq_integral AE_I2)
64888
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   139
  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
   140
               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
   141
  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
   142
    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
   143
  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
   144
  finally show ?thesis .
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   145
qed
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   146
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   147
lemma circle_area:
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   148
  assumes "R \<ge> 0"
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   150
proof (cases "R = 0")
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   151
  assume "R \<noteq> 0"
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   152
  with assms have R: "R > 0" by simp
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   156
       simp_all
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   158
  proof (rule nn_integral_cong)
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   161
  qed
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   163
    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
   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 HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   167
  also {
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   168
    fix x y
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   172
  }
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   175
    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
   176
  also have "... = emeasure lborel ?A'"
64891
d047004c1109 more standard header;
wenzelm
parents: 64888
diff changeset
   177
    by (subst lborel_prod[symmetric], subst lborel.emeasure_pair_measure, subst lborel_prod)
d047004c1109 more standard header;
wenzelm
parents: 64888
diff changeset
   178
       simp_all
64888
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   179
  also have "... = pi" by (rule unit_circle_area)
eb019ab30bdc Added Circle_Area to HOL-Analysis 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 HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   181
qed simp
eb019ab30bdc Added Circle_Area to HOL-Analysis examples
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   182
64891
d047004c1109 more standard header;
wenzelm
parents: 64888
diff changeset
   183
end