Theory Unit_Geometry
theory Unit_Geometry
imports
"HOL-Analysis.Polytope"
Polygon_Jordan_Curve
Triangle_Lemmas
begin
section "Measure Setup"
lemma finite_convex_is_measurable:
fixes p :: "(real^2) set"
assumes "p = convex hull l" and "finite l"
shows "p ∈ sets lebesgue"
proof-
have "polytope p"
unfolding polytope_def using assms by force
hence "compact p" using polytope_imp_compact by auto
thus ?thesis using lmeasurable_compact by blast
qed
lemma unit_square_lebesgue: "unit_square ∈ sets lebesgue"
using finite_convex_is_measurable by auto
lemma unit_triangle_lebesgue: "unit_triangle ∈ sets lebesgue"
using finite_convex_is_measurable by auto
lemma unit_triangle_lmeasurable: "unit_triangle ∈ lmeasurable"
by (simp add: bounded_convex_hull bounded_set_imp_lmeasurable unit_triangle_lebesgue)
section "Unit Triangle"
lemma unit_triangle_vts_not_collinear:
"¬ collinear {(vector [0, 0])::real^2, vector [1, 0], vector [0, 1]}"
(is "¬ collinear {?a, ?b, ?c}")
proof(rule ccontr)
assume "¬ ¬ collinear {?a, ?b, ?c}"
then have "collinear {?a, ?b, ?c}" by auto
then obtain u :: "real^2" where u: "u ≠ 0 ∧
(∀x∈{?a, ?b, ?c}. ∀y∈{?a, ?b, ?c}. ∃c. x - y = c *⇩R u)"
by (meson collinear)
then obtain c1 c2 where c1: "?b - ?a = c1 *⇩R u" and c2: "?c - ?a = c2 *⇩R u" by blast
then have "c1 *⇩R u = ?b"
by (metis (no_types, opaque_lifting) diff_zero scaleR_eq_0_iff vector_2(1) vector_2(2) vector_minus_component vector_scaleR_component zero_neq_one)
moreover have "c2 *⇩R u = ?c" using c1 c2 calculation by force
ultimately have "u$1 = 0 ∧ u$2 = 0"
by (metis scaleR_eq_0_iff vector_2(1) vector_2(2) vector_scaleR_component zero_neq_one)
then have "u = 0"
by (metis (mono_tags, opaque_lifting) exhaust_2 vec_eq_iff zero_index)
moreover have "u ≠ 0" using u by auto
ultimately show False by auto
qed
lemma unit_triangle_convex:
assumes "p = (make_polygonal_path [vector [0, 0], vector [1, 0], vector [0, 1], vector[0, 0]])"
(is "p = make_polygonal_path [?O, ?e1, ?e2, ?O]")
shows "convex (path_inside p)"
proof-
have "¬ collinear {?O, ?e1, ?e2}" by (simp add: unit_triangle_vts_not_collinear)
thus ?thesis using triangle_is_convex make_triangle_def assms by force
qed
lemma unit_triangle_char:
shows "unit_triangle = {x. 0 ≤ x $ 1 ∧ 0 ≤ x $ 2 ∧ x $ 1 + x $ 2 ≤ 1}"
(is "unit_triangle = ?S")
proof-
have "unit_triangle ⊆ ?S"
proof(rule subsetI)
fix x assume "x ∈ unit_triangle"
then obtain a b c where
"x = a *⇩R (vector [0, 0]) + b *⇩R (vector [1, 0]) + c *⇩R (vector [0, 1])
∧ a ≥ 0 ∧ b ≥ 0 ∧ c ≥ 0 ∧ a + b + c = 1"
using convex_hull_3 by blast
thus "x ∈ {x. 0 ≤ x $ 1 ∧ 0 ≤ x $ 2 ∧ x $ 1 + x $ 2 ≤ 1}" by simp
qed
moreover have "?S ⊆ unit_triangle"
proof(rule subsetI)
fix x assume "x ∈ ?S"
then obtain b c where bc: "x$1 = b ∧ x$2 = c ∧ 0 ≤ b ∧ 0 ≤ c ∧ b + c ≤ 1" by blast
moreover then obtain a where "a ≥ 0 ∧ a + b + c = 1" using that[of "1 - b - c"] by argo
moreover have "a *⇩R ((vector [0, 0])::(real^2)) = vector [0, 0]" by (simp add: vec_scaleR_2)
moreover have "x = (a *⇩R vector [0, 0]) + (b *⇩R vector [1, 0]) + (c *⇩R vector [0, 1])"
using segment_horizontal bc by fastforce
ultimately show "x ∈ unit_triangle" using convex_hull_3 by blast
qed
ultimately show ?thesis by blast
qed
lemma unit_triangle_interior_char:
shows "interior unit_triangle = {x. 0 < x $ 1 ∧ 0 < x $ 2 ∧ x $ 1 + x $ 2 < 1}"
(is "interior unit_triangle = ?S")
proof-
have "interior unit_triangle ⊆ ?S"
proof(rule subsetI)
fix x assume "x ∈ interior unit_triangle"
moreover have "DIM(real^2) = 2" by simp
ultimately obtain a b c where
"x = a *⇩R (vector [0, 0]) + b *⇩R (vector [1, 0]) + c *⇩R (vector [0, 1])
∧ a > 0 ∧ b > 0 ∧ c > 0 ∧ a + b + c = 1"
using interior_convex_hull_3_minimal[of "(vector [0, 0])::(real^2)" "(vector [1, 0])::(real^2)" "(vector [0, 1])::(real^2)"]
using unit_triangle_vts_not_collinear
by auto
thus "x ∈ {x. 0 < x $ 1 ∧ 0 < x $ 2 ∧ x $ 1 + x $ 2 < 1}" by simp
qed
moreover have "?S ⊆ interior unit_triangle"
proof(rule subsetI)
fix x assume "x ∈ ?S"
then obtain b c where bc: "x$1 = b ∧ x$2 = c ∧ 0 < b ∧ 0 < c ∧ b + c < 1" by blast
moreover then obtain a where "a > 0 ∧ a + b + c = 1" using that[of "1 - b - c"] by argo
moreover have "a *⇩R ((vector [0, 0])::(real^2)) = vector [0, 0]" by (simp add: vec_scaleR_2)
moreover have "x = (a *⇩R vector [0, 0]) + (b *⇩R vector [1, 0]) + (c *⇩R vector [0, 1])"
using segment_horizontal bc by fastforce
moreover have "DIM(real^2) = 2" by simp
ultimately show "x ∈ interior unit_triangle"
using interior_convex_hull_3_minimal[of "(vector [0, 0])::(real^2)" "(vector [1, 0])::(real^2)" "(vector [0, 1])::(real^2)"]
using unit_triangle_vts_not_collinear
by fast
qed
ultimately show ?thesis by blast
qed
lemma unit_triangle_is_elementary: "elem_triangle (vector [0, 0]) (vector [1, 0]) (vector [0, 1])"
(is "elem_triangle ?a ?b ?c")
proof-
let ?UT = "unit_triangle"
have "¬ collinear {?a, ?b, ?c}" using unit_triangle_vts_not_collinear by auto
moreover have "integral_vec ?a ∧ integral_vec ?b ∧ integral_vec ?c"
by (simp add: integral_vec_def is_int_def)
moreover have "{x ∈ ?UT. integral_vec x} = {?a, ?b, ?c}" (is "?UT_integral = ?abc")
proof-
have "?UT_integral ⊇ ?abc" using calculation(2) hull_subset by fastforce
moreover have "?UT_integral ⊆ ?abc"
proof -
have "⋀x. x ∈ unit_triangle ⟹ integral_vec x ⟹ x ≠ vector [0, 0] ⟹ x ≠ vector [1, 0] ⟹ x ≠ vector [0, 1] ⟹ False"
proof-
fix x
assume *: "x ∈ unit_triangle"
"integral_vec x"
" x ≠ vector [0, 0]"
"x ≠ vector [1, 0]"
"x ≠ vector [0, 1]"
then have x_inset: "x ∈{x. 0 ≤ x $ 1 ∧ 0 ≤ x $ 2 ∧ x $ 1 + x $ 2 ≤ 1}"
using unit_triangle_char by auto
have "x $ 1 = 1 ⟹ x $ 2 ≠ 0"
using *
by (smt (verit, del_insts) exhaust_2 vec_eq_iff vector_2(1) vector_2(2))
then have "x $ 1 = 1 ⟹ x $ 1 + x $ 2 > 1 ∨ x $ 2 < 0"
using *(2) unfolding integral_vec_def is_int_def
by linarith
then have x1_not_1: "x$1 = 1 ⟹ False"
using x_inset by simp
have "x $ 1 = 0 ⟹ x $ 2 ≠ 0 ∧ x $ 2 ≠ 1"
using *
by (smt (verit, del_insts) exhaust_2 vec_eq_iff vector_2(1) vector_2(2))
then have "x $ 1 = 0 ⟹ x $ 1 + x $ 2 > 1 ∨ x $ 1 + x $ 2 < 0"
using *(2) unfolding integral_vec_def is_int_def
by auto
then have x1_not_0: "x $ 1 = 0 ⟹ False"
using x_inset by simp
have x1_not_lt0: "x $ 1 < 0 ⟹ False"
using x_inset by auto
have x1_not_gt1: "x $ 1 > 1 ⟹ False"
using x_inset by auto
then show "False" using x1_not_0 x1_not_1 x1_not_lt0 x1_not_gt1
using *(2) unfolding integral_vec_def is_int_def
by force
qed
then have "∃x ∈ ?UT_integral. x ∉ ?abc ∧ integral_vec x ⟹ False"
by blast
then show ?thesis by blast
qed
ultimately show ?thesis by blast
qed
ultimately show ?thesis unfolding elem_triangle_def by auto
qed
lemma unit_triangles_same_area:
"measure lebesgue unit_triangle' = measure lebesgue unit_triangle"
proof-
let ?a = "(vector [1, 1])::real^2"
let ?b = "(vector [0, 1])::real^2"
let ?c = "(vector [1, 0])::real^2"
let ?A = "triangle_affine ?a ?b ?c"
let ?L = "triangle_linear ?a ?b ?c"
have collinear_second_component: "⋀c::real^2. collinear {?a, ?b, c} ⟹ c $ 2 = 1"
proof -
fix p
assume "collinear {?a, ?b, p} "
then obtain u where u_prop: "∀x∈{vector [1, 1], vector [0, 1], p}.
∀y∈{vector [1, 1], vector [0, 1], p}. ∃c. x - y = c *⇩R u"
unfolding collinear_def by auto
then have c_ab: "∃c. ?a - ?b = c *⇩R u"
by blast
then have u_2: "u $ 2 = 0"
using vector_2
by (metis cancel_comm_monoid_add_class.diff_cancel diff_zero scaleR_eq_0_iff vector_minus_component vector_scaleR_component zero_neq_one)
have u_1: "u$1 ≠ 0"
using c_ab vector_2
by (smt (z3) scaleR_right_diff_distrib vector_minus_component vector_scaleR_component)
then have "(∃c. ?a - p = c *⇩R u) ∧ (∃c. ?b - p = c *⇩R u)"
using u_prop by blast
then show "p $ 2 = 1"
using u_1 u_2
by (metis eq_iff_diff_eq_0 scaleR_zero_right vector_2(2) vector_minus_component vector_scaleR_component)
qed
have "unit_triangle' = convex hull {?a, ?b, ?c}" by (simp add: insert_commute)
then have "?A ` unit_triangle = unit_triangle'" using triangle_affine_img[of ?a ?b ?c] by argo
moreover have "abs (det (matrix ?L)) = 1"
proof-
have "matrix ?L = transpose (vector [?b - ?a, ?c - ?a])"
unfolding triangle_linear_def
by (simp add: triangle_mat_def)
also have "det ... = det (vector [?b - ?a, ?c - ?a])" using det_transpose by blast
also have "... = (?b - ?a)$1 * (?c - ?a)$2 - (?c - ?a)$1 * (?b - ?a)$2"
using det_2 by (metis mult.commute vector_2(1) vector_2(2))
finally show ?thesis by simp
qed
moreover have "¬ collinear {?a, ?b, ?c}" using collinear_second_component vector_2 by force
ultimately have "measure lebesgue unit_triangle' = integral unit_triangle (λ(x::real^2). 1)"
using triangle_measure_integral_of_det[of ?a ?b ?c]
by (smt (verit, ccfv_SIG) Henstock_Kurzweil_Integration.integral_cong insert_commute)
also have "... = measure lebesgue unit_triangle"
by (simp add: lmeasure_integral unit_triangle_lmeasurable)
finally show ?thesis .
qed
section "Unit Square"
lemma convex_hull_4:
"convex hull {a,b,c,d} = { u *⇩R a + v *⇩R b + w *⇩R c + t *⇩R d | u v w t. 0 ≤ u ∧ 0 ≤ v ∧ 0 ≤ w ∧ 0 ≤ t ∧ u + v + w + t = 1}"
proof -
have fin: "finite {a,b,c,d}" "finite {b,c,d}" "finite {c,d}" "finite {d}"
by auto
have *: "⋀x y z w ::real. x + y + z + w = 1 ⟷ x = 1 - y - z - w"
by (auto simp: field_simps)
show ?thesis
unfolding convex_hull_finite[OF fin(1)]
unfolding convex_hull_finite_step[OF fin(2)]
unfolding convex_hull_finite_step[OF fin(3)]
unfolding convex_hull_finite_step[OF fin(4)]
unfolding *
apply auto
apply (smt (verit, ccfv_threshold) add.commute diff_add_cancel diff_diff_eq)
subgoal for v w t
apply (rule exI [where x="1 - v - w - t"], simp)
apply (rule exI [where x=v], simp)
apply (rule exI [where x=w], simp)
apply (rule exI [where x="λx. t"], simp)
done
done
qed
lemma unit_square_characterization_helper:
fixes a b :: real
assumes "0 ≤ a ∧ a ≤ 1 ∧ 0 ≤ b ∧ b ≤ 1" and
"a ≤ b"
obtains u v w t where
"vector [a, b] = u *⇩R ((vector [0, 0])::real^2)
+ v *⇩R (vector [0, 1])
+ w *⇩R (vector [1, 1])
+ t *⇩R (vector [1, 0])
∧ 0 ≤ u ∧ 0 ≤ v ∧ 0 ≤ w ∧ 0 ≤ t ∧ u + v + w + t = 1"
proof-
let ?a = "(vector [0, 0])::(real^2)"
let ?b = "(vector [0, 1])::(real^2)"
let ?c = "(vector [1, 1])::(real^2)"
let ?d = "(vector [1, 0])::(real^2)"
let ?w = "a"
let ?v = "b - a"
let ?u = "(1 - ?w - ?v)::real"
let ?t = "0::real"
let ?T = "{u *⇩R ?a + v *⇩R ?b + w *⇩R ?c + t *⇩R ?d | u v w t. 0 ≤ u ∧ 0 ≤ v ∧ 0 ≤ w ∧ 0 ≤ t ∧ u + v + w + t = 1}"
have "?u *⇩R ?a = 0"
by (smt (verit, del_insts) exhaust_2 scaleR_zero_right vec_eq_iff vector_2(1) vector_2(2) zero_index)
moreover have "?w *⇩R ?c = vector [a, a]"
proof-
have "(?w *⇩R ?c)$1 = a" by simp
moreover have "(?w *⇩R ?c)$2 = a" by simp
ultimately show ?thesis by (smt (verit) vec_eq_iff exhaust_2 vector_2(1) vector_2(2))
qed
moreover have "?v *⇩R ?b = vector [0, b - a]"
proof-
have "(?v *⇩R ?b)$1 = 0" by fastforce
moreover have "(?v *⇩R ?b)$2 = b - a" by simp
ultimately show ?thesis by (smt (verit) vec_eq_iff exhaust_2 vector_2(1) vector_2(2))
qed
ultimately have "?u *⇩R ?a + ?v *⇩R ?b + ?w *⇩R ?c + ?t *⇩R ?d = vector [0, b - a] + vector [a, a]"
by fastforce
also have "... = vector [a, b]"
by (smt (verit, del_insts) diff_add_cancel exhaust_2 vec_eq_iff vector_2(1) vector_2(2) vector_add_component)
finally have "vector [a, b] = ?u *⇩R ?a + ?v *⇩R ?b + ?w *⇩R ?c + ?t *⇩R ?d" by presburger
moreover have "0 ≤ ?u ∧ ?u ≤ 1 ∧ 0 ≤ ?v ∧ ?v ≤ 1" using assms by simp
moreover have "0 ≤ ?w ∧ ?w ≤ 1 ∧ 0 ≤ ?t ∧ ?t ≤ 1" using assms by simp
moreover have "?u + ?v + ?w + ?t = 1" by argo
ultimately show ?thesis using that[of ?u ?v ?w ?t] by blast
qed
lemma unit_square_characterization:
"unit_square = {x. 0 ≤ x$1 ∧ x$1 ≤ 1 ∧ 0 ≤ x$2 ∧ x$2 ≤ 1}" (is "unit_square = ?S")
proof-
let ?a = "(vector [0, 0])::(real^2)"
let ?b = "(vector [0, 1])::(real^2)"
let ?c = "(vector [1, 1])::(real^2)"
let ?d = "(vector [1, 0])::(real^2)"
let ?T = "{u *⇩R ?a + v *⇩R ?b + w *⇩R ?c + t *⇩R ?d | u v w t. 0 ≤ u ∧ 0 ≤ v ∧ 0 ≤ w ∧ 0 ≤ t ∧ u + v + w + t = 1}"
have "unit_square = ?T" using convex_hull_4 by blast
moreover have "?T ⊆ ?S"
proof(rule subsetI)
fix x
assume "x ∈ ?T"
then obtain u v w t where "x = u *⇩R ?a + v *⇩R ?b + w *⇩R ?c + t *⇩R ?d" and
"0 ≤ u" and "0 ≤ v" and "0 ≤ w" and "0 ≤ t" and "u + v + w + t = 1" by auto
moreover from this have
"x$1 = u * 0 + v * 0 + w * 1 + t * 1 ∧ x$2 = u * 0 + v * 1 + w * 1 + t * 0" by simp
ultimately have "0 ≤ x$1 ∧ x$1 ≤ 1 ∧ 0 ≤ x$2 ∧ x$2 ≤ 1" by linarith
thus "x ∈ ?S" by blast
qed
moreover have "?S ⊆ ?T"
proof(rule subsetI)
fix x :: "real^2"
assume *: "x ∈ ?S"
{ assume "x$1 < x$2"
then have "x$1 ≤ x$2" by fastforce
then obtain u v w t where "vector [x$1, x$2] = u *⇩R ?a + v *⇩R ?b + w *⇩R ?c + t *⇩R ?d ∧ 0 ≤ u ∧ 0 ≤ v ∧ 0 ≤ w ∧ 0 ≤ t ∧ u + v + w + t = 1"
using * unit_square_characterization_helper[of "x$1" "x$2"] by blast
moreover have "x = vector [x$1, x$2]"
by (smt (verit, ccfv_threshold) exhaust_2 vec_eq_iff vector_2(1) vector_2(2))
ultimately have "x ∈ ?T" by force
} moreover
{ assume "x$1 ≥ x$2"
then obtain u v w t where **: "vector [x$2, x$1] = u *⇩R ?a + v *⇩R ?b + w *⇩R ?c + t *⇩R ?d ∧ 0 ≤ u ∧ 0 ≤ v ∧ 0 ≤ w ∧ 0 ≤ t ∧ u + v + w + t = 1"
using * unit_square_characterization_helper[of "x$2" "x$1"] by blast
have x1: "x$1 = v + w" using **
by (smt (verit, ccfv_threshold) mult_cancel_left1 real_scaleR_def scaleR_zero_right vector_2(2) vector_add_component vector_scaleR_component)
have x2: "x$2 = w + t" using **
by (smt (verit) mult_cancel_left1 real_scaleR_def scaleR_zero_right vector_2(1) vector_add_component vector_scaleR_component)
have "(u *⇩R ?a + t *⇩R ?b + w *⇩R ?c + v *⇩R ?d)$1 = w + v" by auto
moreover have "(u *⇩R ?a + t *⇩R ?b + w *⇩R ?c + v *⇩R ?d)$2 = t + w" by fastforce
ultimately have "u *⇩R ?a + t *⇩R ?b + w *⇩R ?c + v *⇩R ?d = vector [w + v, t + w]"
by (smt (verit) vec_eq_iff exhaust_2 vector_2(1) vector_2(2))
also have "... = x" using x1 x2
by (smt (verit, del_insts) add.commute exhaust_2 vec_eq_iff vector_2(1) vector_2(2))
ultimately have "x ∈ ?T"
by (smt (verit, ccfv_SIG) ** mem_Collect_eq)
}
ultimately show "x ∈ ?T" by argo
qed
ultimately show ?thesis by auto
qed
lemma e1e2_basis:
defines "e1 ≡ (vector [1, 0])::(real^2)" and
"e2 ≡ (vector [0, 1])::(real^2)"
shows "e1 = axis 1 (1::real)" and "e1 ∈ (Basis::((real^2) set))" and
"e2 = axis 2 (1::real)" and "e2 ∈ (Basis::((real^2) set))"
proof-
have "(1::real) ∈ Basis" by simp
then have "axis 1 (1::real) ∈ (⋃i. ⋃u∈(Basis::(real set)). {axis i u})" by blast
moreover show e1_axis: "e1 = axis 1 (1::real)"
unfolding axis_def vector_def e1_def by auto
ultimately show e1_basis: "e1 ∈ (Basis::((real^2) set))" by simp
have "(1::real) ∈ Basis" by simp
then have "axis 1 (1::real) ∈ (⋃i. ⋃u∈(Basis::(real set)). {axis i u})" by blast
moreover show e2_axis: "e2 = axis 2 (1::real)"
unfolding axis_def vector_def e2_def by auto
ultimately show e2_basis: "e2 ∈ (Basis::((real^2) set))" by simp
qed
lemma unit_square_cbox: "unit_square = cbox (vector [0, 0]) (vector [1, 1])"
proof-
let ?O = "(vector [0, 0])::(real^2)"
let ?e1 = "(vector [1, 0])::(real^2)"
let ?e2 = "(vector [0, 1])::(real^2)"
let ?I = "(vector [1, 1])::(real^2)"
let ?cbox = "{x. ∀i∈Basis. ?O ∙ i ≤ x ∙ i ∧ x ∙ i ≤ ?I ∙ i}"
have "unit_square = {x. 0 ≤ x$1 ∧ x$1 ≤ 1 ∧ 0 ≤ x$2 ∧ x$2 ≤ 1}" (is "unit_square = ?S")
using unit_square_characterization by auto
moreover have "?S ⊆ ?cbox"
proof(rule subsetI)
fix x
assume *: "x ∈ ?S"
have "?O ∙ ?e1 ≤ x ∙ ?e1 ∧ x ∙ ?e1 ≤ ?I ∙ ?e1"
using e1e2_basis
by (smt (verit, del_insts) * cart_eq_inner_axis mem_Collect_eq vector_2(1))
moreover have "?O ∙ ?e2 ≤ x ∙ ?e2 ∧ x ∙ ?e2 ≤ ?I ∙ ?e2"
using e1e2_basis
by (smt (verit, del_insts) * cart_eq_inner_axis mem_Collect_eq vector_2(2))
ultimately show "x ∈ ?cbox"
by (smt (verit, best) * axis_index cart_eq_inner_axis exhaust_2 mem_Collect_eq vector_2(1) vector_2(2))
qed
moreover have "?cbox ⊆ ?S"
proof(rule subsetI)
fix x :: "real^2"
assume *: "x ∈ ?cbox"
then have "0 ≤ ?e1 ∙ x" using e1e2_basis
by (metis (no_types, lifting) cart_eq_inner_axis inner_commute mem_Collect_eq vector_2(1))
moreover have "?e1 ∙ x ≤ 1" using e1e2_basis
by (smt (verit, ccfv_SIG) * inner_axis inner_commute mem_Collect_eq real_inner_1_right vector_2(1))
moreover have "0 ≤ ?e2 ∙ x"
by (metis (no_types, lifting) * cart_eq_inner_axis e1e2_basis(3) e1e2_basis(4) inner_commute mem_Collect_eq vector_2(2))
moreover have "?e2 ∙ x ≤ 1"
by (metis (no_types, lifting) * cart_eq_inner_axis e1e2_basis(3) e1e2_basis(4) inner_commute mem_Collect_eq vector_2(2))
moreover have "?e1 ∙ x = x$1"
by (simp add: cart_eq_inner_axis e1e2_basis inner_commute)
moreover have "?e2 ∙ x = x$2"
by (simp add: cart_eq_inner_axis e1e2_basis inner_commute)
ultimately show "x ∈ ?S" by force
qed
ultimately show ?thesis unfolding cbox_def by order
qed
lemma unit_square_area: "measure lebesgue unit_square = 1"
proof-
let ?e1 = "(vector [1, 0])::(real^2)"
let ?e2 = "(vector [0, 1])::(real^2)"
have "unit_square = cbox (vector [0, 0]) (vector [1, 1])" (is "unit_square = cbox ?O ?I")
using unit_square_cbox by blast
also have "emeasure lborel ... = 1" using emeasure_lborel_cbox_eq
proof-
have "?I ∙ ?e1 = (1::real)"
by (simp add: e1e2_basis(1) inner_axis' inner_commute)
moreover have "?I ∙ ?e2 = (1::real)" by (simp add: e1e2_basis(3) inner_axis' inner_commute)
ultimately have basis_dot: "∀b ∈ Basis. ?I ∙ b = 1"
by (metis (full_types) axis_inverse e1e2_basis(1) e1e2_basis(3) exhaust_2)
have "?O ∙ ?e1 ≤ ?I ∙ ?e1" by (simp add: e1e2_basis(1) inner_axis)
moreover have "?O ∙ ?e2 ≤ ?I ∙ ?e2" by (simp add: e1e2_basis(3) inner_axis)
ultimately have "∀b ∈ Basis. ?O ∙ b ≤ ?I ∙ b"
by (smt (verit, ccfv_threshold) axis_index cart_eq_inner_axis exhaust_2 insert_iff vector_2(1) vector_2(2))
then have "emeasure lborel (cbox ?O ?I) = (∏b∈Basis. (?I - ?O) ∙ b)"
using emeasure_lborel_cbox_eq by auto
also have "... = (∏b∈Basis. ?I ∙ b)"
by (smt (verit, del_insts) axis_index diff_zero euclidean_all_zero_iff exhaust_2 inner_axis real_inner_1_right vector_2(1) vector_2(2))
also have "... = (∏b∈Basis. (1::real))" using basis_dot by fastforce
finally show ?thesis by simp
qed
finally have "emeasure lborel unit_square = 1" .
moreover have "emeasure lborel unit_square = measure lebesgue unit_square"
by (simp add: emeasure_eq_measure2 unit_square_cbox)
ultimately show ?thesis by fastforce
qed
section "Unit Triangle Area is 1/2"
lemma unit_triangle'_char:
shows "unit_triangle' = {x. x $ 1 ≤ 1 ∧ x $ 2 ≤ 1 ∧ x $ 1 + x $ 2 ≥ 1}"
proof -
let ?I = "(vector [1, 1])::real^2"
let ?e1 = "(vector [1, 0])::real^2"
let ?e2 = "(vector [0, 1])::real^2"
have "unit_triangle' = {u *⇩R ?I + v *⇩R ?e1 + w *⇩R ?e2 | u v w. 0 ≤ u ∧ 0 ≤ v ∧ 0 ≤ w ∧ u + v + w = 1}"
using convex_hull_3[of ?I ?e1 ?e2] by auto
moreover have "⋀u v w. u *⇩R ?I + v *⇩R ?e1 + w *⇩R ?e2 = ((vector [u + v, u + w])::real^2)"
proof-
fix u v w :: real
let ?v_e1 = "((vector [v, 0])::real^2)"
let ?w_e2 = "((vector [0, w])::real^2)"
let ?u_I = "((vector [u, u])::real^2)"
have "u *⇩R ?I = ?u_I" using vec_scaleR_2 by simp
moreover have "v *⇩R ?e1 = ?v_e1" using vec_scaleR_2 by simp
moreover have "w *⇩R ?e2 = ?w_e2" using vec_scaleR_2 by simp
ultimately have 1: "u *⇩R ?I + v *⇩R ?e1 + w *⇩R ?e2 = ?u_I + ?v_e1 + ?w_e2" by argo
moreover have "(?u_I + ?v_e1 + ?w_e2)$1 = u + v"
using vector_add_component by simp
moreover have "(?u_I + ?v_e1 + ?w_e2)$2 = u + w"
using vector_add_component by simp
ultimately have "?u_I + ?v_e1 + ?w_e2 = ((vector [u + v, u + w])::real^2)"
using vector_2 exhaust_2 by (smt (verit, del_insts) vec_eq_iff)
thus "u *⇩R ?I + v *⇩R ?e1 + w *⇩R ?e2 = ((vector [u + v, u + w])::real^2)" using 1 by argo
qed
ultimately have 1: "unit_triangle' = {(vector[u + v, u + w])::real^2 | u v w. 0 ≤ u ∧ 0 ≤ v ∧ 0 ≤ w ∧ u + v + w = 1}"
(is "unit_triangle' = ?S")
by presburger
have "unit_triangle' = {(vector[x, y])::real^2 | x y. 0 ≤ x ∧ x ≤ 1 ∧ 0 ≤ y ∧ y ≤ 1 ∧ x + y ≥ 1}"
(is "unit_triangle' = ?T")
proof-
have "⋀x y::real. ∃u v w. 0 ≤ u ∧ 0 ≤ v ∧ 0 ≤ w ∧ u + v + w = 1 ∧ x = u + v ∧ y = u + w
⟹ 0 ≤ x ∧ x ≤ 1 ∧ 0 ≤ y ∧ y ≤ 1 ∧ x + y ≥ 1" by force
moreover have *: "⋀x y::real. 0 ≤ x ∧ x ≤ 1 ∧ 0 ≤ y ∧ y ≤ 1 ∧ x + y ≥ 1
⟹ ∃u v w. 0 ≤ u ∧ 0 ≤ v ∧ 0 ≤ w ∧ u + v + w = 1 ∧ x = u + v ∧ y = u + w"
proof-
fix x y :: real
let ?u = "y + x - 1"
let ?v = "1 - y"
let ?w = "1 - x"
assume "0 ≤ x ∧ x ≤ 1 ∧ 0 ≤ y ∧ y ≤ 1 ∧ 1 ≤ x + y"
then have "0 ≤ ?u ∧ 0 ≤ ?v ∧ 0 ≤ ?w ∧ ?u + ?v + ?w = 1 ∧ x = ?u + ?v ∧ y = ?u + ?w" by argo
thus "∃u v w. 0 ≤ u ∧ 0 ≤ v ∧ 0 ≤ w ∧ u + v + w = 1 ∧ x = u + v ∧ y = u + w" by blast
qed
ultimately have "∀x y::real. ((∃u v w. 0 ≤ u ∧ 0 ≤ v ∧ 0 ≤ w ∧ u + v + w = 1 ∧ x = u + v ∧ y = u + w)
⟷ (0 ≤ x ∧ x ≤ 1 ∧ 0 ≤ y ∧ y ≤ 1 ∧ x + y ≥ 1))"
by metis
then have "∀z::real^2. ((∃u v w. 0 ≤ u ∧ 0 ≤ v ∧ 0 ≤ w ∧ u + v + w = 1 ∧ z$1 = u + v ∧ z$2 = u + w)
⟷ (0 ≤ z$1 ∧ z$1 ≤ 1 ∧ 0 ≤ z$2 ∧ z$2 ≤ 1 ∧ z$1 + z$2 ≥ 1))" by presburger
then have "∀z::real^2. ((∃u v w. 0 ≤ u ∧ 0 ≤ v ∧ 0 ≤ w ∧ u + v + w = 1 ∧ z = vector [u + v, u + w])
⟷ (∃x y. 0 ≤ x ∧ x ≤ 1 ∧ 0 ≤ y ∧ y ≤ 1 ∧ x + y ≥ 1 ∧ z = vector [x, y]))"
by (smt (verit) *)
moreover have "∀z::real^2. z ∈ ?S ⟷ (∃u v w. 0 ≤ u ∧ 0 ≤ v ∧ 0 ≤ w ∧ u + v + w = 1 ∧ z = vector [u + v, u + w])"
by blast
moreover have "∀z::real^2. z ∈ ?T ⟷ (∃x y. 0 ≤ x ∧ x ≤ 1 ∧ 0 ≤ y ∧ y ≤ 1 ∧ x + y ≥ 1 ∧ z = vector [x, y])"
by blast
ultimately have "?S = ?T" by auto
then show ?thesis using 1 by auto
qed
moreover have "{x. 0 ≤ x$1 ∧ x$1 ≤ 1 ∧ 0 ≤ x$2 ∧ x$2 ≤ 1 ∧ x$1 + x$2 ≥ 1} ⊆ ?T"
proof(rule subsetI)
fix z :: "real^2"
assume *: "z ∈ {x. 0 ≤ x$1 ∧ x$1 ≤ 1 ∧ 0 ≤ x$2 ∧ x$2 ≤ 1 ∧ x$1 + x$2 ≥ 1}"
then obtain x y :: real where "z = vector[x, y] ∧ 0 ≤ x" using forall_vector_2 by fastforce
moreover from this have "x ≤ 1 ∧ 0 ≤ y ∧ y ≤ 1 ∧ x + y ≥ 1" using * vector_2[of x y] by simp
ultimately show "z ∈ ?T" by blast
qed
moreover have "?T ⊆ {x. 0 ≤ x$1 ∧ x$1 ≤ 1 ∧ 0 ≤ x$2 ∧ x$2 ≤ 1 ∧ x$1 + x$2 ≥ 1}"
using vector_2 by force
ultimately show ?thesis
by (smt (verit, best) Collect_cong subset_antisym)
qed
lemma unit_square_split_diag:
shows "unit_square = unit_triangle ∪ unit_triangle'"
proof-
let ?S = "({vector [0, 0], vector [0, 1], vector [1, 0]})::((real^2) set)"
let ?S' = "({vector [1, 1], vector [0, 1], vector [1, 0]})::((real^2) set)"
have "unit_triangle ∪ unit_triangle' ⊆ convex hull (?S ∪ ?S')" by (simp add: hull_mono)
moreover have "convex hull (?S ∪ ?S') ⊆ unit_triangle ∪ unit_triangle'"
by (smt (z3) Un_commute Un_left_commute Un_upper1 in_mono insert_is_Un mem_Collect_eq subsetI sup.idem unit_square_characterization unit_triangle_char unit_triangle'_char)
moreover have "unit_square = convex hull (?S ∪ ?S')" by (simp add: insert_commute)
ultimately show ?thesis by blast
qed
lemma unit_triangle_INT_unit_triangle'_measure:
"measure lebesgue (unit_triangle ∩ unit_triangle') = 0"
proof -
let ?e1 = "(vector [1, 0])::real^2"
let ?e2 = "(vector [0, 1])::real^2"
have "unit_triangle ∩ unit_triangle' = {x::(real^2). 0 ≤ x $ 1 ∧ x $ 1 ≤ 1 ∧ 0 ≤ x $ 2 ∧ x $ 2 ≤ 1 ∧ x $ 1 + x $ 2 = 1}"
(is "unit_triangle ∩ unit_triangle' = ?S")
using unit_triangle_char unit_triangle'_char
by auto
also have "... = path_image (linepath ?e2 ?e1)"
(is "... = ?p")
proof-
have "?S ⊆ ?p"
proof(rule subsetI)
fix x :: "real^2"
assume "x ∈ ?S"
then have *: "0 ≤ 1 - x$2 ∧ x$2 = 1 - x$1 ∧ 0 ≤ x$2 ∧ x$2 ≤ 1" by simp
have "x$2 *⇩R ?e2 + x$1 *⇩R ?e1 = vector[x$1, x$2]"
proof-
have "(x$1 *⇩R ?e1)$1 = x$1" by simp
moreover have "(x$1 *⇩R ?e1)$2 = 0" by auto
moreover have "(x$2 *⇩R ?e2)$1 = 0" by auto
moreover have "(x$2 *⇩R ?e2)$2 = x$2" by fastforce
ultimately have "x$1 *⇩R ?e1 = vector [x$1, 0] ∧ x$2 *⇩R ?e2 = vector [0, x$2]"
by (smt (verit, ccfv_SIG) exhaust_2 vec_eq_iff vector_2(1) vector_2(2))
then have "x$1 *⇩R ?e1 + x$2 *⇩R ?e2 = vector [x$1, 0] + vector [0, x$2]" by auto
moreover from this have "(x$1 *⇩R ?e1 + x$2 *⇩R ?e2)$1 = x$1" by auto
moreover from calculation have "(x$1 *⇩R ?e1 + x$2 *⇩R ?e2)$2 = x$2" by auto
ultimately show ?thesis
by (smt (verit) add.commute exhaust_2 vec_eq_iff vector_2(1) vector_2(2))
qed
also have "... = x"
by (smt (verit, best) exhaust_2 vec_eq_iff vector_2(1) vector_2(2))
finally have "x$2 *⇩R ?e2 + x$1 *⇩R ?e1 = x" .
then have "x = (λx. (1 - x) *⇩R ?e2 + x *⇩R ?e1) (x$1) ∧ x$1 ∈ {0..1}" using * by auto
thus "x ∈ ?p" unfolding path_image_def linepath_def by fast
qed
moreover have "?p ⊆ ?S"
proof(rule subsetI)
fix x
assume *: "x ∈ ?p"
then obtain t where *: "x = (1 - t) *⇩R ?e2 + t *⇩R ?e1 ∧ t ∈ {0..1}"
unfolding path_image_def linepath_def by blast
moreover from this have "x$1 = t" by simp
moreover from calculation have "x$2 = 1 - t" by simp
moreover from calculation have "0 ≤ t ∧ t ≤ 1 ∧ 0 ≤ 1 - t ∧ 1 - t ≤ 1" by simp
ultimately show "x ∈ ?S" by simp
qed
ultimately show ?thesis by blast
qed
also have "measure lebesgue ?p = 0" using linepath_has_measure_0 by blast
finally show ?thesis .
qed
lemma unit_triangle_area: "measure lebesgue unit_triangle = 1/2"
proof-
let ?μ = "measure lebesgue"
have "?μ unit_square = ?μ unit_triangle + ?μ unit_triangle'"
using unit_square_split_diag unit_triangle_INT_unit_triangle'_measure
by (simp add: finite_imp_bounded_convex_hull measurable_convex measure_Un3)
thus ?thesis using unit_triangles_same_area unit_square_area by simp
qed
end