(* File: Analysis/Simplex_Content.thy Author: Manuel Eberl <manuel@pruvisto.org> 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⇩_{M}A (λ_. lborel)) (S A t ∩ space (Pi⇩_{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⇩_{M}A (λ_. lborel))" { fix A :: "'a set" and t :: real assume "finite A" have "S A t ∩ space (Pi⇩_{M}A (λ_. lborel)) = Pi⇩_{E}A (λ_. {0..}) ∩ (λx. sum x A) -` {..t} ∩ space (Pi⇩_{M}A (λ_. lborel))" by (auto simp: S_def space_PiM) also have "… ∈ sets (Pi⇩_{M}A (λ_. lborel))" using ‹finite A› by measurable finally have "S A t ∩ space (Pi⇩_{M}A (λ_. lborel)) ∈ sets (Pi⇩_{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 "… = (∫⇧^{+}y. ∫⇧^{+}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 "… = (∫⇧^{+}y. ∫⇧^{+}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 "… = (∫⇧^{+}y. indicator {0..t} y * (∫⇧^{+}x. indicator (S A (t - y) ∩ space (?M A)) x ∂?M A) ∂lborel)" using ‹finite A› by (subst nn_integral_cmult) auto also have "… = (∫⇧^{+}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 "… = (∫⇧^{+}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 "… = (∫⇧^{+}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 "(∫⇧^{+}y. indicator {0..t} y * (t - y) ^ card A ∂lborel) = (∫⇧^{+}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 "(∫⇧^{+}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_remove) (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⇩_{M}Basis (λb. lborel)) borel (λf. ∑b∈Basis. f b *⇩_{R}b)) {x::'a. (∀i∈Basis. 0 ≤ x ∙ i) ∧ sum ((∙) x) Basis ≤ 1}" by (subst lborel_eq) simp also have "… = emeasure (Pi⇩_{M}Basis (λb. lborel)) ({y::'a ⇒ real. (∀i∈Basis. 0 ≤ y i) ∧ sum y Basis ≤ 1} ∩ space (Pi⇩_{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 *) proposition 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 field_split_simps) 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