src/HOL/Analysis/Simplex_Content.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (3 weeks ago) changeset 69981 3dced198b9ec parent 69737 ec3cc98c38db permissions -rw-r--r--
more strict AFP properties;
```     1 (*
```
```     2    File:      Analysis/Simplex_Content.thy
```
```     3    Author:    Manuel Eberl <eberlm@in.tum.de>
```
```     4
```
```     5    The content of an n-dimensional simplex, including the formula for the content of a
```
```     6    triangle and Heron's formula.
```
```     7 *)
```
```     8 section \<open>Volume of a Simplex\<close>
```
```     9
```
```    10 theory Simplex_Content
```
```    11 imports Change_Of_Vars
```
```    12 begin
```
```    13
```
```    14 lemma fact_neq_top_ennreal [simp]: "fact n \<noteq> (top :: ennreal)"
```
```    15   by (induction n) (auto simp: ennreal_mult_eq_top_iff)
```
```    16
```
```    17 lemma ennreal_fact: "ennreal (fact n) = fact n"
```
```    18   by (induction n) (auto simp: ennreal_mult algebra_simps ennreal_of_nat_eq_real_of_nat)
```
```    19
```
```    20 context
```
```    21   fixes S :: "'a set \<Rightarrow> real \<Rightarrow> ('a \<Rightarrow> real) set"
```
```    22   defines "S \<equiv> (\<lambda>A t. {x. (\<forall>i\<in>A. 0 \<le> x i) \<and> sum x A \<le> t})"
```
```    23 begin
```
```    24
```
```    25 lemma emeasure_std_simplex_aux_step:
```
```    26   assumes "b \<notin> A" "finite A"
```
```    27   shows   "x(b := y) \<in> S (insert b A) t \<longleftrightarrow> y \<in> {0..t} \<and> x \<in> S A (t - y)"
```
```    28   using assms sum_nonneg[of A x] unfolding S_def
```
```    29   by (force simp: sum_delta_notmem algebra_simps)
```
```    30
```
```    31 lemma emeasure_std_simplex_aux:
```
```    32   fixes t :: real
```
```    33   assumes "finite (A :: 'a set)" "t \<ge> 0"
```
```    34   shows   "emeasure (Pi\<^sub>M A (\<lambda>_. lborel))
```
```    35              (S A t \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) = t ^ card A / fact (card A)"
```
```    36   using assms(1,2)
```
```    37 proof (induction arbitrary: t rule: finite_induct)
```
```    38   case (empty t)
```
```    39   thus ?case by (simp add: PiM_empty S_def)
```
```    40 next
```
```    41   case (insert b A t)
```
```    42   define n where "n = Suc (card A)"
```
```    43   have n_pos: "n > 0" by (simp add: n_def)
```
```    44   let ?M = "\<lambda>A. (Pi\<^sub>M A (\<lambda>_. lborel))"
```
```    45   {
```
```    46     fix A :: "'a set" and t :: real assume "finite A"
```
```    47     have "S A t \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel)) =
```
```    48             Pi\<^sub>E A (\<lambda>_. {0..}) \<inter> (\<lambda>x. sum x A) -` {..t} \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))"
```
```    49       by (auto simp: S_def space_PiM)
```
```    50     also have "\<dots> \<in> sets (Pi\<^sub>M A (\<lambda>_. lborel))"
```
```    51       using \<open>finite A\<close> by measurable
```
```    52     finally have "S A t \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel)) \<in> sets (Pi\<^sub>M A (\<lambda>_. lborel))" .
```
```    53   } note meas [measurable] = this
```
```    54
```
```    55   interpret product_sigma_finite "\<lambda>_. lborel"
```
```    56     by standard
```
```    57   have "emeasure (?M (insert b A)) (S (insert b A) t \<inter> space (?M (insert b A))) =
```
```    58         nn_integral (?M (insert b A))
```
```    59           (\<lambda>x. indicator (S (insert b A) t \<inter> space (?M (insert b A))) x)"
```
```    60     using insert.hyps by (subst nn_integral_indicator) auto
```
```    61   also have "\<dots> = (\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. indicator (S (insert b A) t \<inter> space (?M (insert b A)))
```
```    62                     (x(b := y)) \<partial>?M A \<partial>lborel)"
```
```    63     using insert.prems insert.hyps by (intro product_nn_integral_insert_rev) auto
```
```    64   also have "\<dots> = (\<integral>\<^sup>+ y. \<integral>\<^sup>+ x. indicator {0..t} y * indicator (S A (t - y) \<inter> space (?M A)) x
```
```    65                     \<partial>?M A \<partial>lborel)"
```
```    66     using insert.hyps insert.prems emeasure_std_simplex_aux_step[of b A]
```
```    67     by (intro nn_integral_cong)
```
```    68        (auto simp: fun_eq_iff indicator_def space_PiM PiE_def extensional_def)
```
```    69   also have "\<dots> = (\<integral>\<^sup>+ y. indicator {0..t} y * (\<integral>\<^sup>+ x. indicator (S A (t - y) \<inter> space (?M A)) x
```
```    70                     \<partial>?M A) \<partial>lborel)" using \<open>finite A\<close>
```
```    71     by (subst nn_integral_cmult) auto
```
```    72   also have "\<dots> = (\<integral>\<^sup>+ y. indicator {0..t} y * emeasure (?M A) (S A (t - y) \<inter> space (?M A)) \<partial>lborel)"
```
```    73     using \<open>finite A\<close> by (subst nn_integral_indicator) auto
```
```    74   also have "\<dots> = (\<integral>\<^sup>+ y. indicator {0..t} y * (t - y) ^ card A / ennreal (fact (card A)) \<partial>lborel)"
```
```    75     using insert.IH by (intro nn_integral_cong) (auto simp: indicator_def divide_ennreal)
```
```    76   also have "\<dots> = (\<integral>\<^sup>+ y. indicator {0..t} y * (t - y) ^ card A \<partial>lborel) / ennreal (fact (card A))"
```
```    77     using \<open>finite A\<close> by (subst nn_integral_divide) auto
```
```    78   also have "(\<integral>\<^sup>+ y. indicator {0..t} y * (t - y) ^ card A \<partial>lborel) =
```
```    79                (\<integral>\<^sup>+y\<in>{0..t}. ennreal ((t - y) ^ (n - 1)) \<partial>lborel)"
```
```    80     by (intro nn_integral_cong) (auto simp: indicator_def n_def)
```
```    81   also have "((\<lambda>x. - ((t - x) ^ n / n)) has_real_derivative (t - x) ^ (n - 1)) (at x)"
```
```    82     if "x \<in> {0..t}" for x by (rule derivative_eq_intros refl | simp add: n_pos)+
```
```    83   hence "(\<integral>\<^sup>+y\<in>{0..t}. ennreal ((t - y) ^ (n - 1)) \<partial>lborel) =
```
```    84            ennreal (-((t - t) ^ n / n) - (-((t - 0) ^ n / n)))"
```
```    85     using insert.prems insert.hyps by (intro nn_integral_FTC_Icc) auto
```
```    86   also have "\<dots> = ennreal (t ^ n / n)" using n_pos by (simp add: zero_power)
```
```    87   also have "\<dots> / ennreal (fact (card A)) = ennreal (t ^ n / n / fact (card A))"
```
```    88     using n_pos \<open>t \<ge> 0\<close> by (subst divide_ennreal) auto
```
```    89   also have "t ^ n / n / fact (card A) = t ^ n / fact n"
```
```    90     by (simp add: n_def)
```
```    91   also have "n = card (insert b A)"
```
```    92     using insert.hyps by (subst card_insert) (auto simp: n_def)
```
```    93   finally show ?case .
```
```    94 qed
```
```    95
```
```    96 end
```
```    97
```
```    98 lemma emeasure_std_simplex:
```
```    99   "emeasure lborel (convex hull (insert 0 Basis :: 'a :: euclidean_space set)) =
```
```   100      ennreal (1 / fact DIM('a))"
```
```   101 proof -
```
```   102   have "emeasure lborel {x::'a. (\<forall>i\<in>Basis. 0 \<le> x \<bullet> i) \<and> sum ((\<bullet>) x) Basis \<le> 1} =
```
```   103                emeasure (distr (Pi\<^sub>M Basis (\<lambda>b. lborel)) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b))
```
```   104                  {x::'a. (\<forall>i\<in>Basis. 0 \<le> x \<bullet> i) \<and> sum ((\<bullet>) x) Basis \<le> 1}"
```
```   105     by (subst lborel_eq) simp
```
```   106   also have "\<dots> = emeasure (Pi\<^sub>M Basis (\<lambda>b. lborel))
```
```   107                     ({y::'a \<Rightarrow> real. (\<forall>i\<in>Basis. 0 \<le> y i) \<and> sum y Basis \<le> 1} \<inter>
```
```   108                       space (Pi\<^sub>M Basis (\<lambda>b. lborel)))"
```
```   109     by (subst emeasure_distr) auto
```
```   110   also have "\<dots> = ennreal (1 / fact DIM('a))"
```
```   111     by (subst emeasure_std_simplex_aux) auto
```
```   112   finally show ?thesis by (simp only: std_simplex)
```
```   113 qed
```
```   114
```
```   115 theorem content_std_simplex:
```
```   116   "measure lborel (convex hull (insert 0 Basis :: 'a :: euclidean_space set)) =
```
```   117      1 / fact DIM('a)"
```
```   118   by (simp add: measure_def emeasure_std_simplex)
```
```   119
```
```   120 (* TODO: move to Change_of_Vars *)
```
```   121 proposition measure_lebesgue_linear_transformation:
```
```   122   fixes A :: "(real ^ 'n :: {finite, wellorder}) set"
```
```   123   fixes f :: "_ \<Rightarrow> real ^ 'n :: {finite, wellorder}"
```
```   124   assumes "bounded A" "A \<in> sets lebesgue" "linear f"
```
```   125   shows   "measure lebesgue (f ` A) = \<bar>det (matrix f)\<bar> * measure lebesgue A"
```
```   126 proof -
```
```   127   from assms have [intro]: "A \<in> lmeasurable"
```
```   128     by (intro bounded_set_imp_lmeasurable) auto
```
```   129   hence [intro]: "f ` A \<in> lmeasurable"
```
```   130     by (intro lmeasure_integral measurable_linear_image assms)
```
```   131   have "measure lebesgue (f ` A) = integral (f ` A) (\<lambda>_. 1)"
```
```   132     by (intro lmeasure_integral measurable_linear_image assms) auto
```
```   133   also have "\<dots> = integral (f ` A) (\<lambda>_. 1 :: real ^ 1) \$ 0"
```
```   134     by (subst integral_component_eq_cart [symmetric]) (auto intro: integrable_on_const)
```
```   135   also have "\<dots> = \<bar>det (matrix f)\<bar> * integral A (\<lambda>x. 1 :: real ^ 1) \$ 0"
```
```   136     using assms
```
```   137     by (subst integral_change_of_variables_linear)
```
```   138        (auto simp: o_def absolutely_integrable_on_def intro: integrable_on_const)
```
```   139   also have "integral A (\<lambda>x. 1 :: real ^ 1) \$ 0 = integral A (\<lambda>x. 1)"
```
```   140     by (subst integral_component_eq_cart [symmetric]) (auto intro: integrable_on_const)
```
```   141   also have "\<dots> = measure lebesgue A"
```
```   142     by (intro lmeasure_integral [symmetric]) auto
```
```   143   finally show ?thesis .
```
```   144 qed
```
```   145
```
```   146 theorem content_simplex:
```
```   147   fixes X :: "(real ^ 'n :: {finite, wellorder}) set" and f :: "'n :: _ \<Rightarrow> real ^ ('n :: _)"
```
```   148   assumes "finite X" "card X = Suc CARD('n)" and x0: "x0 \<in> X" and bij: "bij_betw f UNIV (X - {x0})"
```
```   149   defines "M \<equiv> (\<chi> i. \<chi> j. f j \$ i - x0 \$ i)"
```
```   150   shows "content (convex hull X) = \<bar>det M\<bar> / fact (CARD('n))"
```
```   151 proof -
```
```   152   define g where "g = (\<lambda>x. M *v x)"
```
```   153   have [simp]: "M *v axis i 1 = f i - x0" for i :: 'n
```
```   154     by (simp add: M_def matrix_vector_mult_basis column_def vec_eq_iff)
```
```   155   define std where "std = (convex hull insert 0 Basis :: (real ^ 'n :: _) set)"
```
```   156   have compact: "compact std" unfolding std_def
```
```   157     by (intro finite_imp_compact_convex_hull) auto
```
```   158
```
```   159   have "measure lebesgue (convex hull X) = measure lebesgue (((+) (-x0)) ` (convex hull X))"
```
```   160     by (rule measure_translation [symmetric])
```
```   161   also have "((+) (-x0)) ` (convex hull X) = convex hull (((+) (-x0)) ` X)"
```
```   162     by (rule convex_hull_translation [symmetric])
```
```   163   also have "((+) (-x0)) ` X = insert 0 ((\<lambda>x. x - x0) ` (X - {x0}))"
```
```   164     using x0 by (auto simp: image_iff)
```
```   165   finally have eq: "measure lebesgue (convex hull X) = measure lebesgue (convex hull \<dots>)" .
```
```   166
```
```   167   from compact have "measure lebesgue (g ` std) = \<bar>det M\<bar> * measure lebesgue std"
```
```   168     by (subst measure_lebesgue_linear_transformation)
```
```   169        (auto intro: finite_imp_bounded_convex_hull dest: compact_imp_closed simp: g_def std_def)
```
```   170   also have "measure lebesgue std = content std" using compact
```
```   171     by (intro measure_completion) (auto dest: compact_imp_closed)
```
```   172   also have "content std = 1 / fact CARD('n)" unfolding std_def
```
```   173     by (simp add: content_std_simplex)
```
```   174   also have "g ` std = convex hull (g ` insert 0 Basis)" unfolding std_def
```
```   175     by (rule convex_hull_linear_image) (auto simp: g_def)
```
```   176   also have "g ` insert 0 Basis = insert 0 (g ` Basis)"
```
```   177     by (auto simp: g_def)
```
```   178   also have "g ` Basis = (\<lambda>x. x - x0) ` range f"
```
```   179     by (auto simp: g_def Basis_vec_def image_iff)
```
```   180   also have "range f = X - {x0}" using bij
```
```   181     using bij_betw_imp_surj_on by blast
```
```   182   also note eq [symmetric]
```
```   183   finally show ?thesis
```
```   184     using finite_imp_compact_convex_hull[OF \<open>finite X\<close>] by (auto dest: compact_imp_closed)
```
```   185 qed
```
```   186
```
```   187 theorem content_triangle:
```
```   188   fixes A B C :: "real ^ 2"
```
```   189   shows "content (convex hull {A, B, C}) =
```
```   190            \<bar>(C \$ 1 - A \$ 1) * (B \$ 2 - A \$ 2) - (B \$ 1 - A \$ 1) * (C \$ 2 - A \$ 2)\<bar> / 2"
```
```   191 proof -
```
```   192   define M :: "real ^ 2 ^ 2" where "M \<equiv> (\<chi> i. \<chi> j. (if j = 1 then B else C) \$ i - A \$ i)"
```
```   193   define g where "g = (\<lambda>x. M *v x)"
```
```   194   define std where "std = (convex hull insert 0 Basis :: (real ^ 2) set)"
```
```   195   have [simp]: "M *v axis i 1 = (if i = 1 then B - A else C - A)" for i
```
```   196     by (auto simp: M_def matrix_vector_mult_basis column_def vec_eq_iff)
```
```   197   have compact: "compact std" unfolding std_def
```
```   198     by (intro finite_imp_compact_convex_hull) auto
```
```   199
```
```   200   have "measure lebesgue (convex hull {A, B, C}) =
```
```   201           measure lebesgue (((+) (-A)) ` (convex hull {A, B, C}))"
```
```   202     by (rule measure_translation [symmetric])
```
```   203   also have "((+) (-A)) ` (convex hull {A, B, C}) = convex hull (((+) (-A)) ` {A, B, C})"
```
```   204     by (rule convex_hull_translation [symmetric])
```
```   205   also have "((+) (-A)) ` {A, B, C} = {0, B - A, C - A}"
```
```   206     by (auto simp: image_iff)
```
```   207   finally have eq: "measure lebesgue (convex hull {A, B, C}) =
```
```   208                       measure lebesgue (convex hull {0, B - A, C - A})" .
```
```   209
```
```   210   from compact have "measure lebesgue (g ` std) = \<bar>det M\<bar> * measure lebesgue std"
```
```   211     by (subst measure_lebesgue_linear_transformation)
```
```   212        (auto intro: finite_imp_bounded_convex_hull dest: compact_imp_closed simp: g_def std_def)
```
```   213   also have "measure lebesgue std = content std" using compact
```
```   214     by (intro measure_completion) (auto dest: compact_imp_closed)
```
```   215   also have "content std = 1 / 2" unfolding std_def
```
```   216     by (simp add: content_std_simplex)
```
```   217   also have "g ` std = convex hull (g ` insert 0 Basis)" unfolding std_def
```
```   218     by (rule convex_hull_linear_image) (auto simp: g_def)
```
```   219   also have "g ` insert 0 Basis = insert 0 (g ` Basis)"
```
```   220     by (auto simp: g_def)
```
```   221   also have "(2 :: 2) \<noteq> 1" by auto
```
```   222   hence "\<not>(\<forall>y::2. y = 1)" by blast
```
```   223   hence "g ` Basis = {B - A, C - A}"
```
```   224     by (auto simp: g_def Basis_vec_def image_iff)
```
```   225   also note eq [symmetric]
```
```   226   finally show ?thesis
```
```   227     using finite_imp_compact_convex_hull[of "{A, B, C}"]
```
```   228     by (auto dest!: compact_imp_closed simp: det_2 M_def)
```
```   229 qed
```
```   230
```
```   231 theorem heron:
```
```   232   fixes A B C :: "real ^ 2"
```
```   233   defines "a \<equiv> dist B C" and "b \<equiv> dist A C" and "c \<equiv> dist A B"
```
```   234   defines "s \<equiv> (a + b + c) / 2"
```
```   235   shows   "content (convex hull {A, B, C}) = sqrt (s * (s - a) * (s - b) * (s - c))"
```
```   236 proof -
```
```   237   have [simp]: "(UNIV :: 2 set) = {1, 2}"
```
```   238     using exhaust_2 by auto
```
```   239   have dist_eq: "dist (A :: real ^ 2) B ^ 2 = (A \$ 1 - B \$ 1) ^ 2 + (A \$ 2 - B \$ 2) ^ 2"
```
```   240     for A B by (simp add: dist_vec_def dist_real_def)
```
```   241   have nonneg: "s * (s - a) * (s - b) * (s - c) \<ge> 0"
```
```   242     using dist_triangle[of A B C] dist_triangle[of A C B] dist_triangle[of B C A]
```
```   243     by (intro mult_nonneg_nonneg) (auto simp: s_def a_def b_def c_def dist_commute)
```
```   244
```
```   245   have "16 * content (convex hull {A, B, C}) ^ 2 =
```
```   246           4 * ((C \$ 1 - A \$ 1) * (B \$ 2 - A \$ 2) - (B \$ 1 - A \$ 1) * (C \$ 2 - A \$ 2)) ^ 2"
```
```   247     by (subst content_triangle) (simp add: power_divide)
```
```   248   also have "\<dots> = (2 * (dist A B ^ 2 * dist A C ^ 2 + dist A B ^ 2 * dist B C ^ 2 +
```
```   249       dist A C ^ 2 * dist B C ^ 2) - (dist A B ^ 2) ^ 2 - (dist A C ^ 2) ^ 2 - (dist B C ^ 2) ^ 2)"
```
```   250     unfolding dist_eq unfolding power2_eq_square by algebra
```
```   251   also have "\<dots> = (a + b + c) * ((a + b + c) - 2 * a) * ((a + b + c) - 2 * b) *
```
```   252                     ((a + b + c) - 2 * c)"
```
```   253     unfolding power2_eq_square by (simp add: s_def a_def b_def c_def algebra_simps)
```
```   254   also have "\<dots> = 16 * s * (s - a) * (s - b) * (s - c)"
```
```   255     by (simp add: s_def divide_simps mult_ac)
```
```   256   finally have "content (convex hull {A, B, C}) ^ 2 = s * (s - a) * (s - b) * (s - c)"
```
```   257     by simp
```
```   258   also have "\<dots> = sqrt (s * (s - a) * (s - b) * (s - c)) ^ 2"
```
```   259     by (intro real_sqrt_pow2 [symmetric] nonneg)
```
```   260   finally show ?thesis using nonneg
```
```   261     by (subst (asm) power2_eq_iff_nonneg) auto
```
```   262 qed
```
```   263
```
```   264 end
```