Theory Euler_Formula
section ‹Euler's Polyhedron Formula›
text ‹One of the Famous 100 Theorems, ported from HOL Light›
text‹Cited source:
Lawrence, J. (1997). A Short Proof of Euler's Relation for Convex Polytopes.
\emph{Canadian Mathematical Bulletin}, \textbf{40}(4), 471--474.›
theory Euler_Formula
imports
"HOL-Analysis.Analysis"
begin
text‹ Interpret which "side" of a hyperplane a point is on. ›
definition hyperplane_side
where "hyperplane_side ≡ λ(a,b). λx. sgn (a ∙ x - b)"
text‹ Equivalence relation imposed by a hyperplane arrangement. ›
definition hyperplane_equiv
where "hyperplane_equiv ≡ λA x y. ∀h ∈ A. hyperplane_side h x = hyperplane_side h y"
lemma hyperplane_equiv_refl [iff]: "hyperplane_equiv A x x"
by (simp add: hyperplane_equiv_def)
lemma hyperplane_equiv_sym:
"hyperplane_equiv A x y ⟷ hyperplane_equiv A y x"
by (auto simp: hyperplane_equiv_def)
lemma hyperplane_equiv_trans:
"⟦hyperplane_equiv A x y; hyperplane_equiv A y z⟧ ⟹ hyperplane_equiv A x z"
by (auto simp: hyperplane_equiv_def)
lemma hyperplane_equiv_Un:
"hyperplane_equiv (A ∪ B) x y ⟷ hyperplane_equiv A x y ∧ hyperplane_equiv B x y"
by (meson Un_iff hyperplane_equiv_def)
subsection‹ Cells of a hyperplane arrangement›
definition hyperplane_cell :: "('a::real_inner × real) set ⇒ 'a set ⇒ bool"
where "hyperplane_cell ≡ λA C. ∃x. C = Collect (hyperplane_equiv A x)"
lemma hyperplane_cell: "hyperplane_cell A C ⟷ (∃x. C = {y. hyperplane_equiv A x y})"
by (simp add: hyperplane_cell_def)
lemma not_hyperplane_cell_empty [simp]: "¬ hyperplane_cell A {}"
using hyperplane_cell by auto
lemma nonempty_hyperplane_cell: "hyperplane_cell A C ⟹ (C ≠ {})"
by auto
lemma Union_hyperplane_cells: "⋃ {C. hyperplane_cell A C} = UNIV"
using hyperplane_cell by blast
lemma disjoint_hyperplane_cells:
"⟦hyperplane_cell A C1; hyperplane_cell A C2; C1 ≠ C2⟧ ⟹ disjnt C1 C2"
by (force simp: hyperplane_cell_def disjnt_iff hyperplane_equiv_def)
lemma disjoint_hyperplane_cells_eq:
"⟦hyperplane_cell A C1; hyperplane_cell A C2⟧ ⟹ (disjnt C1 C2 ⟷ (C1 ≠ C2))"
using disjoint_hyperplane_cells by auto
lemma hyperplane_cell_empty [iff]: "hyperplane_cell {} C ⟷ C = UNIV"
by (simp add: hyperplane_cell hyperplane_equiv_def)
lemma hyperplane_cell_singleton_cases:
assumes "hyperplane_cell {(a,b)} C"
shows "C = {x. a ∙ x = b} ∨ C = {x. a ∙ x < b} ∨ C = {x. a ∙ x > b}"
proof -
obtain x where x: "C = {y. hyperplane_side (a, b) x = hyperplane_side (a, b) y}"
using assms by (auto simp: hyperplane_equiv_def hyperplane_cell)
then show ?thesis
by (auto simp: hyperplane_side_def sgn_if split: if_split_asm)
qed
lemma hyperplane_cell_singleton:
"hyperplane_cell {(a,b)} C ⟷
(if a = 0 then C = UNIV else C = {x. a ∙ x = b} ∨ C = {x. a ∙ x < b} ∨ C = {x. a ∙ x > b})"
apply (simp add: hyperplane_cell_def hyperplane_equiv_def hyperplane_side_def sgn_if split: if_split_asm)
by (smt (verit) Collect_cong gt_ex hyperplane_eq_Ex lt_ex)
lemma hyperplane_cell_Un:
"hyperplane_cell (A ∪ B) C ⟷
C ≠ {} ∧
(∃C1 C2. hyperplane_cell A C1 ∧ hyperplane_cell B C2 ∧ C = C1 ∩ C2)"
by (auto simp: hyperplane_cell hyperplane_equiv_def)
lemma finite_hyperplane_cells:
"finite A ⟹ finite {C. hyperplane_cell A C}"
proof (induction rule: finite_induct)
case (insert p A)
obtain a b where peq: "p = (a,b)"
by fastforce
have "Collect (hyperplane_cell {p}) ⊆ {{x. a ∙ x = b},{x. a ∙ x < b},{x. a ∙ x > b}}"
using hyperplane_cell_singleton_cases
by (auto simp: peq)
then have *: "finite (Collect (hyperplane_cell {p}))"
by (simp add: finite_subset)
define 𝒞 where "𝒞 ≡ (⋃C1 ∈ {C. hyperplane_cell A C}. ⋃C2 ∈ {C. hyperplane_cell {p} C}. {C1 ∩ C2})"
have "{a. hyperplane_cell (insert p A) a} ⊆ 𝒞"
using hyperplane_cell_Un [of "{p}" A] by (auto simp: 𝒞_def)
moreover have "finite 𝒞"
using * 𝒞_def insert.IH by blast
ultimately show ?case
using finite_subset by blast
qed auto
lemma finite_restrict_hyperplane_cells:
"finite A ⟹ finite {C. hyperplane_cell A C ∧ P C}"
by (simp add: finite_hyperplane_cells)
lemma finite_set_of_hyperplane_cells:
"⟦finite A; ⋀C. C ∈ 𝒞 ⟹ hyperplane_cell A C⟧ ⟹ finite 𝒞"
by (metis finite_hyperplane_cells finite_subset mem_Collect_eq subsetI)
lemma pairwise_disjoint_hyperplane_cells:
"(⋀C. C ∈ 𝒞 ⟹ hyperplane_cell A C) ⟹ pairwise disjnt 𝒞"
by (metis disjoint_hyperplane_cells pairwiseI)
lemma hyperplane_cell_Int_open_affine:
assumes "finite A" "hyperplane_cell A C"
obtains S T where "open S" "affine T" "C = S ∩ T"
using assms
proof (induction arbitrary: thesis C rule: finite_induct)
case empty
then show ?case
by auto
next
case (insert p A thesis C')
obtain a b where peq: "p = (a,b)"
by fastforce
obtain C C1 where C1: "hyperplane_cell {(a,b)} C1" and C: "hyperplane_cell A C"
and "C' ≠ {}" and C': "C' = C1 ∩ C"
by (metis hyperplane_cell_Un insert.prems(2) insert_is_Un peq)
then obtain S T where ST: "open S" "affine T" "C = S ∩ T"
by (meson insert.IH)
show ?case
proof (cases "a=0")
case True
with insert.prems show ?thesis
by (metis C1 Int_commute ST ‹C' = C1 ∩ C› hyperplane_cell_singleton inf_top.right_neutral)
next
case False
then consider "C1 = {x. a ∙ x = b}" | "C1 = {x. a ∙ x < b}" | "C1 = {x. b < a ∙ x}"
by (metis C1 hyperplane_cell_singleton)
then show ?thesis
proof cases
case 1
then show thesis
by (metis C' ST affine_Int affine_hyperplane inf_left_commute insert.prems(1))
next
case 2
with ST show thesis
by (metis Int_assoc C' insert.prems(1) open_Int open_halfspace_lt)
next
case 3
with ST show thesis
by (metis Int_assoc C' insert.prems(1) open_Int open_halfspace_gt)
qed
qed
qed
lemma hyperplane_cell_relatively_open:
assumes "finite A" "hyperplane_cell A C"
shows "openin (subtopology euclidean (affine hull C)) C"
proof -
obtain S T where "open S" "affine T" "C = S ∩ T"
by (meson assms hyperplane_cell_Int_open_affine)
show ?thesis
proof (cases "S ∩ T = {}")
case True
then show ?thesis
by (simp add: ‹C = S ∩ T›)
next
case False
then have "affine hull (S ∩ T) = T"
by (metis ‹affine T› ‹open S› affine_hull_affine_Int_open hull_same inf_commute)
then show ?thesis
using ‹C = S ∩ T› ‹open S› openin_subtopology by fastforce
qed
qed
lemma hyperplane_cell_relative_interior:
"⟦finite A; hyperplane_cell A C⟧ ⟹ rel_interior C = C"
by (simp add: hyperplane_cell_relatively_open rel_interior_openin)
lemma hyperplane_cell_convex:
assumes "hyperplane_cell A C"
shows "convex C"
proof -
obtain c where c: "C = {y. hyperplane_equiv A c y}"
by (meson assms hyperplane_cell)
have "convex (⋂h∈A. {y. hyperplane_side h c = hyperplane_side h y})"
proof (rule convex_INT)
fix h :: "'a × real"
assume "h ∈ A"
obtain a b where heq: "h = (a,b)"
by fastforce
have [simp]: "{y. ¬ a ∙ c < a ∙ y ∧ a ∙ y = a ∙ c} = {y. a ∙ y = a ∙ c}"
"{y. ¬ b < a ∙ y ∧ a ∙ y ≠ b} = {y. b > a ∙ y}"
by auto
then show "convex {y. hyperplane_side h c = hyperplane_side h y}"
by (fastforce simp: heq hyperplane_side_def sgn_if convex_halfspace_gt convex_halfspace_lt convex_hyperplane cong: conj_cong)
qed
with c show ?thesis
by (simp add: hyperplane_equiv_def INTER_eq)
qed
lemma hyperplane_cell_Inter:
assumes "⋀C. C ∈ 𝒞 ⟹ hyperplane_cell A C"
and "𝒞 ≠ {}" and INT: "⋂𝒞 ≠ {}"
shows "hyperplane_cell A (⋂𝒞)"
proof -
have "⋂𝒞 = {y. hyperplane_equiv A z y}"
if "z ∈ ⋂𝒞" for z
using assms that by (force simp: hyperplane_cell hyperplane_equiv_def)
with INT hyperplane_cell show ?thesis
by fastforce
qed
lemma hyperplane_cell_Int:
"⟦hyperplane_cell A S; hyperplane_cell A T; S ∩ T ≠ {}⟧ ⟹ hyperplane_cell A (S ∩ T)"
by (metis hyperplane_cell_Un sup.idem)
subsection‹ A cell complex is considered to be a union of such cells›
definition hyperplane_cellcomplex
where "hyperplane_cellcomplex A S ≡
∃𝒯. (∀C ∈ 𝒯. hyperplane_cell A C) ∧ S = ⋃𝒯"
lemma hyperplane_cellcomplex_empty [simp]: "hyperplane_cellcomplex A {}"
using hyperplane_cellcomplex_def by auto
lemma hyperplane_cell_cellcomplex:
"hyperplane_cell A C ⟹ hyperplane_cellcomplex A C"
by (auto simp: hyperplane_cellcomplex_def)
lemma hyperplane_cellcomplex_Union:
assumes "⋀S. S ∈ 𝒞 ⟹ hyperplane_cellcomplex A S"
shows "hyperplane_cellcomplex A (⋃ 𝒞)"
proof -
obtain ℱ where ℱ: "⋀S. S ∈ 𝒞 ⟹ (∀C ∈ ℱ S. hyperplane_cell A C) ∧ S = ⋃(ℱ S)"
by (metis assms hyperplane_cellcomplex_def)
show ?thesis
unfolding hyperplane_cellcomplex_def
using ℱ by (fastforce intro: exI [where x="⋃ (ℱ ` 𝒞)"])
qed
lemma hyperplane_cellcomplex_Un:
"⟦hyperplane_cellcomplex A S; hyperplane_cellcomplex A T⟧
⟹ hyperplane_cellcomplex A (S ∪ T)"
by (smt (verit) Un_iff Union_Un_distrib hyperplane_cellcomplex_def)
lemma hyperplane_cellcomplex_UNIV [simp]: "hyperplane_cellcomplex A UNIV"
by (metis Union_hyperplane_cells hyperplane_cellcomplex_def mem_Collect_eq)
lemma hyperplane_cellcomplex_Inter:
assumes "⋀S. S ∈ 𝒞 ⟹ hyperplane_cellcomplex A S"
shows "hyperplane_cellcomplex A (⋂𝒞)"
proof (cases "𝒞 = {}")
case True
then show ?thesis
by simp
next
case False
obtain ℱ where ℱ: "⋀S. S ∈ 𝒞 ⟹ (∀C ∈ ℱ S. hyperplane_cell A C) ∧ S = ⋃(ℱ S)"
by (metis assms hyperplane_cellcomplex_def)
have *: "𝒞 = (λS. ⋃(ℱ S)) ` 𝒞"
using ℱ by force
define U where "U ≡ ⋃ {T ∈ {⋂(g ` 𝒞) |g. ∀S∈𝒞. g S ∈ ℱ S}. T ≠ {}}"
have "⋂𝒞 = ⋃{⋂(g ` 𝒞) |g. ∀S∈𝒞. g S ∈ ℱ S}"
using False ℱ unfolding Inter_over_Union [symmetric]
by blast
also have "… = U"
unfolding U_def
by blast
finally have "⋂𝒞 = U" .
have "hyperplane_cellcomplex A U"
using False ℱ unfolding U_def
apply (intro hyperplane_cellcomplex_Union hyperplane_cell_cellcomplex)
by (auto intro!: hyperplane_cell_Inter)
then show ?thesis
by (simp add: ‹⋂𝒞 = U›)
qed
lemma hyperplane_cellcomplex_Int:
"⟦hyperplane_cellcomplex A S; hyperplane_cellcomplex A T⟧
⟹ hyperplane_cellcomplex A (S ∩ T)"
using hyperplane_cellcomplex_Inter [of "{S,T}"] by force
lemma hyperplane_cellcomplex_Compl:
assumes "hyperplane_cellcomplex A S"
shows "hyperplane_cellcomplex A (- S)"
proof -
obtain 𝒞 where 𝒞: "⋀C. C ∈ 𝒞 ⟹ hyperplane_cell A C" and "S = ⋃𝒞"
by (meson assms hyperplane_cellcomplex_def)
have "hyperplane_cellcomplex A (⋂T ∈ 𝒞. -T)"
proof (intro hyperplane_cellcomplex_Inter)
fix C0
assume "C0 ∈ uminus ` 𝒞"
then obtain C where C: "C0 = -C" "C ∈ 𝒞"
by auto
have *: "-C = ⋃ {D. hyperplane_cell A D ∧ D ≠ C}" (is "_ = ?rhs")
proof
show "- C ⊆ ?rhs"
using hyperplane_cell by blast
show "?rhs ⊆ - C"
by clarify (meson ‹C ∈ 𝒞› 𝒞 disjnt_iff disjoint_hyperplane_cells)
qed
then show "hyperplane_cellcomplex A C0"
by (metis (no_types, lifting) C(1) hyperplane_cell_cellcomplex hyperplane_cellcomplex_Union mem_Collect_eq)
qed
then show ?thesis
by (simp add: ‹S = ⋃ 𝒞› uminus_Sup)
qed
lemma hyperplane_cellcomplex_diff:
"⟦hyperplane_cellcomplex A S; hyperplane_cellcomplex A T⟧
⟹ hyperplane_cellcomplex A (S - T)"
using hyperplane_cellcomplex_Inter [of "{S,-T}"]
by (force simp: Diff_eq hyperplane_cellcomplex_Compl)
lemma hyperplane_cellcomplex_mono:
assumes "hyperplane_cellcomplex A S" "A ⊆ B"
shows "hyperplane_cellcomplex B S"
proof -
obtain 𝒞 where 𝒞: "⋀C. C ∈ 𝒞 ⟹ hyperplane_cell A C" and eq: "S = ⋃𝒞"
by (meson assms hyperplane_cellcomplex_def)
show ?thesis
unfolding eq
proof (intro hyperplane_cellcomplex_Union)
fix C
assume "C ∈ 𝒞"
have "⋀x. x ∈ C ⟹ ∃D'. (∃D. D' = D ∩ C ∧ hyperplane_cell (B - A) D ∧ D ∩ C ≠ {}) ∧ x ∈ D'"
unfolding hyperplane_cell_def by blast
then
have "hyperplane_cellcomplex (A ∪ (B - A)) C"
unfolding hyperplane_cellcomplex_def hyperplane_cell_Un
using 𝒞 ‹C ∈ 𝒞› by (fastforce intro!: exI [where x=" {D ∩ C |D. hyperplane_cell (B - A) D ∧ D ∩ C ≠ {}}"])
moreover have "B = A ∪ (B - A)"
using ‹A ⊆ B› by auto
ultimately show "hyperplane_cellcomplex B C" by simp
qed
qed
lemma finite_hyperplane_cellcomplexes:
assumes "finite A"
shows "finite {C. hyperplane_cellcomplex A C}"
proof -
have "{C. hyperplane_cellcomplex A C} ⊆ image ⋃ {T. T ⊆ {C. hyperplane_cell A C}}"
by (force simp: hyperplane_cellcomplex_def subset_eq)
with finite_hyperplane_cells show ?thesis
by (metis assms finite_Collect_subsets finite_surj)
qed
lemma finite_restrict_hyperplane_cellcomplexes:
"finite A ⟹ finite {C. hyperplane_cellcomplex A C ∧ P C}"
by (simp add: finite_hyperplane_cellcomplexes)
lemma finite_set_of_hyperplane_cellcomplex:
assumes "finite A" "⋀C. C ∈ 𝒞 ⟹ hyperplane_cellcomplex A C"
shows "finite 𝒞"
by (metis assms finite_hyperplane_cellcomplexes mem_Collect_eq rev_finite_subset subsetI)
lemma cell_subset_cellcomplex:
"⟦hyperplane_cell A C; hyperplane_cellcomplex A S⟧ ⟹ C ⊆ S ⟷ ~ disjnt C S"
by (smt (verit) Union_iff disjnt_iff disjnt_subset1 disjoint_hyperplane_cells_eq hyperplane_cellcomplex_def subsetI)
subsection ‹Euler characteristic›
definition Euler_characteristic :: "('a::euclidean_space × real) set ⇒ 'a set ⇒ int"
where "Euler_characteristic A S ≡
(∑C | hyperplane_cell A C ∧ C ⊆ S. (-1) ^ nat (aff_dim C))"
lemma Euler_characteristic_empty [simp]: "Euler_characteristic A {} = 0"
by (simp add: sum.neutral Euler_characteristic_def)
lemma Euler_characteristic_cell_Union:
assumes "⋀C. C ∈ 𝒞 ⟹ hyperplane_cell A C"
shows "Euler_characteristic A (⋃ 𝒞) = (∑C∈𝒞. (- 1) ^ nat (aff_dim C))"
proof -
have "⋀x. ⟦hyperplane_cell A x; x ⊆ ⋃ 𝒞⟧ ⟹ x ∈ 𝒞"
by (metis assms disjnt_Union1 disjnt_subset1 disjoint_hyperplane_cells_eq)
then have "{C. hyperplane_cell A C ∧ C ⊆ ⋃ 𝒞} = 𝒞"
by (auto simp: assms)
then show ?thesis
by (auto simp: Euler_characteristic_def)
qed
lemma Euler_characteristic_cell:
"hyperplane_cell A C ⟹ Euler_characteristic A C = (-1) ^ (nat(aff_dim C))"
using Euler_characteristic_cell_Union [of "{C}"] by force
lemma Euler_characteristic_cellcomplex_Un:
assumes "finite A" "hyperplane_cellcomplex A S"
and AT: "hyperplane_cellcomplex A T" and "disjnt S T"
shows "Euler_characteristic A (S ∪ T) =
Euler_characteristic A S + Euler_characteristic A T"
proof -
have *: "{C. hyperplane_cell A C ∧ C ⊆ S ∪ T} =
{C. hyperplane_cell A C ∧ C ⊆ S} ∪ {C. hyperplane_cell A C ∧ C ⊆ T}"
using cell_subset_cellcomplex [OF _ AT] by (auto simp: disjnt_iff)
have **: "{C. hyperplane_cell A C ∧ C ⊆ S} ∩ {C. hyperplane_cell A C ∧ C ⊆ T} = {}"
using assms cell_subset_cellcomplex disjnt_subset1 by fastforce
show ?thesis
unfolding Euler_characteristic_def
by (simp add: finite_restrict_hyperplane_cells assms * ** flip: sum.union_disjoint)
qed
lemma Euler_characteristic_cellcomplex_Union:
assumes "finite A"
and 𝒞: "⋀C. C ∈ 𝒞 ⟹ hyperplane_cellcomplex A C" "pairwise disjnt 𝒞"
shows "Euler_characteristic A (⋃ 𝒞) = sum (Euler_characteristic A) 𝒞"
proof -
have "finite 𝒞"
using assms finite_set_of_hyperplane_cellcomplex by blast
then show ?thesis
using 𝒞
proof (induction rule: finite_induct)
case empty
then show ?case
by auto
next
case (insert C 𝒞)
then obtain "disjoint 𝒞" "disjnt C (⋃ 𝒞)"
by (metis disjnt_Union2 pairwise_insert)
with insert show ?case
by (simp add: Euler_characteristic_cellcomplex_Un hyperplane_cellcomplex_Union ‹finite A›)
qed
qed
lemma Euler_characteristic:
fixes A :: "('n::euclidean_space * real) set"
assumes "finite A"
shows "Euler_characteristic A S =
(∑d = 0..DIM('n). (-1) ^ d * int (card {C. hyperplane_cell A C ∧ C ⊆ S ∧ aff_dim C = int d}))"
(is "_ = ?rhs")
proof -
have "⋀T. ⟦hyperplane_cell A T; T ⊆ S⟧ ⟹ aff_dim T ∈ {0..DIM('n)}"
by (metis atLeastAtMost_iff nle_le order.strict_iff_not aff_dim_negative_iff
nonempty_hyperplane_cell aff_dim_le_DIM)
then have *: "aff_dim ` {C. hyperplane_cell A C ∧ C ⊆ S} ⊆ int ` {0..DIM('n)}"
by (auto simp: image_int_atLeastAtMost)
have "Euler_characteristic A S = (∑y∈int ` {0..DIM('n)}.
∑C∈{x. hyperplane_cell A x ∧ x ⊆ S ∧ aff_dim x = y}. (- 1) ^ nat y) "
using sum.group [of "{C. hyperplane_cell A C ∧ C ⊆ S}" "int ` {0..DIM('n)}" aff_dim "λC. (-1::int) ^ nat(aff_dim C)", symmetric]
by (simp add: assms Euler_characteristic_def finite_restrict_hyperplane_cells *)
also have "… = ?rhs"
by (simp add: sum.reindex mult_of_nat_commute)
finally show ?thesis .
qed
subsection ‹Show that the characteristic is invariant w.r.t. hyperplane arrangement.›
lemma hyperplane_cells_distinct_lemma:
"{x. a ∙ x = b} ∩ {x. a ∙ x < b} = {} ∧
{x. a ∙ x = b} ∩ {x. a ∙ x > b} = {} ∧
{x. a ∙ x < b} ∩ {x. a ∙ x = b} = {} ∧
{x. a ∙ x < b} ∩ {x. a ∙ x > b} = {} ∧
{x. a ∙ x > b} ∩ {x. a ∙ x = b} = {} ∧
{x. a ∙ x > b} ∩ {x. a ∙ x < b} = {}"
by auto
proposition Euler_characterstic_lemma:
assumes "finite A" and "hyperplane_cellcomplex A S"
shows "Euler_characteristic (insert h A) S = Euler_characteristic A S"
proof -
obtain 𝒞 where 𝒞: "⋀C. C ∈ 𝒞 ⟹ hyperplane_cell A C" and "S = ⋃𝒞"
and "pairwise disjnt 𝒞"
by (meson assms hyperplane_cellcomplex_def pairwise_disjoint_hyperplane_cells)
obtain a b where "h = (a,b)"
by fastforce
have "⋀C. C ∈ 𝒞 ⟹ hyperplane_cellcomplex A C ∧ hyperplane_cellcomplex (insert (a,b) A) C"
by (meson 𝒞 hyperplane_cell_cellcomplex hyperplane_cellcomplex_mono subset_insertI)
moreover
have "sum (Euler_characteristic (insert (a,b) A)) 𝒞 = sum (Euler_characteristic A) 𝒞"
proof (rule sum.cong [OF refl])
fix C
assume "C ∈ 𝒞"
have "Euler_characteristic (insert (a, b) A) C = (-1) ^ nat(aff_dim C)"
proof (cases "hyperplane_cell (insert (a,b) A) C")
case True
then show ?thesis
using Euler_characteristic_cell by blast
next
case False
with 𝒞[OF ‹C ∈ 𝒞›] have "a ≠ 0"
by (smt (verit, ccfv_threshold) hyperplane_cell_Un hyperplane_cell_empty hyperplane_cell_singleton insert_is_Un sup_bot_left)
have "convex C"
using ‹hyperplane_cell A C› hyperplane_cell_convex by blast
define r where "r ≡ (∑D∈{C' ∩ C |C'. hyperplane_cell {(a, b)} C' ∧ C' ∩ C ≠ {}}. (-1::int) ^ nat (aff_dim D))"
have "Euler_characteristic (insert (a, b) A) C
= (∑D | (D ≠ {} ∧
(∃C1 C2. hyperplane_cell {(a, b)} C1 ∧ hyperplane_cell A C2 ∧ D = C1 ∩ C2)) ∧ D ⊆ C.
(- 1) ^ nat (aff_dim D))"
unfolding r_def Euler_characteristic_def insert_is_Un [of _ A] hyperplane_cell_Un ..
also have "… = r"
unfolding r_def
apply (rule sum.cong [OF _ refl])
using ‹hyperplane_cell A C› disjoint_hyperplane_cells disjnt_iff
by (smt (verit, ccfv_SIG) Collect_cong Int_iff disjoint_iff subsetD subsetI)
also have "… = (-1) ^ nat(aff_dim C)"
proof -
have "C ≠ {}"
using ‹hyperplane_cell A C› by auto
show ?thesis
proof (cases "C ⊆ {x. a ∙ x < b} ∨ C ⊆ {x. a ∙ x > b} ∨ C ⊆ {x. a ∙ x = b}")
case Csub: True
with ‹C ≠ {}› have "r = sum (λc. (-1) ^ nat (aff_dim c)) {C}"
unfolding r_def
apply (intro sum.cong [OF _ refl])
by (auto simp: ‹a ≠ 0› hyperplane_cell_singleton)
also have "… = (-1) ^ nat(aff_dim C)"
by simp
finally show ?thesis .
next
case False
then obtain u v where uv: "u ∈ C" "¬ a ∙ u < b" "v ∈ C" "¬ a ∙ v > b"
by blast
have CInt_ne: "C ∩ {x. a ∙ x = b} ≠ {}"
proof (cases "a ∙ u = b ∨ a ∙ v = b")
case True
with uv show ?thesis
by blast
next
case False
have "a ∙ v < a ∙ u"
using False uv by auto
define w where "w ≡ v + ((b - a ∙ v) / (a ∙ u - a ∙ v)) *⇩R (u - v)"
have **: "v + a *⇩R (u - v) = (1 - a) *⇩R v + a *⇩R u" for a
by (simp add: algebra_simps)
have "w ∈ C"
unfolding w_def **
proof (intro convexD_alt)
qed (use ‹a ∙ v < a ∙ u› ‹convex C› uv in auto)
moreover have "w ∈ {x. a ∙ x = b}"
using ‹a ∙ v < a ∙ u› by (simp add: w_def inner_add_right inner_diff_right)
ultimately show ?thesis
by blast
qed
have Cab: "C ∩ {x. a ∙ x < b} ≠ {} ∧ C ∩ {x. b < a ∙ x} ≠ {}"
proof -
obtain u v where "u ∈ C" "a ∙ u = b" "v ∈ C" "a ∙ v ≠ b" "u≠v"
using False ‹C ∩ {x. a ∙ x = b} ≠ {}› by blast
have "openin (subtopology euclidean (affine hull C)) C"
using ‹hyperplane_cell A C› ‹finite A› hyperplane_cell_relatively_open by blast
then obtain ε where "0 < ε"
and ε: "⋀x'. ⟦x' ∈ affine hull C; dist x' u < ε⟧ ⟹ x' ∈ C"
by (meson ‹u ∈ C› openin_euclidean_subtopology_iff)
define ξ where "ξ ≡ u - (ε / 2 / norm (v - u)) *⇩R (v - u)"
have "ξ ∈ C"
proof (rule ε)
show "ξ ∈ affine hull C"
by (simp add: ξ_def ‹u ∈ C› ‹v ∈ C› hull_inc mem_affine_3_minus2)
qed (use ξ_def ‹0 < ε› in force)
consider "a ∙ v < b" | "a ∙ v > b"
using ‹a ∙ v ≠ b› by linarith
then show ?thesis
proof cases
case 1
moreover have "ξ ∈ {x. b < a ∙ x}"
using "1" ‹0 < ε› ‹a ∙ u = b› divide_less_cancel
by (fastforce simp: ξ_def algebra_simps)
ultimately show ?thesis
using ‹v ∈ C› ‹ξ ∈ C› by blast
next
case 2
moreover have "ξ ∈ {x. b > a ∙ x}"
using "2" ‹0 < ε› ‹a ∙ u = b› divide_less_cancel
by (fastforce simp: ξ_def algebra_simps)
ultimately show ?thesis
using ‹v ∈ C› ‹ξ ∈ C› by blast
qed
qed
have "r = (∑C∈{{x. a ∙ x = b} ∩ C, {x. b < a ∙ x} ∩ C, {x. a ∙ x < b} ∩ C}.
(- 1) ^ nat (aff_dim C))"
unfolding r_def
proof (intro sum.cong [OF _ refl] equalityI)
show "{{x. a ∙ x = b} ∩ C, {x. b < a ∙ x} ∩ C, {x. a ∙ x < b} ∩ C}
⊆ {C' ∩ C |C'. hyperplane_cell {(a, b)} C' ∧ C' ∩ C ≠ {}}"
apply clarsimp
using Cab Int_commute ‹C ∩ {x. a ∙ x = b} ≠ {}› hyperplane_cell_singleton ‹a ≠ 0›
by metis
qed (auto simp: ‹a ≠ 0› hyperplane_cell_singleton)
also have "… = (-1) ^ nat (aff_dim (C ∩ {x. a ∙ x = b}))
+ (-1) ^ nat (aff_dim (C ∩ {x. b < a ∙ x}))
+ (-1) ^ nat (aff_dim (C ∩ {x. a ∙ x < b}))"
using hyperplane_cells_distinct_lemma [of a b] Cab
by (auto simp: sum.insert_if Int_commute Int_left_commute)
also have "… = (- 1) ^ nat (aff_dim C)"
proof -
have *: "aff_dim (C ∩ {x. a ∙ x < b}) = aff_dim C ∧ aff_dim (C ∩ {x. a ∙ x > b}) = aff_dim C"
by (metis Cab open_halfspace_lt open_halfspace_gt aff_dim_affine_hull
affine_hull_convex_Int_open[OF ‹convex C›])
obtain S T where "open S" "affine T" and Ceq: "C = S ∩ T"
by (meson ‹hyperplane_cell A C› ‹finite A› hyperplane_cell_Int_open_affine)
have "affine hull C = affine hull T"
by (metis Ceq ‹C ≠ {}› ‹affine T› ‹open S› affine_hull_affine_Int_open inf_commute)
moreover
have "T ∩ ({x. a ∙ x = b} ∩ S) ≠ {}"
using Ceq ‹C ∩ {x. a ∙ x = b} ≠ {}› by blast
then have "affine hull (C ∩ {x. a ∙ x = b}) = affine hull (T ∩ {x. a ∙ x = b})"
using affine_hull_affine_Int_open[of "T ∩ {x. a ∙ x = b}" S]
by (simp add: Ceq Int_ac ‹affine T› ‹open S› affine_Int affine_hyperplane)
ultimately have "aff_dim (affine hull C) = aff_dim(affine hull (C ∩ {x. a ∙ x = b})) + 1"
using CInt_ne False Ceq
by (auto simp: aff_dim_affine_Int_hyperplane ‹affine T›)
moreover have "0 ≤ aff_dim (C ∩ {x. a ∙ x = b})"
by (metis CInt_ne aff_dim_negative_iff linorder_not_le)
ultimately show ?thesis
by (simp add: * nat_add_distrib)
qed
finally show ?thesis .
qed
qed
finally show "Euler_characteristic (insert (a, b) A) C = (-1) ^ nat(aff_dim C)" .
qed
then show "Euler_characteristic (insert (a, b) A) C = (Euler_characteristic A C)"
by (simp add: Euler_characteristic_cell 𝒞 ‹C ∈ 𝒞›)
qed
ultimately show ?thesis
by (simp add: Euler_characteristic_cellcomplex_Union ‹S = ⋃ 𝒞› ‹disjoint 𝒞› ‹h = (a, b)› assms(1))
qed
lemma Euler_characterstic_invariant_aux:
assumes "finite B" "finite A" "hyperplane_cellcomplex A S"
shows "Euler_characteristic (A ∪ B) S = Euler_characteristic A S"
using assms
by (induction rule: finite_induct) (auto simp: Euler_characterstic_lemma hyperplane_cellcomplex_mono)
lemma Euler_characterstic_invariant:
assumes "finite A" "finite B" "hyperplane_cellcomplex A S" "hyperplane_cellcomplex B S"
shows "Euler_characteristic A S = Euler_characteristic B S"
by (metis Euler_characterstic_invariant_aux assms sup_commute)
lemma Euler_characteristic_inclusion_exclusion:
assumes "finite A" "finite 𝒮" "⋀K. K ∈ 𝒮 ⟹ hyperplane_cellcomplex A K"
shows "Euler_characteristic A (⋃ 𝒮) = (∑𝒯 | 𝒯 ⊆ 𝒮 ∧ 𝒯 ≠ {}. (- 1) ^ (card 𝒯 + 1) * Euler_characteristic A (⋂𝒯))"
proof -
interpret Incl_Excl "hyperplane_cellcomplex A" "Euler_characteristic A"
proof
show "Euler_characteristic A (S ∪ T) = Euler_characteristic A S + Euler_characteristic A T"
if "hyperplane_cellcomplex A S" and "hyperplane_cellcomplex A T" and "disjnt S T" for S T
using that Euler_characteristic_cellcomplex_Un assms(1) by blast
qed (use hyperplane_cellcomplex_Int hyperplane_cellcomplex_Un hyperplane_cellcomplex_diff in auto)
show ?thesis
using restricted assms by blast
qed
subsection ‹Euler-type relation for full-dimensional proper polyhedral cones›
lemma Euler_polyhedral_cone:
fixes S :: "'n::euclidean_space set"
assumes "polyhedron S" "conic S" and intS: "interior S ≠ {}" and "S ≠ UNIV"
shows "(∑d = 0..DIM('n). (- 1) ^ d * int (card {f. f face_of S ∧ aff_dim f = int d})) = 0" (is "?lhs = 0")
proof -
have [simp]: "affine hull S = UNIV"
by (simp add: affine_hull_nonempty_interior intS)
with ‹polyhedron S›
obtain H where "finite H"
and Seq: "S = ⋂H"
and Hex: "⋀h. h∈H ⟹ ∃a b. a≠0 ∧ h = {x. a ∙ x ≤ b}"
and Hsub: "⋀𝒢. 𝒢 ⊂ H ⟹ S ⊂ ⋂𝒢"
by (fastforce simp: polyhedron_Int_affine_minimal)
have "0 ∈ S"
using assms(2) conic_contains_0 intS interior_empty by blast
have *: "∃a. a≠0 ∧ h = {x. a ∙ x ≤ 0}" if "h ∈ H" for h
proof -
obtain a b where "a≠0" and ab: "h = {x. a ∙ x ≤ b}"
using Hex [OF ‹h ∈ H›] by blast
have "0 ∈ ⋂H"
using Seq ‹0 ∈ S› by force
then have "0 ∈ h"
using that by blast
consider "b=0" | "b < 0" | "b > 0"
by linarith
then
show ?thesis
proof cases
case 1
then show ?thesis
using ‹a ≠ 0› ab by blast
next
case 2
then show ?thesis
using ‹0 ∈ h› ab by auto
next
case 3
have "S ⊂ ⋂(H - {h})"
using Hsub [of "H - {h}"] that by auto
then obtain x where x: "x ∈ ⋂(H - {h})" and "x ∉ S"
by auto
define ε where "ε ≡ min (1/2) (b / (a ∙ x))"
have "b < a ∙ x"
using ‹x ∉ S› ab x by (fastforce simp: ‹S = ⋂H›)
with 3 have "0 < a ∙ x"
by auto
with 3 have "0 < ε"
by (simp add: ε_def)
have "ε < 1"
using ε_def by linarith
have "ε * (a ∙ x) ≤ b"
unfolding ε_def using ‹0 < a ∙ x› pos_le_divide_eq by fastforce
have "x = inverse ε *⇩R ε *⇩R x"
using ‹0 < ε› by force
moreover
have "ε *⇩R x ∈ S"
proof -
have "ε *⇩R x ∈ h"
by (simp add: ‹ε * (a ∙ x) ≤ b› ab)
moreover have "ε *⇩R x ∈ ⋂(H - {h})"
proof -
have "ε *⇩R x ∈ k" if "x ∈ k" "k ∈ H" "k ≠ h" for k
proof -
obtain a' b' where "a'≠0" "k = {x. a' ∙ x ≤ b'}"
using Hex ‹k ∈ H› by blast
have "(0 ≤ a' ∙ x ⟹ a' ∙ ε *⇩R x ≤ a' ∙ x)"
by (metis ‹ε < 1› inner_scaleR_right order_less_le pth_1 real_scaleR_def scaleR_right_mono)
moreover have "(0 ≤ -(a' ∙ x) ⟹ 0 ≤ -(a' ∙ ε *⇩R x)) "
using ‹0 < ε› mult_le_0_iff order_less_imp_le by auto
ultimately
have "a' ∙ x ≤ b' ⟹ a' ∙ ε *⇩R x ≤ b'"
by (smt (verit) InterD ‹0 ∈ ⋂H› ‹k = {x. a' ∙ x ≤ b'}› inner_zero_right mem_Collect_eq that(2))
then show ?thesis
using ‹k = {x. a' ∙ x ≤ b'}› ‹x ∈ k› by fastforce
qed
with x show ?thesis
by blast
qed
ultimately show ?thesis
using Seq by blast
qed
with ‹conic S› have "inverse ε *⇩R ε *⇩R x ∈ S"
by (meson ‹0 < ε› conic_def inverse_nonnegative_iff_nonnegative order_less_le)
ultimately show ?thesis
using ‹x ∉ S› by presburger
qed
qed
then obtain fa where fa: "⋀h. h ∈ H ⟹ fa h ≠ 0 ∧ h = {x. fa h ∙ x ≤ 0}"
by metis
define fa_le_0 where "fa_le_0 ≡ λh. {x. fa h ∙ x ≤ 0}"
have fa': "⋀h. h ∈ H ⟹ fa_le_0 h = h"
using fa fa_le_0_def by blast
define A where "A ≡ (λh. (fa h,0::real)) ` H"
have "finite A"
using ‹finite H› by (simp add: A_def)
then have "?lhs = Euler_characteristic A S"
proof -
have [simp]: "card {f. f face_of S ∧ aff_dim f = int d} = card {C. hyperplane_cell A C ∧ C ⊆ S ∧ aff_dim C = int d}"
if "finite A" and "d ≤ card (Basis::'n set)"
for d :: nat
proof (rule bij_betw_same_card)
have hyper1: "hyperplane_cell A (rel_interior f) ∧ rel_interior f ⊆ S
∧ aff_dim (rel_interior f) = d ∧ closure (rel_interior f) = f"
if "f face_of S" "aff_dim f = d" for f
proof -
have 1: "closure(rel_interior f) = f"
proof -
have "closure(rel_interior f) = closure f"
by (meson convex_closure_rel_interior face_of_imp_convex that(1))
also have "… = f"
by (meson assms(1) closure_closed face_of_polyhedron_polyhedron polyhedron_imp_closed that(1))
finally show ?thesis .
qed
then have 2: "aff_dim (rel_interior f) = d"
by (metis closure_aff_dim that(2))
have "f ≠ {}"
using aff_dim_negative_iff [of f] by (simp add: that(2))
obtain J0 where "J0 ⊆ H" and J0: "f = ⋂ (fa_le_0 ` H) ∩ (⋂h ∈ J0. {x. fa h ∙ x = 0})"
proof (cases "f = S")
case True
have "S = ⋂ (fa_le_0 ` H)"
using Seq fa by (auto simp: fa_le_0_def)
then show ?thesis
using True that by blast
next
case False
have fexp: "f = ⋂{S ∩ {x. fa h ∙ x = 0} | h. h ∈ H ∧ f ⊆ S ∩ {x. fa h ∙ x = 0}}"
proof (rule face_of_polyhedron_explicit)
show "S = affine hull S ∩ ⋂ H"
by (simp add: Seq hull_subset inf.absorb2)
qed (auto simp: False ‹f ≠ {}› ‹f face_of S› ‹finite H› Hsub fa)
show ?thesis
proof
have *: "⋀x h. ⟦x ∈ f; h ∈ H⟧ ⟹ fa h ∙ x ≤ 0"
using Seq fa face_of_imp_subset ‹f face_of S› by fastforce
show "f = ⋂ (fa_le_0 ` H) ∩ (⋂h ∈ {h ∈ H. f ⊆ S ∩ {x. fa h ∙ x = 0}}. {x. fa h ∙ x = 0})"
(is "f = ?I")
proof
show "f ⊆ ?I"
using ‹f face_of S› fa face_of_imp_subset by (force simp: * fa_le_0_def)
show "?I ⊆ f"
apply (subst (2) fexp)
apply (clarsimp simp: * fa_le_0_def)
by (metis Inter_iff Seq fa mem_Collect_eq)
qed
qed blast
qed
define H' where "H' = (λh. {x. -(fa h) ∙ x ≤ 0}) ` H"
have "∃J. finite J ∧ J ⊆ H ∪ H' ∧ f = affine hull f ∩ ⋂J"
proof (intro exI conjI)
let ?J = "H ∪ image (λh. {x. -(fa h) ∙ x ≤ 0}) J0"
show "finite (?J::'n set set)"
using ‹J0 ⊆ H› ‹finite H› finite_subset by fastforce
show "?J ⊆ H ∪ H'"
using ‹J0 ⊆ H› by (auto simp: H'_def)
have "f = ⋂?J"
proof
show "f ⊆ ⋂?J"
unfolding J0 by (auto simp: fa')
have "⋀x j. ⟦j ∈ J0; ∀h∈H. x ∈ h; ∀j∈J0. 0 ≤ fa j ∙ x⟧ ⟹ fa j ∙ x = 0"
by (metis ‹J0 ⊆ H› fa in_mono inf.absorb2 inf.orderE mem_Collect_eq)
then show "⋂?J ⊆ f"
unfolding J0 by (auto simp: fa')
qed
then show "f = affine hull f ∩ ⋂?J"
by (simp add: Int_absorb1 hull_subset)
qed
then have **: "∃n J. finite J ∧ card J = n ∧ J ⊆ H ∪ H' ∧ f = affine hull f ∩ ⋂J"
by blast
obtain J nJ where J: "finite J" "card J = nJ" "J ⊆ H ∪ H'" and feq: "f = affine hull f ∩ ⋂J"
and minJ: "⋀m J'. ⟦finite J'; m < nJ; card J' = m; J' ⊆ H ∪ H'⟧ ⟹ f ≠ affine hull f ∩ ⋂J'"
using exists_least_iff [THEN iffD1, OF **] by metis
have FF: "f ⊂ (affine hull f ∩ ⋂J')" if "J' ⊂ J" for J'
proof -
have "f ≠ affine hull f ∩ ⋂J'"
using minJ
by (metis J finite_subset psubset_card_mono psubset_imp_subset psubset_subset_trans that)
then show ?thesis
by (metis Int_subset_iff Inter_Un_distrib feq hull_subset inf_sup_ord(2) psubsetI sup.absorb4 that)
qed
have "∃a. {x. a ∙ x ≤ 0} = h ∧ (h ∈ H ∧ a = fa h ∨ (∃h'. h' ∈ H ∧ a = -(fa h')))"
if "h ∈ J" for h
proof -
have "h ∈ H ∪ H'"
using ‹J ⊆ H ∪ H'› that by blast
then show ?thesis
proof
show ?thesis if "h ∈ H"
using that fa by blast
next
assume "h ∈ H'"
then obtain h' where "h' ∈ H" "h = {x. 0 ≤ fa h' ∙ x}"
by (auto simp: H'_def)
then show ?thesis
by (force simp: intro!: exI[where x="- (fa h')"])
qed
qed
then obtain ga
where ga_h: "⋀h. h ∈ J ⟹ h = {x. ga h ∙ x ≤ 0}"
and ga_fa: "⋀h. h ∈ J ⟹ h ∈ H ∧ ga h = fa h ∨ (∃h'. h' ∈ H ∧ ga h = -(fa h'))"
by metis
have 3: "hyperplane_cell A (rel_interior f)"
proof -
have D: "rel_interior f = {x ∈ f. ∀h∈J. ga h ∙ x < 0}"
proof (rule rel_interior_polyhedron_explicit [OF ‹finite J› feq])
show "ga h ≠ 0 ∧ h = {x. ga h ∙ x ≤ 0}" if "h ∈ J" for h
using that fa ga_fa ga_h by force
qed (auto simp: FF)
have H: "h ∈ H ∧ ga h = fa h" if "h ∈ J" for h
proof -
obtain z where z: "z ∈ rel_interior f"
using "1" ‹f ≠ {}› by force
then have "z ∈ f ∧ z ∈ S"
using D ‹f face_of S› face_of_imp_subset by blast
then show ?thesis
using ga_fa [OF that]
by (smt (verit, del_insts) D InterE Seq fa inner_minus_left mem_Collect_eq that z)
qed
then obtain K where "K ⊆ H"
and K: "f = ⋂ (fa_le_0 ` H) ∩ (⋂h ∈ K. {x. fa h ∙ x = 0})"
using J0 ‹J0 ⊆ H› by blast
have E: "rel_interior f = {x. (∀h ∈ H. fa h ∙ x ≤ 0) ∧ (∀h ∈ K. fa h ∙ x = 0) ∧ (∀h ∈ J. ga h ∙ x < 0)}"
unfolding D by (simp add: K fa_le_0_def)
have relif: "rel_interior f ≠ {}"
using "1" ‹f ≠ {}› by force
with E have "disjnt J K"
using H disjnt_iff by fastforce
define IFJK where "IFJK ≡ λh. if h ∈ J then {x. fa h ∙ x < 0}
else if h ∈ K then {x. fa h ∙ x = 0}
else if rel_interior f ⊆ {x. fa h ∙ x = 0}
then {x. fa h ∙ x = 0}
else {x. fa h ∙ x < 0}"
have relint_f: "rel_interior f = ⋂(IFJK ` H)"
proof
have A: False
if x: "x ∈ rel_interior f" and y: "y ∈ rel_interior f" and less0: "fa h ∙ y < 0"
and fa0: "fa h ∙ x = 0" and "h ∈ H" "h ∉ J" "h ∉ K" for x h y
proof -
obtain ε where "x ∈ f" "ε>0"
and ε: "⋀t. ⟦dist x t ≤ ε; t ∈ affine hull f⟧ ⟹ t ∈ f"
using x by (force simp: mem_rel_interior_cball)
then have "y ≠ x"
using fa0 less0 by force
define x' where "x' ≡ x + (ε / norm(y - x)) *⇩R (x - y)"
have "x ∈ affine hull f ∧ y ∈ affine hull f"
by (metis ‹x ∈ f› hull_inc mem_rel_interior_cball y)
moreover have "dist x x' ≤ ε"
using ‹0 < ε› ‹y ≠ x› by (simp add: x'_def divide_simps dist_norm norm_minus_commute)
ultimately have "x' ∈ f"
by (simp add: ε mem_affine_3_minus x'_def)
have "x' ∈ S"
using ‹f face_of S› ‹x' ∈ f› face_of_imp_subset by auto
then have "x' ∈ h"
using Seq that(5) by blast
then have "x' ∈ {x. fa h ∙ x ≤ 0}"
using fa that(5) by blast
moreover have "ε / norm (y - x) * -(fa h ∙ y) > 0"
using ‹0 < ε› ‹y ≠ x› less0 by (simp add: field_split_simps)
ultimately show ?thesis
by (simp add: x'_def fa0 inner_diff_right inner_right_distrib)
qed
show "rel_interior f ⊆ ⋂(IFJK ` H)"
unfolding IFJK_def by (smt (verit, ccfv_SIG) A E H INT_I in_mono mem_Collect_eq subsetI)
show "⋂(IFJK ` H) ⊆ rel_interior f"
using ‹K ⊆ H› ‹disjnt J K›
apply (clarsimp simp add: ball_Un E H disjnt_iff IFJK_def)
apply (smt (verit, del_insts) IntI Int_Collect subsetD)
done
qed
obtain z where zrelf: "z ∈ rel_interior f"
using relif by blast
moreover
have H: "z ∈ IFJK h ⟹ (x ∈ IFJK h) = (hyperplane_side (fa h, 0) z = hyperplane_side (fa h, 0) x)" for h x
using zrelf by (auto simp: IFJK_def hyperplane_side_def sgn_if split: if_split_asm)
then have "z ∈ ⋂(IFJK ` H) ⟹ (x ∈ ⋂(IFJK ` H)) = hyperplane_equiv A z x" for x
unfolding A_def Inter_iff hyperplane_equiv_def ball_simps using H by blast
then have "x ∈ rel_interior f ⟷ hyperplane_equiv A z x" for x
using relint_f zrelf by presburger
ultimately show ?thesis
by (metis equalityI hyperplane_cell mem_Collect_eq subset_iff)
qed
have 4: "rel_interior f ⊆ S"
by (meson face_of_imp_subset order_trans rel_interior_subset that(1))
show ?thesis
using "1" "2" "3" "4" by blast
qed
have hyper2: "(closure c face_of S ∧ aff_dim (closure c) = d) ∧ rel_interior (closure c) = c"
if c: "hyperplane_cell A c" and "c ⊆ S" "aff_dim c = d" for c
proof (intro conjI)
obtain J where "J ⊆ H" and J: "c = (⋂h ∈ J. {x. (fa h) ∙ x < 0}) ∩ (⋂h ∈ (H - J). {x. (fa h) ∙ x = 0})"
proof -
obtain z where z: "c = {y. ∀x ∈ H. sgn (fa x ∙ y) = sgn (fa x ∙ z)}"
using c by (force simp: hyperplane_cell A_def hyperplane_equiv_def hyperplane_side_def)
show thesis
proof
let ?J = "{h ∈ H. sgn(fa h ∙ z) = -1}"
have 1: "fa h ∙ x < 0"
if "∀h∈H. sgn (fa h ∙ x) = sgn (fa h ∙ z)" and "h ∈ H" and "sgn (fa h ∙ z) = - 1" for x h
using that by (metis sgn_1_neg)
have 2: "sgn (fa h ∙ z) = - 1"
if "∀h∈H. sgn (fa h ∙ x) = sgn (fa h ∙ z)" and "h ∈ H" and "fa h ∙ x ≠ 0" for x h
proof -
have "⟦0 < fa h ∙ x; 0 < fa h ∙ z⟧ ⟹ False"
using that fa by (smt (verit, del_insts) Inter_iff Seq ‹c ⊆ S› mem_Collect_eq subset_iff z)
then show ?thesis
by (metis that sgn_if sgn_zero_iff)
qed
have 3: "sgn (fa h ∙ x) = sgn (fa h ∙ z)"
if "h ∈ H" and "∀h. h ∈ H ∧ sgn (fa h ∙ z) = - 1 ⟶ fa h ∙ x < 0"
and "∀h∈H - {h ∈ H. sgn (fa h ∙ z) = - 1}. fa h ∙ x = 0"
for x h
using that 2 by (metis (mono_tags, lifting) Diff_iff mem_Collect_eq sgn_neg)
show "c = (⋂h ∈?J. {x. fa h ∙ x < 0}) ∩ (⋂h∈H - ?J. {x. fa h ∙ x = 0})"
unfolding z by (auto intro: 1 2 3)
qed auto
qed
have "finite J"
using ‹J ⊆ H› ‹finite H› finite_subset by blast
show "closure c face_of S"
proof -
have cc: "closure c = closure (⋂h∈J. {x. fa h ∙ x < 0}) ∩ closure (⋂h∈H - J. {x. fa h ∙ x = 0})"
unfolding J
proof (rule closure_Int_convex)
show "convex (⋂h∈J. {x. fa h ∙ x < 0})"
by (simp add: convex_INT convex_halfspace_lt)
show "convex (⋂h∈H - J. {x. fa h ∙ x = 0})"
by (simp add: convex_INT convex_hyperplane)
have o1: "open (⋂h∈J. {x. fa h ∙ x < 0})"
by (metis open_INT[OF ‹finite J›] open_halfspace_lt)
have o2: "openin (top_of_set (affine hull (⋂h∈H - J. {x. fa h ∙ x = 0}))) (⋂h∈H - J. {x. fa h ∙ x = 0})"
proof -
have "affine (⋂h∈H - J. {n. fa h ∙ n = 0})"
using affine_hyperplane by auto
then show ?thesis
by (metis (no_types) affine_hull_eq openin_subtopology_self)
qed
show "rel_interior (⋂h∈J. {x. fa h ∙ x < 0}) ∩ rel_interior (⋂h∈H - J. {x. fa h ∙ x = 0}) ≠ {}"
by (metis nonempty_hyperplane_cell c rel_interior_open o1 rel_interior_openin o2 J)
qed
have clo_im_J: "closure ` ((λh. {x. fa h ∙ x < 0}) ` J) = (λh. {x. fa h ∙ x ≤ 0}) ` J"
using ‹J ⊆ H› by (force simp: image_comp fa)
have cleq: "closure (⋂h∈H - J. {x. fa h ∙ x = 0}) = (⋂h∈H - J. {x. fa h ∙ x = 0})"
by (intro closure_closed) (blast intro: closed_hyperplane)
have **: "(⋂h∈J. {x. fa h ∙ x ≤ 0}) ∩ (⋂h∈H - J. {x. fa h ∙ x = 0}) face_of S"
if "(⋂h∈J. {x. fa h ∙ x < 0}) ≠ {}"
proof (cases "J=H")
case True
have [simp]: "(⋂x∈H. {xa. fa x ∙ xa ≤ 0}) = ⋂H"
using fa by auto
show ?thesis
using ‹polyhedron S› by (simp add: Seq True polyhedron_imp_convex face_of_refl)
next
case False
have **: "(⋂h∈J. {n. fa h ∙ n ≤ 0}) ∩ (⋂h∈H - J. {x. fa h ∙ x = 0}) =
(⋂h∈H - J. S ∩ {x. fa h ∙ x = 0})" (is "?L = ?R")
proof
show "?L ⊆ ?R"
by clarsimp (smt (verit) DiffI InterI Seq fa mem_Collect_eq)
show "?R ⊆ ?L"
using False Seq ‹J ⊆ H› fa by blast
qed
show ?thesis
unfolding **
proof (rule face_of_Inter)
show "(λh. S ∩ {x. fa h ∙ x = 0}) ` (H - J) ≠ {}"
using False ‹J ⊆ H› by blast
show "T face_of S"
if T: "T ∈ (λh. S ∩ {x. fa h ∙ x = 0}) ` (H - J)" for T
proof -
obtain h where h: "T = S ∩ {x. fa h ∙ x = 0}" and "h ∈ H" "h ∉ J"
using T by auto
have "S ∩ {x. fa h ∙ x = 0} face_of S"
proof (rule face_of_Int_supporting_hyperplane_le)
show "convex S"
by (simp add: assms(1) polyhedron_imp_convex)
show "fa h ∙ x ≤ 0" if "x ∈ S" for x
using that Seq fa ‹h ∈ H› by auto
qed
then show ?thesis
using h by blast
qed
qed
qed
have *: "⋀S. S ∈ (λh. {x. fa h ∙ x < 0}) ` J ⟹ convex S ∧ open S"
using convex_halfspace_lt open_halfspace_lt by fastforce
show ?thesis
unfolding cc
apply (simp add: * closure_Inter_convex_open)
by (metis "**" cleq clo_im_J image_image)
qed
show "aff_dim (closure c) = int d"
by (simp add: that)
show "rel_interior (closure c) = c"
by (metis ‹finite A› c convex_rel_interior_closure hyperplane_cell_convex hyperplane_cell_relative_interior)
qed
have "rel_interior ` {f. f face_of S ∧ aff_dim f = int d}
= {C. hyperplane_cell A C ∧ C ⊆ S ∧ aff_dim C = int d}"
using hyper1 hyper2 by fastforce
then show "bij_betw (rel_interior) {f. f face_of S ∧ aff_dim f = int d} {C. hyperplane_cell A C ∧ C ⊆ S ∧ aff_dim C = int d}"
unfolding bij_betw_def inj_on_def by (metis (mono_tags) hyper1 mem_Collect_eq)
qed
show ?thesis
by (simp add: Euler_characteristic ‹finite A›)
qed
also have "… = 0"
proof -
have A: "hyperplane_cellcomplex A (- h)" if "h ∈ H" for h
proof (rule hyperplane_cellcomplex_mono [OF hyperplane_cell_cellcomplex])
have "- h = {x. fa h ∙ x = 0} ∨ - h = {x. fa h ∙ x < 0} ∨ - h = {x. 0 < fa h ∙ x}"
by (smt (verit, ccfv_SIG) Collect_cong Collect_neg_eq fa that)
then show "hyperplane_cell {(fa h,0)} (- h)"
by (simp add: hyperplane_cell_singleton fa that)
show "{(fa h,0)} ⊆ A"
by (simp add: A_def that)
qed
then have "⋀h. h ∈ H ⟹ hyperplane_cellcomplex A h"
using hyperplane_cellcomplex_Compl by fastforce
then have "hyperplane_cellcomplex A S"
by (simp add: Seq hyperplane_cellcomplex_Inter)
then have D: "Euler_characteristic A (UNIV::'n set) =
Euler_characteristic A (⋂H) + Euler_characteristic A (- ⋂H)"
using Euler_characteristic_cellcomplex_Un
by (metis Compl_partition Diff_cancel Diff_eq Seq ‹finite A› disjnt_def hyperplane_cellcomplex_Compl)
have "Euler_characteristic A UNIV = Euler_characteristic {} (UNIV::'n set)"
by (simp add: Euler_characterstic_invariant ‹finite A›)
then have E: "Euler_characteristic A UNIV = (-1) ^ (DIM('n))"
by (simp add: Euler_characteristic_cell)
have DD: "Euler_characteristic A (⋂ (uminus ` J)) = (- 1) ^ DIM('n)"
if "J ≠ {}" "J ⊆ H" for J
proof -
define B where "B ≡ (λh. (fa h,0::real)) ` J"
then have "B ⊆ A"
by (simp add: A_def image_mono that)
have "∃x. y = -x" if "y ∈ ⋂ (uminus ` H)" for y::'n
by (metis add.inverse_inverse)
moreover have "-x ∈ ⋂ (uminus ` H) ⟷ x ∈ interior S" for x
proof -
have 1: "interior S = {x ∈ S. ∀h∈H. fa h ∙ x < 0}"
using rel_interior_polyhedron_explicit [OF ‹finite H› _ fa]
by (metis (no_types, lifting) inf_top_left Hsub Seq ‹affine hull S = UNIV› rel_interior_interior)
have 2: "⋀x y. ⟦y ∈ H; ∀h∈H. fa h ∙ x < 0; - x ∈ y⟧ ⟹ False"
by (smt (verit, best) fa inner_minus_right mem_Collect_eq)
show ?thesis
apply (simp add: 1)
by (smt (verit) 2 * fa Inter_iff Seq inner_minus_right mem_Collect_eq)
qed
ultimately have INT_Compl_H: "⋂ (uminus ` H) = uminus ` interior S"
by blast
obtain z where z: "z ∈ ⋂ (uminus ` J)"
using ‹J ⊆ H› ‹⋂ (uminus ` H) = uminus ` interior S› intS by fastforce
have "⋂ (uminus ` J) = Collect (hyperplane_equiv B z)" (is "?L = ?R")
proof
show "?L ⊆ ?R"
using fa ‹J ⊆ H› z
by (fastforce simp: hyperplane_equiv_def hyperplane_side_def B_def set_eq_iff )
show "?R ⊆ ?L"
using z ‹J ⊆ H› apply (clarsimp simp add: hyperplane_equiv_def hyperplane_side_def B_def)
by (metis fa in_mono mem_Collect_eq sgn_le_0_iff)
qed
then have hyper_B: "hyperplane_cell B (⋂ (uminus ` J))"
by (metis hyperplane_cell)
have "Euler_characteristic A (⋂ (uminus ` J)) = Euler_characteristic B (⋂ (uminus ` J))"
proof (rule Euler_characterstic_invariant [OF ‹finite A›])
show "finite B"
using ‹B ⊆ A› ‹finite A› finite_subset by blast
show "hyperplane_cellcomplex A (⋂ (uminus ` J))"
by (meson ‹B ⊆ A› hyper_B hyperplane_cell_cellcomplex hyperplane_cellcomplex_mono)
show "hyperplane_cellcomplex B (⋂ (uminus ` J))"
by (simp add: hyper_B hyperplane_cell_cellcomplex)
qed
also have "… = (- 1) ^ nat (aff_dim (⋂ (uminus ` J)))"
using Euler_characteristic_cell hyper_B by blast
also have "… = (- 1) ^ DIM('n)"
proof -
have "affine hull ⋂ (uminus ` H) = UNIV"
by (simp add: INT_Compl_H affine_hull_nonempty_interior intS interior_negations)
then have "affine hull ⋂ (uminus ` J) = UNIV"
by (metis Inf_superset_mono hull_mono subset_UNIV subset_antisym subset_image_iff that(2))
with aff_dim_eq_full show ?thesis
by (metis nat_int)
qed
finally show ?thesis .
qed
have EE: "(∑𝒯 | 𝒯 ⊆ uminus ` H ∧ 𝒯≠{}. (-1) ^ (card 𝒯 + 1) * Euler_characteristic A (⋂𝒯))
= (∑𝒯 | 𝒯 ⊆ uminus ` H ∧ 𝒯 ≠ {}. (-1) ^ (card 𝒯 + 1) * (- 1) ^ DIM('n))"
by (intro sum.cong [OF refl]) (fastforce simp: subset_image_iff intro!: DD)
also have "… = (-1) ^ DIM('n)"
proof -
have A: "(∑y = 1..card H. ∑t∈{x ∈ {𝒯. 𝒯 ⊆ uminus ` H ∧ 𝒯 ≠ {}}. card x = y}. (- 1) ^ (card t + 1))
= (∑𝒯∈{𝒯. 𝒯 ⊆ uminus ` H ∧ 𝒯 ≠ {}}. (- 1) ^ (card 𝒯 + 1))"
proof (rule sum.group)
have "⋀C. ⟦C ⊆ uminus ` H; C ≠ {}⟧ ⟹ Suc 0 ≤ card C ∧ card C ≤ card H"
by (meson ‹finite H› card_eq_0_iff finite_surj le_zero_eq not_less_eq_eq surj_card_le)
then show "card ` {𝒯. 𝒯 ⊆ uminus ` H ∧ 𝒯 ≠ {}} ⊆ {1..card H}"
by force
qed (auto simp: ‹finite H›)
have "(∑n = Suc 0..card H. - (int (card {x. x ⊆ uminus ` H ∧ x ≠ {} ∧ card x = n}) * (- 1) ^ n))
= (∑n = Suc 0..card H. (-1) ^ (Suc n) * (card H choose n))"
proof (rule sum.cong [OF refl])
fix n
assume "n ∈ {Suc 0..card H}"
then have "{𝒯. 𝒯 ⊆ uminus ` H ∧ 𝒯 ≠ {} ∧ card 𝒯 = n} = {𝒯. 𝒯 ⊆ uminus ` H ∧ card 𝒯 = n}"
by auto
then have "card{𝒯. 𝒯 ⊆ uminus ` H ∧ 𝒯 ≠ {} ∧ card 𝒯 = n} = card (uminus ` H) choose n"
by (simp add: ‹finite H› n_subsets)
also have "… = card H choose n"
by (metis card_image double_complement inj_on_inverseI)
finally
show "- (int (card {𝒯. 𝒯 ⊆ uminus ` H ∧ 𝒯 ≠ {} ∧ card 𝒯 = n}) * (- 1) ^ n) = (- 1) ^ Suc n * int (card H choose n)"
by simp
qed
also have "… = - (∑k = Suc 0..card H. (-1) ^ k * (card H choose k))"
by (simp add: sum_negf)
also have "… = 1 - (∑k=0..card H. (-1) ^ k * (card H choose k))"
using atLeastSucAtMost_greaterThanAtMost by (simp add: sum.head [of 0])
also have "… = 1 - 0 ^ card H"
using binomial_ring [of "-1" "1::int" "card H"] by (simp add: mult.commute atLeast0AtMost)
also have "… = 1"
using Seq ‹finite H› ‹S ≠ UNIV› card_0_eq by auto
finally have C: "(∑n = Suc 0..card H. - (int (card {x. x ⊆ uminus ` H ∧ x ≠ {} ∧ card x = n}) * (- 1) ^ n)) = (1::int)" .
have "(∑𝒯 | 𝒯 ⊆ uminus ` H ∧ 𝒯 ≠ {}. (- 1) ^ (card 𝒯 + 1)) = (1::int)"
unfolding A [symmetric] by (simp add: C)
then show ?thesis
by (simp flip: sum_distrib_right power_Suc)
qed
finally have "(∑𝒯 | 𝒯 ⊆ uminus ` H ∧ 𝒯≠{}. (-1) ^ (card 𝒯 + 1) * Euler_characteristic A (⋂𝒯))
= (-1) ^ DIM('n)" .
then have "Euler_characteristic A (⋃ (uminus ` H)) = (-1) ^ (DIM('n))"
using Euler_characteristic_inclusion_exclusion [OF ‹finite A›]
by (smt (verit) A Collect_cong ‹finite H› finite_imageI image_iff sum.cong)
then show ?thesis
using D E by (simp add: uminus_Inf Seq)
qed
finally show ?thesis .
qed
subsection ‹Euler-Poincare relation for special $(n-1)$-dimensional polytope›
lemma Euler_Poincare_lemma:
fixes p :: "'n::euclidean_space set"
assumes "DIM('n) ≥ 2" "polytope p" "i ∈ Basis" and affp: "affine hull p = {x. x ∙ i = 1}"
shows "(∑d = 0..DIM('n) - 1. (-1) ^ d * int (card {f. f face_of p ∧ aff_dim f = int d})) = 1"
proof -
have "aff_dim p = aff_dim {x. i ∙ x = 1}"
by (metis (no_types, lifting) Collect_cong aff_dim_affine_hull affp inner_commute)
also have "... = int (DIM('n) - 1)"
using aff_dim_hyperplane [of i 1] ‹i ∈ Basis› by fastforce
finally have AP: "aff_dim p = int (DIM('n) - 1)" .
show ?thesis
proof (cases "p = {}")
case True
with AP show ?thesis by simp
next
case False
define S where "S ≡ conic hull p"
have 1: "(conic hull f) ∩ {x. x ∙ i = 1} = f" if "f ⊆ {x. x ∙ i = 1}" for f
using that
by (smt (verit, ccfv_threshold) affp conic_hull_Int_affine_hull hull_hull inner_zero_left mem_Collect_eq)
obtain K where "finite K" and K: "p = convex hull K"
by (meson assms(2) polytope_def)
then have "convex_cone hull K = conic hull (convex hull K)"
using False convex_cone_hull_separate_nonempty by auto
then have "polyhedron S"
using polyhedron_convex_cone_hull
by (simp add: S_def ‹polytope p› polyhedron_conic_hull_polytope)
then have "convex S"
by (simp add: polyhedron_imp_convex)
then have "conic S"
by (simp add: S_def conic_conic_hull)
then have "0 ∈ S"
by (simp add: False S_def)
have "S ≠ UNIV"
proof
assume "S = UNIV"
then have "conic hull p ∩ {x. x∙i = 1} = p"
by (metis "1" affp hull_subset)
then have "bounded {x. x ∙ i = 1}"
using S_def ‹S = UNIV› assms(2) polytope_imp_bounded by auto
then obtain B where "B>0" and B: "⋀x. x ∈ {x. x ∙ i = 1} ⟹ norm x ≤ B"
using bounded_normE by blast
define x where "x ≡ (∑b∈Basis. (if b=i then 1 else B+1) *⇩R b)"
obtain j where j: "j ∈ Basis" "j≠i"
using ‹DIM('n) ≥ 2›
by (metis DIM_complex DIM_ge_Suc0 card_2_iff' card_le_Suc0_iff_eq euclidean_space_class.finite_Basis le_antisym)
have "B+1 ≤ ¦x ∙ j¦"
using j by (simp add: x_def)
also have "… ≤ norm x"
using Basis_le_norm j by blast
finally have "norm x > B"
by simp
moreover have "x ∙ i = 1"
by (simp add: x_def ‹i ∈ Basis›)
ultimately show False
using B by force
qed
have "S ≠ {}"
by (metis False S_def empty_subsetI equalityI hull_subset)
have "⋀c x. ⟦0 < c; x ∈ p; x ≠ 0⟧ ⟹ 0 < (c *⇩R x) ∙ i"
by (metis (mono_tags) Int_Collect Int_iff affp hull_inc inner_commute inner_scaleR_right mult.right_neutral)
then have doti_gt0: "0 < x ∙ i" if S: "x ∈ S" and "x ≠ 0" for x
using that by (auto simp: S_def conic_hull_explicit)
have "⋀a. {a} face_of S ⟹ a = 0"
using ‹conic S› conic_contains_0 face_of_conic by blast
moreover have "{0} face_of S"
proof -
have "⋀a b u. ⟦a ∈ S; b ∈ S; a ≠ b; u < 1; 0 < u; (1 - u) *⇩R a + u *⇩R b = 0⟧ ⟹ False"
using conic_def euclidean_all_zero_iff inner_left_distrib scaleR_eq_0_iff
by (smt (verit, del_insts) doti_gt0 ‹conic S› ‹i ∈ Basis›)
then show ?thesis
by (auto simp: in_segment face_of_singleton extreme_point_of_def ‹0 ∈ S›)
qed
ultimately have face_0: "{f. f face_of S ∧ (∃a. f = {a})} = {{0}}"
by auto
have "interior S ≠ {}"
proof
assume "interior S = {}"
then obtain a b where "a ≠ 0" and ab: "S ⊆ {x. a ∙ x = b}"
by (metis ‹convex S› empty_interior_subset_hyperplane)
have "{x. x ∙ i = 1} ⊆ {x. a ∙ x = b}"
by (metis S_def ab affine_hyperplane affp hull_inc subset_eq subset_hull)
moreover have "¬ {x. x ∙ i = 1} ⊂ {x. a ∙ x = b}"
using aff_dim_hyperplane [of a b]
by (metis AP ‹a ≠ 0› aff_dim_eq_full_gen affine_hyperplane affp hull_subset less_le_not_le subset_hull)
ultimately have "S ⊆ {x. x ∙ i = 1}"
using ab by auto
with ‹S ≠ {}› show False
using ‹conic S› conic_contains_0 by fastforce
qed
then have "(∑d = 0..DIM('n). (-1) ^ d * int (card {f. f face_of S ∧ aff_dim f = int d})) = 0"
using Euler_polyhedral_cone ‹S ≠ UNIV› ‹conic S› ‹polyhedron S› by blast
then have "1 + (∑d = 1..DIM('n). (-1) ^ d * (card {f. f face_of S ∧ aff_dim f = d})) = 0"
by (simp add: sum.atLeast_Suc_atMost aff_dim_eq_0 face_0)
moreover have "(∑d = 1..DIM('n). (-1) ^ d * (card {f. f face_of S ∧ aff_dim f = d}))
= - (∑d = 0..DIM('n) - 1. (-1) ^ d * int (card {f. f face_of p ∧ aff_dim f = int d}))"
proof -
have "(∑d = 1..DIM('n). (-1) ^ d * (card {f. f face_of S ∧ aff_dim f = d}))
= (∑d = Suc 0..Suc (DIM('n)-1). (-1) ^ d * (card {f. f face_of S ∧ aff_dim f = d}))"
by auto
also have "... = - (∑d = 0..DIM('n) - 1. (-1) ^ d * card {f. f face_of S ∧ aff_dim f = 1 + int d})"
unfolding sum.atLeast_Suc_atMost_Suc_shift by (simp add: sum_negf)
also have "... = - (∑d = 0..DIM('n) - 1. (-1) ^ d * card {f. f face_of p ∧ aff_dim f = int d})"
proof -
{ fix d
assume "d ≤ DIM('n) - Suc 0"
have conic_face_p: "(conic hull f) face_of S" if "f face_of p" for f
proof (cases "f={}")
case False
have "{c *⇩R x |c x. 0 ≤ c ∧ x ∈ f} ⊆ {c *⇩R x |c x. 0 ≤ c ∧ x ∈ p}"
using face_of_imp_subset that by blast
moreover
have "convex {c *⇩R x |c x. 0 ≤ c ∧ x ∈ f}"
by (metis (no_types) cone_hull_expl convex_cone_hull face_of_imp_convex that)
moreover
have "(∃c x. ca *⇩R a = c *⇩R x ∧ 0 ≤ c ∧ x ∈ f) ∧ (∃c x. cb *⇩R b = c *⇩R x ∧ 0 ≤ c ∧ x ∈ f)"
if "∀a∈p. ∀b∈p. (∃x∈f. x ∈ open_segment a b) ⟶ a ∈ f ∧ b ∈ f"
and "0 ≤ ca" "a ∈ p" "0 ≤ cb" "b ∈ p"
and "0 ≤ cx" "x ∈ f" and oseg: "cx *⇩R x ∈ open_segment (ca *⇩R a) (cb *⇩R b)"
for ca a cb b cx x
proof -
have ai: "a ∙ i = 1" and bi: "b ∙ i = 1"
using affp hull_inc that(3,5) by fastforce+
have xi: "x ∙ i = 1"
using affp that ‹f face_of p› face_of_imp_subset hull_subset by fastforce
show ?thesis
proof (cases "cx *⇩R x = 0")
case True
then show ?thesis
using ‹{0} face_of S› face_ofD ‹conic S› that
by (smt (verit, best) S_def conic_def hull_subset insertCI singletonD subsetD)
next
case False
then have "cx ≠ 0" "x ≠ 0"
by auto
obtain u where "0 < u" "u < 1" and u: "cx *⇩R x = (1 - u) *⇩R (ca *⇩R a) + u *⇩R (cb *⇩R b)"
using oseg in_segment(2) by metis
show ?thesis
proof (cases "x = a")
case True
then have ua: "(cx - (1 - u) * ca) *⇩R a = (u * cb) *⇩R b"
using u by (simp add: algebra_simps)
then have "(cx - (1 - u) * ca) * 1 = u * cb * 1"
by (metis ai bi inner_scaleR_left)
then have "a=b ∨ cb = 0"
using ua ‹0 < u› by force
then show ?thesis
by (metis True scaleR_zero_left that(2) that(4) that(7))
next
case False
show ?thesis
proof (cases "x = b")
case True
then have ub: "(cx - (u * cb)) *⇩R b = ((1 - u) * ca) *⇩R a"
using u by (simp add: algebra_simps)
then have "(cx - (u * cb)) * 1 = ((1 - u) * ca) * 1"
by (metis ai bi inner_scaleR_left)
then have "a=b ∨ ca = 0"
using ‹u < 1› ub by auto
then show ?thesis
using False True that(4) that(7) by auto
next
case False
have "cx > 0"
using ‹cx ≠ 0› ‹0 ≤ cx› by linarith
have False if "ca = 0"
proof -
have "cx = u * cb"
by (metis add_0 bi inner_real_def inner_scaleR_left real_inner_1_right scale_eq_0_iff that u xi)
then show False
using ‹x ≠ b› ‹cx ≠ 0› that u by force
qed
with ‹0 ≤ ca› have "ca > 0"
by force
have aff: "x ∈ affine hull p ∧ a ∈ affine hull p ∧ b ∈ affine hull p"
using affp xi ai bi by blast
show ?thesis
proof (cases "cb=0")
case True
have u': "cx *⇩R x = ((1 - u) * ca) *⇩R a"
using u by (simp add: True)
then have "cx = ((1 - u) * ca)"
by (metis ai inner_scaleR_left mult.right_neutral xi)
then show ?thesis
using True u' ‹cx ≠ 0› ‹ca ≥ 0› ‹x ∈ f› by auto
next
case False
with ‹cb ≥ 0› have "cb > 0"
by linarith
{ have False if "a=b"
proof -
have *: "cx *⇩R x = ((1 - u) * ca + u * cb) *⇩R b"
using u that by (simp add: algebra_simps)
then have "cx = ((1 - u) * ca + u * cb)"
by (metis xi bi inner_scaleR_left mult.right_neutral)
with ‹x ≠ b› ‹cx ≠ 0› * show False
by force
qed
}
moreover
have "cx *⇩R x /⇩R cx = (((1 - u) * ca) *⇩R a + (cb * u) *⇩R b) /⇩R cx"
using u by simp
then have xeq: "x = ((1-u) * ca / cx) *⇩R a + (cb * u / cx) *⇩R b"
by (simp add: ‹cx ≠ 0› divide_inverse_commute scaleR_right_distrib)
then have proj: "1 = ((1-u) * ca / cx) + (cb * u / cx)"
using ai bi xi by (simp add: inner_left_distrib)
then have eq: "cx + ca * u = ca + cb * u"
using ‹cx > 0› by (simp add: field_simps)
have "∃u>0. u < 1 ∧ x = (1 - u) *⇩R a + u *⇩R b"
proof (intro exI conjI)
show "0 < inverse cx * u * cb"
by (simp add: ‹0 < cb› ‹0 < cx› ‹0 < u›)
show "inverse cx * u * cb < 1"
using proj ‹0 < ca› ‹0 < cx› ‹u < 1› by (simp add: divide_simps)
show "x = (1 - inverse cx * u * cb) *⇩R a + (inverse cx * u * cb) *⇩R b"
using eq ‹cx ≠ 0› by (simp add: xeq field_simps)
qed
ultimately show ?thesis
using that by (metis in_segment(2))
qed
qed
qed
qed
qed
ultimately show ?thesis
using that by (auto simp: S_def conic_hull_explicit face_of_def)
qed auto
moreover
have conic_hyperplane_eq: "conic hull (f ∩ {x. x ∙ i = 1}) = f"
if "f face_of S" "0 < aff_dim f" for f
proof
show "conic hull (f ∩ {x. x ∙ i = 1}) ⊆ f"
by (metis ‹conic S› face_of_conic inf_le1 subset_hull that(1))
have "∃c x'. x = c *⇩R x' ∧ 0 ≤ c ∧ x' ∈ f ∧ x' ∙ i = 1" if "x ∈ f" for x
proof (cases "x=0")
case True
obtain y where "y ∈ f" "y ≠ 0"
by (metis ‹0 < aff_dim f› aff_dim_sing aff_dim_subset insertCI linorder_not_le subset_iff)
then have "y ∙ i > 0"
using ‹f face_of S› doti_gt0 face_of_imp_subset by blast
then have "y /⇩R (y ∙ i) ∈ f ∧ (y /⇩R (y ∙ i)) ∙ i = 1"
using ‹conic S› ‹f face_of S› ‹y ∈ f› conic_def face_of_conic by fastforce
then show ?thesis
using True by fastforce
next
case False
then have "x ∙ i > 0"
using ‹f face_of S› doti_gt0 face_of_imp_subset that by blast
then have "x /⇩R (x ∙ i) ∈ f ∧ (x /⇩R (x ∙ i)) ∙ i = 1"
using ‹conic S› ‹f face_of S› ‹x ∈ f› conic_def face_of_conic by fastforce
then show ?thesis
by (metis ‹0 < x ∙ i› divideR_right eucl_less_le_not_le)
qed
then show "f ⊆ conic hull (f ∩ {x. x ∙ i = 1})"
by (auto simp: conic_hull_explicit)
qed
have conic_face_S: "conic hull f face_of S"
if "f face_of S" for f
by (metis ‹conic S› face_of_conic hull_same that)
have aff_1d: "aff_dim (conic hull f) = aff_dim f + 1" (is "?lhs = ?rhs")
if "f face_of p" and "f ≠ {}" for f
proof (rule order_antisym)
have "?lhs ≤ aff_dim(affine hull (insert 0 (affine hull f)))"
proof (intro aff_dim_subset hull_minimal)
show "f ⊆ affine hull insert 0 (affine hull f)"
by (metis hull_insert hull_subset insert_subset)
show "conic (affine hull insert 0 (affine hull f))"
by (metis affine_hull_span_0 conic_span hull_inc insertI1)
qed
also have "… ≤ ?rhs"
by (simp add: aff_dim_insert)
finally show "?lhs ≤ ?rhs" .
have "aff_dim f < aff_dim (conic hull f)"
proof (intro aff_dim_psubset psubsetI)
show "affine hull f ⊆ affine hull (conic hull f)"
by (simp add: hull_mono hull_subset)
have "0 ∉ affine hull f"
using affp face_of_imp_subset hull_mono that(1) by fastforce
moreover have "0 ∈ affine hull (conic hull f)"
by (simp add: ‹f ≠ {}› hull_inc)
ultimately show "affine hull f ≠ affine hull (conic hull f)"
by auto
qed
then show "?rhs ≤ ?lhs"
by simp
qed
have face_S_imp_face_p: "⋀f. f face_of S ⟹ f ∩ {x. x ∙ i = 1} face_of p"
by (metis "1" S_def affp convex_affine_hull face_of_slice hull_subset)
have conic_eq_f: "conic hull f ∩ {x. x ∙ i = 1} = f"
if "f face_of p" for f
by (metis "1" affp face_of_imp_subset hull_subset le_inf_iff that)
have dim_f_hyperplane: "aff_dim (f ∩ {x. x ∙ i = 1}) = int d"
if "f face_of S" "aff_dim f = 1 + int d" for f
proof -
have "conic f"
using ‹conic S› face_of_conic that(1) by blast
then have "0 ∈ f"
using conic_contains_0 that by force
moreover have "¬ f ⊆ {0}"
using subset_singletonD that(2) by fastforce
ultimately obtain y where y: "y ∈ f" "y ≠ 0"
by blast
then have "y ∙ i > 0"
using doti_gt0 face_of_imp_subset that(1) by blast
have "aff_dim (conic hull (f ∩ {x. x ∙ i = 1})) = aff_dim (f ∩ {x. x ∙ i = 1}) + 1"
proof (rule aff_1d)
show "f ∩ {x. x ∙ i = 1} face_of p"
by (simp add: face_S_imp_face_p that(1))
have "inverse(y ∙ i) *⇩R y ∈ f"
using ‹0 < y ∙ i› ‹conic S› conic_mul face_of_conic that(1) y(1) by fastforce
moreover have "inverse(y ∙ i) *⇩R y ∈ {x. x ∙ i = 1}"
using ‹y ∙ i > 0› by (simp add: field_simps)
ultimately show "f ∩ {x. x ∙ i = 1} ≠ {}"
by blast
qed
then show ?thesis
by (simp add: conic_hyperplane_eq that)
qed
have "card {f. f face_of S ∧ aff_dim f = 1 + int d}
= card {f. f face_of p ∧ aff_dim f = int d}"
proof (intro bij_betw_same_card bij_betw_imageI)
show "inj_on (λf. f ∩ {x. x ∙ i = 1}) {f. f face_of S ∧ aff_dim f = 1 + int d}"
by (smt (verit) conic_hyperplane_eq inj_on_def mem_Collect_eq of_nat_less_0_iff)
show "(λf. f ∩ {x. x ∙ i = 1}) ` {f. f face_of S ∧ aff_dim f = 1 + int d} = {f. f face_of p ∧ aff_dim f = int d}"
using aff_1d conic_eq_f conic_face_p
by (fastforce simp: image_iff face_S_imp_face_p dim_f_hyperplane)
qed
}
then show ?thesis
by force
qed
finally show ?thesis .
qed
ultimately show ?thesis
by auto
qed
qed
corollary Euler_poincare_special:
fixes p :: "'n::euclidean_space set"
assumes "2 ≤ DIM('n)" "polytope p" "i ∈ Basis" and affp: "affine hull p = {x. x ∙ i = 0}"
shows "(∑d = 0..DIM('n) - 1. (-1) ^ d * card {f. f face_of p ∧ aff_dim f = d}) = 1"
proof -
{ fix d
have eq: "image((+) i) ` {f. f face_of p} ∩ image((+) i) ` {f. aff_dim f = int d}
= image((+) i) ` {f. f face_of p} ∩ {f. aff_dim f = int d}"
by (auto simp: aff_dim_translation_eq)
have "card {f. f face_of p ∧ aff_dim f = int d} = card (image((+) i) ` {f. f face_of p ∧ aff_dim f = int d})"
by (simp add: inj_on_image card_image)
also have "… = card (image((+) i) ` {f. f face_of p} ∩ {f. aff_dim f = int d})"
by (simp add: Collect_conj_eq image_Int inj_on_image eq)
also have "… = card {f. f face_of (+) i ` p ∧ aff_dim f = int d}"
by (simp add: Collect_conj_eq faces_of_translation)
finally have "card {f. f face_of p ∧ aff_dim f = int d} = card {f. f face_of (+) i ` p ∧ aff_dim f = int d}" .
}
then
have "(∑d = 0..DIM('n) - 1. (-1) ^ d * card {f. f face_of p ∧ aff_dim f = d})
= (∑d = 0..DIM('n) - 1. (-1) ^ d * card {f. f face_of (+) i ` p ∧ aff_dim f = int d})"
by simp
also have "… = 1"
proof (rule Euler_Poincare_lemma)
have "⋀x. ⟦i ∈ Basis; x ∙ i = 1⟧ ⟹ ∃y. y ∙ i = 0 ∧ x = y + i"
by (metis add_cancel_left_left eq_diff_eq inner_diff_left inner_same_Basis)
then show "affine hull (+) i ` p = {x. x ∙ i = 1}"
using ‹i ∈ Basis› unfolding affine_hull_translation affp by (auto simp: algebra_simps)
qed (use assms polytope_translation_eq in auto)
finally show ?thesis .
qed
subsection ‹Now Euler-Poincare for a general full-dimensional polytope›
theorem Euler_Poincare_full:
fixes p :: "'n::euclidean_space set"
assumes "polytope p" "aff_dim p = DIM('n)"
shows "(∑d = 0..DIM('n). (-1) ^ d * (card {f. f face_of p ∧ aff_dim f = d})) = 1"
proof -
define augm:: "'n ⇒ 'n × real" where "augm ≡ λx. (x,0)"
define S where "S ≡ augm ` p"
obtain i::'n where i: "i ∈ Basis"
by (meson SOME_Basis)
have "bounded_linear augm"
by (auto simp: augm_def bounded_linearI')
then have "polytope S"
unfolding S_def using polytope_linear_image ‹polytope p› bounded_linear.linear by blast
have face_pS: "⋀F. F face_of p ⟷ augm ` F face_of S"
using S_def ‹bounded_linear augm› augm_def bounded_linear.linear face_of_linear_image inj_on_def by blast
have aff_dim_eq[simp]: "aff_dim (augm ` F) = aff_dim F" for F
using ‹bounded_linear augm› aff_dim_injective_linear_image bounded_linear.linear
unfolding augm_def inj_on_def by blast
have *: "{F. F face_of S ∧ aff_dim F = int d} = (image augm) ` {F. F face_of p ∧ aff_dim F = int d}"
(is "?lhs = ?rhs") for d
proof
have "⋀G. ⟦G face_of S; aff_dim G = int d⟧
⟹ ∃F. F face_of p ∧ aff_dim F = int d ∧ G = augm ` F"
by (metis face_pS S_def aff_dim_eq face_of_imp_subset subset_imageE)
then show "?lhs ⊆ ?rhs"
by (auto simp: image_iff)
qed (auto simp: image_iff face_pS)
have ceqc: "card {f. f face_of S ∧ aff_dim f = int d} = card {f. f face_of p ∧ aff_dim f = int d}" for d
unfolding *
by (rule card_image) (auto simp: inj_on_def augm_def)
have "(∑d = 0..DIM('n × real) - 1. (- 1) ^ d * int (card {f. f face_of S ∧ aff_dim f = int d})) = 1"
proof (rule Euler_poincare_special)
show "2 ≤ DIM('n × real)"
by auto
have snd0: "(a, b) ∈ affine hull S ⟹ b = 0" for a b
using S_def ‹bounded_linear augm› affine_hull_linear_image augm_def by blast
moreover have "⋀a. (a, 0) ∈ affine hull S"
using S_def ‹bounded_linear augm› aff_dim_eq_full affine_hull_linear_image assms(2) augm_def by blast
ultimately show "affine hull S = {x. x ∙ (0::'n, 1::real) = 0}"
by auto
qed (auto simp: ‹polytope S› Basis_prod_def)
then show ?thesis
by (simp add: ceqc)
qed
text ‹In particular, the Euler relation in 3 dimensions›
corollary Euler_relation:
fixes p :: "'n::euclidean_space set"
assumes "polytope p" "aff_dim p = 3" "DIM('n) = 3"
shows "(card {v. v face_of p ∧ aff_dim v = 0} + card {f. f face_of p ∧ aff_dim f = 2}) - card {e. e face_of p ∧ aff_dim e = 1} = 2"
proof -
have "⋀x. ⟦x face_of p; aff_dim x = 3⟧ ⟹ x = p"
using assms by (metis face_of_aff_dim_lt less_irrefl polytope_imp_convex)
then have 3: "{f. f face_of p ∧ aff_dim f = 3} = {p}"
using assms by (auto simp: face_of_refl polytope_imp_convex)
have "(∑d = 0..3. (-1) ^ d * int (card {f. f face_of p ∧ aff_dim f = int d})) = 1"
using Euler_Poincare_full [of p] assms by simp
then show ?thesis
by (simp add: sum.atLeast0_atMost_Suc_shift numeral_3_eq_3 3)
qed
end