# HG changeset patch # User Manuel Eberl # Date 1531502838 -3600 # Node ID 2ec84498f56248f83b592ff3b5267a3c9ef8446c # Parent 205d352ed727bcc44822519f8e3333eb9c8fbbc0 HOL-Analysis: Volume of a simplex, Heron's theorem diff -r 205d352ed727 -r 2ec84498f562 src/HOL/Analysis/Analysis.thy --- a/src/HOL/Analysis/Analysis.thy Fri Jul 13 16:54:36 2018 +0100 +++ b/src/HOL/Analysis/Analysis.thy Fri Jul 13 18:27:18 2018 +0100 @@ -25,6 +25,7 @@ Gamma_Function Change_Of_Vars Lipschitz + Simplex_Content begin end diff -r 205d352ed727 -r 2ec84498f562 src/HOL/Analysis/Simplex_Content.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Analysis/Simplex_Content.thy Fri Jul 13 18:27:18 2018 +0100 @@ -0,0 +1,263 @@ +(* + File: Analysis/Simplex_Content.thy + Author: Manuel Eberl + + The content of an n-dimensional simplex, including the formula for the content of a + triangle and Heron's formula. +*) +section \Volume of a simplex\ +theory Simplex_Content + imports Change_Of_Vars +begin + +lemma fact_neq_top_ennreal [simp]: "fact n \ (top :: ennreal)" + by (induction n) (auto simp: ennreal_mult_eq_top_iff) + +lemma ennreal_fact: "ennreal (fact n) = fact n" + by (induction n) (auto simp: ennreal_mult algebra_simps ennreal_of_nat_eq_real_of_nat) + +context + fixes S :: "'a set \ real \ ('a \ real) set" + defines "S \ (\A t. {x. (\i\A. 0 \ x i) \ sum x A \ t})" +begin + +lemma emeasure_std_simplex_aux_step: + assumes "b \ A" "finite A" + shows "x(b := y) \ S (insert b A) t \ y \ {0..t} \ x \ S A (t - y)" + using assms sum_nonneg[of A x] unfolding S_def + by (force simp: sum_delta_notmem algebra_simps) + +lemma emeasure_std_simplex_aux: + fixes t :: real + assumes "finite (A :: 'a set)" "t \ 0" + shows "emeasure (Pi\<^sub>M A (\_. lborel)) + (S A t \ space (Pi\<^sub>M A (\_. lborel))) = t ^ card A / fact (card A)" + using assms(1,2) +proof (induction arbitrary: t rule: finite_induct) + case (empty t) + thus ?case by (simp add: PiM_empty S_def) +next + case (insert b A t) + define n where "n = Suc (card A)" + have n_pos: "n > 0" by (simp add: n_def) + let ?M = "\A. (Pi\<^sub>M A (\_. lborel))" + { + fix A :: "'a set" and t :: real assume "finite A" + have "S A t \ space (Pi\<^sub>M A (\_. lborel)) = + Pi\<^sub>E A (\_. {0..}) \ (\x. sum x A) -` {..t} \ space (Pi\<^sub>M A (\_. lborel))" + by (auto simp: S_def space_PiM) + also have "\ \ sets (Pi\<^sub>M A (\_. lborel))" + using \finite A\ by measurable + finally have "S A t \ space (Pi\<^sub>M A (\_. lborel)) \ sets (Pi\<^sub>M A (\_. lborel))" . + } note meas [measurable] = this + + interpret product_sigma_finite "\_. lborel" + by standard + have "emeasure (?M (insert b A)) (S (insert b A) t \ space (?M (insert b A))) = + nn_integral (?M (insert b A)) + (\x. indicator (S (insert b A) t \ space (?M (insert b A))) x)" + using insert.hyps by (subst nn_integral_indicator) auto + also have "\ = (\\<^sup>+ y. \\<^sup>+ x. indicator (S (insert b A) t \ space (?M (insert b A))) + (x(b := y)) \?M A \lborel)" + using insert.prems insert.hyps by (intro product_nn_integral_insert_rev) auto + also have "\ = (\\<^sup>+ y. \\<^sup>+ x. indicator {0..t} y * indicator (S A (t - y) \ space (?M A)) x + \?M A \lborel)" + using insert.hyps insert.prems emeasure_std_simplex_aux_step[of b A] + by (intro nn_integral_cong) + (auto simp: fun_eq_iff indicator_def space_PiM PiE_def extensional_def) + also have "\ = (\\<^sup>+ y. indicator {0..t} y * (\\<^sup>+ x. indicator (S A (t - y) \ space (?M A)) x + \?M A) \lborel)" using \finite A\ + by (subst nn_integral_cmult) auto + also have "\ = (\\<^sup>+ y. indicator {0..t} y * emeasure (?M A) (S A (t - y) \ space (?M A)) \lborel)" + using \finite A\ by (subst nn_integral_indicator) auto + also have "\ = (\\<^sup>+ y. indicator {0..t} y * (t - y) ^ card A / ennreal (fact (card A)) \lborel)" + using insert.IH by (intro nn_integral_cong) (auto simp: indicator_def divide_ennreal) + also have "\ = (\\<^sup>+ y. indicator {0..t} y * (t - y) ^ card A \lborel) / ennreal (fact (card A))" + using \finite A\ by (subst nn_integral_divide) auto + also have "(\\<^sup>+ y. indicator {0..t} y * (t - y) ^ card A \lborel) = + (\\<^sup>+y\{0..t}. ennreal ((t - y) ^ (n - 1)) \lborel)" + by (intro nn_integral_cong) (auto simp: indicator_def n_def) + also have "((\x. - ((t - x) ^ n / n)) has_real_derivative (t - x) ^ (n - 1)) (at x)" + if "x \ {0..t}" for x by (rule derivative_eq_intros refl | simp add: n_pos)+ + hence "(\\<^sup>+y\{0..t}. ennreal ((t - y) ^ (n - 1)) \lborel) = + ennreal (-((t - t) ^ n / n) - (-((t - 0) ^ n / n)))" + using insert.prems insert.hyps by (intro nn_integral_FTC_Icc) auto + also have "\ = ennreal (t ^ n / n)" using n_pos by (simp add: zero_power) + also have "\ / ennreal (fact (card A)) = ennreal (t ^ n / n / fact (card A))" + using n_pos \t \ 0\ by (subst divide_ennreal) auto + also have "t ^ n / n / fact (card A) = t ^ n / fact n" + by (simp add: n_def) + also have "n = card (insert b A)" + using insert.hyps by (subst card_insert) (auto simp: n_def) + finally show ?case . +qed + +end + +lemma emeasure_std_simplex: + "emeasure lborel (convex hull (insert 0 Basis :: 'a :: euclidean_space set)) = + ennreal (1 / fact DIM('a))" +proof - + have "emeasure lborel {x::'a. (\i\Basis. 0 \ x \ i) \ sum ((\) x) Basis \ 1} = + emeasure (distr (Pi\<^sub>M Basis (\b. lborel)) borel (\f. \b\Basis. f b *\<^sub>R b)) + {x::'a. (\i\Basis. 0 \ x \ i) \ sum ((\) x) Basis \ 1}" + by (subst lborel_eq) simp + also have "\ = emeasure (Pi\<^sub>M Basis (\b. lborel)) + ({y::'a \ real. (\i\Basis. 0 \ y i) \ sum y Basis \ 1} \ + space (Pi\<^sub>M Basis (\b. lborel)))" + by (subst emeasure_distr) auto + also have "\ = ennreal (1 / fact DIM('a))" + by (subst emeasure_std_simplex_aux) auto + finally show ?thesis by (simp only: std_simplex) +qed + +theorem content_std_simplex: + "measure lborel (convex hull (insert 0 Basis :: 'a :: euclidean_space set)) = + 1 / fact DIM('a)" + by (simp add: measure_def emeasure_std_simplex) + +(* TODO: move to Change_of_Vars *) +lemma measure_lebesgue_linear_transformation: + fixes A :: "(real ^ 'n :: {finite, wellorder}) set" + fixes f :: "_ \ real ^ 'n :: {finite, wellorder}" + assumes "bounded A" "A \ sets lebesgue" "linear f" + shows "measure lebesgue (f ` A) = \det (matrix f)\ * measure lebesgue A" +proof - + from assms have [intro]: "A \ lmeasurable" + by (intro bounded_set_imp_lmeasurable) auto + hence [intro]: "f ` A \ lmeasurable" + by (intro lmeasure_integral measurable_linear_image assms) + have "measure lebesgue (f ` A) = integral (f ` A) (\_. 1)" + by (intro lmeasure_integral measurable_linear_image assms) auto + also have "\ = integral (f ` A) (\_. 1 :: real ^ 1) $ 0" + by (subst integral_component_eq_cart [symmetric]) (auto intro: integrable_on_const) + also have "\ = \det (matrix f)\ * integral A (\x. 1 :: real ^ 1) $ 0" + using assms + by (subst integral_change_of_variables_linear) + (auto simp: o_def absolutely_integrable_on_def intro: integrable_on_const) + also have "integral A (\x. 1 :: real ^ 1) $ 0 = integral A (\x. 1)" + by (subst integral_component_eq_cart [symmetric]) (auto intro: integrable_on_const) + also have "\ = measure lebesgue A" + by (intro lmeasure_integral [symmetric]) auto + finally show ?thesis . +qed + +theorem content_simplex: + fixes X :: "(real ^ 'n :: {finite, wellorder}) set" and f :: "'n :: _ \ real ^ ('n :: _)" + assumes "finite X" "card X = Suc CARD('n)" and x0: "x0 \ X" and bij: "bij_betw f UNIV (X - {x0})" + defines "M \ (\ i. \ j. f j $ i - x0 $ i)" + shows "content (convex hull X) = \det M\ / fact (CARD('n))" +proof - + define g where "g = (\x. M *v x)" + have [simp]: "M *v axis i 1 = f i - x0" for i :: 'n + by (simp add: M_def matrix_vector_mult_basis column_def vec_eq_iff) + define std where "std = (convex hull insert 0 Basis :: (real ^ 'n :: _) set)" + have compact: "compact std" unfolding std_def + by (intro finite_imp_compact_convex_hull) auto + + have "measure lebesgue (convex hull X) = measure lebesgue (((+) (-x0)) ` (convex hull X))" + by (rule measure_translation [symmetric]) + also have "((+) (-x0)) ` (convex hull X) = convex hull (((+) (-x0)) ` X)" + by (rule convex_hull_translation [symmetric]) + also have "((+) (-x0)) ` X = insert 0 ((\x. x - x0) ` (X - {x0}))" + using x0 by (auto simp: image_iff) + finally have eq: "measure lebesgue (convex hull X) = measure lebesgue (convex hull \)" . + + from compact have "measure lebesgue (g ` std) = \det M\ * measure lebesgue std" + by (subst measure_lebesgue_linear_transformation) + (auto intro: finite_imp_bounded_convex_hull dest: compact_imp_closed simp: g_def std_def) + also have "measure lebesgue std = content std" using compact + by (intro measure_completion) (auto dest: compact_imp_closed) + also have "content std = 1 / fact CARD('n)" unfolding std_def + by (simp add: content_std_simplex) + also have "g ` std = convex hull (g ` insert 0 Basis)" unfolding std_def + by (rule convex_hull_linear_image) (auto simp: g_def) + also have "g ` insert 0 Basis = insert 0 (g ` Basis)" + by (auto simp: g_def) + also have "g ` Basis = (\x. x - x0) ` range f" + by (auto simp: g_def Basis_vec_def image_iff) + also have "range f = X - {x0}" using bij + using bij_betw_imp_surj_on by blast + also note eq [symmetric] + finally show ?thesis + using finite_imp_compact_convex_hull[OF \finite X\] by (auto dest: compact_imp_closed) +qed + +theorem content_triangle: + fixes A B C :: "real ^ 2" + shows "content (convex hull {A, B, C}) = + \(C $ 1 - A $ 1) * (B $ 2 - A $ 2) - (B $ 1 - A $ 1) * (C $ 2 - A $ 2)\ / 2" +proof - + define M :: "real ^ 2 ^ 2" where "M \ (\ i. \ j. (if j = 1 then B else C) $ i - A $ i)" + define g where "g = (\x. M *v x)" + define std where "std = (convex hull insert 0 Basis :: (real ^ 2) set)" + have [simp]: "M *v axis i 1 = (if i = 1 then B - A else C - A)" for i + by (auto simp: M_def matrix_vector_mult_basis column_def vec_eq_iff) + have compact: "compact std" unfolding std_def + by (intro finite_imp_compact_convex_hull) auto + + have "measure lebesgue (convex hull {A, B, C}) = + measure lebesgue (((+) (-A)) ` (convex hull {A, B, C}))" + by (rule measure_translation [symmetric]) + also have "((+) (-A)) ` (convex hull {A, B, C}) = convex hull (((+) (-A)) ` {A, B, C})" + by (rule convex_hull_translation [symmetric]) + also have "((+) (-A)) ` {A, B, C} = {0, B - A, C - A}" + by (auto simp: image_iff) + finally have eq: "measure lebesgue (convex hull {A, B, C}) = + measure lebesgue (convex hull {0, B - A, C - A})" . + + from compact have "measure lebesgue (g ` std) = \det M\ * measure lebesgue std" + by (subst measure_lebesgue_linear_transformation) + (auto intro: finite_imp_bounded_convex_hull dest: compact_imp_closed simp: g_def std_def) + also have "measure lebesgue std = content std" using compact + by (intro measure_completion) (auto dest: compact_imp_closed) + also have "content std = 1 / 2" unfolding std_def + by (simp add: content_std_simplex) + also have "g ` std = convex hull (g ` insert 0 Basis)" unfolding std_def + by (rule convex_hull_linear_image) (auto simp: g_def) + also have "g ` insert 0 Basis = insert 0 (g ` Basis)" + by (auto simp: g_def) + also have "(2 :: 2) \ 1" by auto + hence "\(\y::2. y = 1)" by blast + hence "g ` Basis = {B - A, C - A}" + by (auto simp: g_def Basis_vec_def image_iff) + also note eq [symmetric] + finally show ?thesis + using finite_imp_compact_convex_hull[of "{A, B, C}"] + by (auto dest!: compact_imp_closed simp: det_2 M_def) +qed + +theorem heron: + fixes A B C :: "real ^ 2" + defines "a \ dist B C" and "b \ dist A C" and "c \ dist A B" + defines "s \ (a + b + c) / 2" + shows "content (convex hull {A, B, C}) = sqrt (s * (s - a) * (s - b) * (s - c))" +proof - + have [simp]: "(UNIV :: 2 set) = {1, 2}" + using exhaust_2 by auto + have dist_eq: "dist (A :: real ^ 2) B ^ 2 = (A $ 1 - B $ 1) ^ 2 + (A $ 2 - B $ 2) ^ 2" + for A B by (simp add: dist_vec_def dist_real_def) + have nonneg: "s * (s - a) * (s - b) * (s - c) \ 0" + using dist_triangle[of A B C] dist_triangle[of A C B] dist_triangle[of B C A] + by (intro mult_nonneg_nonneg) (auto simp: s_def a_def b_def c_def dist_commute) + + have "16 * content (convex hull {A, B, C}) ^ 2 = + 4 * ((C $ 1 - A $ 1) * (B $ 2 - A $ 2) - (B $ 1 - A $ 1) * (C $ 2 - A $ 2)) ^ 2" + by (subst content_triangle) (simp add: power_divide) + also have "\ = (2 * (dist A B ^ 2 * dist A C ^ 2 + dist A B ^ 2 * dist B C ^ 2 + + dist A C ^ 2 * dist B C ^ 2) - (dist A B ^ 2) ^ 2 - (dist A C ^ 2) ^ 2 - (dist B C ^ 2) ^ 2)" + unfolding dist_eq unfolding power2_eq_square by algebra + also have "\ = (a + b + c) * ((a + b + c) - 2 * a) * ((a + b + c) - 2 * b) * + ((a + b + c) - 2 * c)" + unfolding power2_eq_square by (simp add: s_def a_def b_def c_def algebra_simps) + also have "\ = 16 * s * (s - a) * (s - b) * (s - c)" + by (simp add: s_def divide_simps mult_ac) + finally have "content (convex hull {A, B, C}) ^ 2 = s * (s - a) * (s - b) * (s - c)" + by simp + also have "\ = sqrt (s * (s - a) * (s - b) * (s - c)) ^ 2" + by (intro real_sqrt_pow2 [symmetric] nonneg) + finally show ?thesis using nonneg + by (subst (asm) power2_eq_iff_nonneg) auto +qed + +end