Crosscutを持たない開集合は凸集合の補集合である
本記事では、crosscut を持たない開集合が凸集合の補集合であることを証明します。
なお、本記事は諸事情につき、お蔵入り的な性格が強い内容となっています。
(本当はMotzkinの定理と呼ばれる、閉集合におけるユークリッド射影の一意性と凸性の同値性に関する定理を示したかったのですが、crosscut を用いた手法は厳密性に議論することがかなり難しそうに思われます。そのため、本記事ではその crosscut に関する議論のみを紹介します。)
ただし、本記事の範囲内において、誤りはないと思います。本記事の末尾に、Lean4による形式化も掲載しています。
定義
以下、$L$ を位相線型空間とします。本記事では簡単のために $L=\mathbb{R}^n$ としますが、他の空間でも同様の議論が成り立ちます。また、集合 $S \subseteq L$ に対して、$S$ の内部を $\operatorname{int} S$、境界を $\operatorname{bd} S$、補集合を $S^c$ と表します。
線分
$x,y \in L$ に対して、閉線分 $xy$ は次のように定義されます（文献1 Definition 1.2）:
xy= \left\lbrace \alpha x+\beta y \mathrel{\mid} \alpha, \beta \geq 0, \ \alpha+\beta=1 \right\rbrace.
また、$x \neq y$ のとき、開線分 $\operatorname{intv} xy$ は次のように定義されます（文献1 Definition 1.8）:
\operatorname{intv} xy = \left\lbrace \alpha x+\beta y \mathrel{\mid} \alpha, \beta > 0,\ \alpha+\beta=1 \right\rbrace.
閉線分 $xy$ は端点 $x,y$ を含みますが、開線分 $\operatorname{intv} xy$ は $x \neq y$ のとき端点を含みません。
ただし、例外として $x=y$ のときは、閉線分 $xy$ と開線分 $\operatorname{intv} xy$ はともに $\lbrace x \rbrace$ となり、端点を含みます。
凸集合
集合 $S \subseteq L$ が凸(convex)であることは、任意の $x,y \in S$ に対して、閉線分 $xy$ が再び $S$ に含まれることと同値です（文献1 Definition 1.3）:
x,y \in S \implies xy \subseteq S.
なお、端点は自明に $S$ に含まれるので、次も同値な条件です:
x, y \in S \implies \operatorname{intv} xy \subseteq S
Crosscut
集合 $S \subseteq L$ と $x,y \in \operatorname{bd} S$ に対して、閉線分 $xy$ が $S$ の crosscut であることは、開線分 $\operatorname{intv} xy$ が $S$ の内部に含まれることと同値です（文献1 Definition 4.1）:
\begin{gather*}
xy \text{ is a crosscut of } S\\
\iff\\
x,y \in \operatorname{bd} S,\ x \neq y,\ \operatorname{intv} xy \subseteq \operatorname{int}S.
\end{gather*}
つまり、crosscut とは、両端点が境界上にあり、その間の点がすべて内部に入っているような線分です。
Crosscut を持たない集合は凸集合の補集合である
以下を示します(文献1 Theorem 4.2):
$K$ を開集合とする。$K$ が crosscut を持たないならば、$K$ はある凸集合の補集合である。
より直感的な解釈としては、対偶により次のように言い換えることができます:
$K^c$ を閉集合とする。$K^c$ が凸集合でなければ、$K$ は crosscut を持つ。
通常は集合の凸性に関する特徴づけを主張する定理が多いですが、この主張は非凸性の特徴づけとなっています。
それ故に、非凸集合が出てきたときに、この crosscut を構成することが出来て、そこから議論を展開することが出来る、という点で少し面白い定理だと思います。
証明
以下では、先述の主張を証明していきます。なお、本記事での証明は、文献1 における行間を埋めたものになっています。この証明の更なる行間は、本記事末尾のLeanによる証明で埋めています。
集合 $K$ の補集合 $K^c$ が凸であることを示します。定義より、任意の $x,y \in K^c$ に対して、開線分 $\operatorname{intv} xy$ が $K^c$ に含まれることを示せばよいです。
背理法で示します。補集合の定義より、
\operatorname{intv} xy \cap K \neq \emptyset
であると仮定したときに、矛盾が導ける、つまり、$K$ が crosscut を持つことが示されることを目指します。まず、この仮定から、
z \in \operatorname{intv} xy \cap K
が存在します。特に、$K$ は開集合なので、
z \in \operatorname{int}K
です。このとき、ある $u,v \in \operatorname{bd} K$ が閉線分 $xy$ 上に存在して、$uv$ が $K$ の crosscut になることを示します。先述の通り、これが示されれば、矛盾が導け主張が証明されます。
以下では $u$ を構成する方法を説明します。$v$ も同様に構成できます。$x$ と $z$ を結ぶ線分上の点をパラメータ $t \in [0, 1]$ を用いて表すと、$\gamma(t) = (1-t)x + tz$ と書けます。このとき、実数の完備性により、次のように $t_u$ および $u$ を構成できます。
\begin{align*}
t_u &\mathrel{\vcenter{:}}= \inf \lbrace t \in [0, 1] \mid \forall s \in (t, 1], \gamma(s) \in K \rbrace\\
u & \mathrel{\vcenter{:}}= \gamma(t_u)
\end{align*}
すると、次のことが成り立ちます:
- $u \neq z$, （$x \notin K, z \in K$ と $K$ の開集合性）
- $u \in \operatorname{bd} K$, （$\gamma$ の連続性と境界の定義）
- $u \in xz$, （$u$ は $x$ であってもよい。crosscut の節における図の2番目の例を参照）
- $(u, z] \subseteq \operatorname{int} K$. （$u$ の構成）
同様に $v$ も構成して、二点 $u,v$ を考えると次を満たします:
- $u,v \in \operatorname{bd} K$,
- $u \neq v$,
- $\operatorname{intv} uv \subseteq \operatorname{int}K$.
これは、閉線分 $uv$ が $K$ の crosscut であることの定義そのものです。よって、確かに $K$ は crosscut を持ち、矛盾が導けました。
Lean による形式化
先ほども言及しましたが、この証明はLean4による形式化も行っています。Lean4とは、数学の証明をコードとして記述することで、機械的に証明を検証できる「定理証明支援系」の機能を持つ純粋関数型プログラミング言語です。命題の記述が正しい限りにおいて、証明の正しさを機械的に保証できることが強みです。
まず、以下に証明の骨格を示します。一部の補題は、後述で示します。(若干補足をコメントで書いているので、こちらだけならLean4を知らない方でもある程度理解できると思います。)
import Motzkin.Crosscut
variable {n : ℕ}
local notation "L" => EuclideanSpace ℝ (Fin n)
/-- `xy` is a crosscut of `K`. -/
def IsCrosscut (K : Set L) (x y : L) : Prop :=
x ∈ frontier K ∧ -- frontier K is the boundary of K
y ∈ frontier K ∧
x ≠ y ∧
openSegment ℝ x y ⊆ interior K
/-- `K` has no crosscuts. -/
def HasNoCrosscut (K : Set L) : Prop :=
∀ x y : L, ¬ IsCrosscut K x y
/-- Lemma asserting the existence of a frontier point `u`. -/
lemma exists_frontier_point_segment_to_interior
{K : Set L} (hK : IsOpen K) {x z : L}
(hx : x ∈ compl K) (hz : z ∈ interior K) :
∃ u : L,
u ≠ z ∧
u ∈ frontier K ∧
u ∈ segment ℝ x z ∧
openSegment ℝ u z ⊆ interior K := by
-- The proof is provided in `Crosscut.lean`.
exact _exists_frontier_point_segment_to_interior hK hx hz
/--
Lemma asserting the intv uv ⊆ intv uz ∪ {z} ∪ intv zv.
`x` -- `u` -- `z` -- `v` -- `y`
-/
lemma openSegment_uv_ordered
{x y z u v : L}
(hNegUZ : u ≠ z)
(hNegZV : z ≠ v)
(hz : z ∈ openSegment ℝ x y)
(hu : u ∈ segment ℝ x z)
(hv : v ∈ segment ℝ z y) :
u ≠ v ∧
openSegment ℝ u v ⊆
openSegment ℝ u z ∪ {z} ∪ openSegment ℝ z v := by
exact _openSegment_uv_ordered hNegUZ hNegZV hz hu hv
/--
Theorem 4.2 in "Convex sets"
If an open set `K` has no crosscut, then its complement is convex.
Reference:
Valentine, F. A. (1964). Convex sets.
McGraw-Hill series in higher mathematics. McGraw-Hill Book Company.
-/
lemma thm_4_2 {K : Set L}
(hKIsOpen : IsOpen K)
(hK : HasNoCrosscut K) :
Convex ℝ (compl K) := by
-- By the definition of convexity, we need to show that
-- `z ∈ Kᶜ` when
-- `x` : a point in `L`
-- `hx` : x ∈ Kᶜ
-- `y` : a point in `L`
-- `hy` : y ∈ Kᶜ
-- `z` : a point in `L`
-- `hz_seg` : z ∈ openSegment ℝ x y
apply convex_iff_openSegment_subset.mpr
intro x hx y hy z hz_seg
-- By the definition of the complement,
-- we have to show `False` when `hz` : z ∈ K.
by_contra hzK
simp at hzK
-- Since `K` is open, we have `z ∈ interior K`.
have hz_int : z ∈ interior K := by
simpa [hKIsOpen.interior_eq] using hzK
-- Obtain `u` and `v` in the frontier of `K` such that
-- `u` : L
-- `hNeqUZ` : u ≠ z
-- `hu_frontier` : u ∈ frontier K
-- `hu_xz` : u ∈ segment ℝ x z
-- `hu_sub` : openSegment ℝ u z ⊆ interior K
obtain ⟨u, hNeqUZ, hu_frontier, hu_xz, hu_sub⟩ :=
exists_frontier_point_segment_to_interior hKIsOpen hx hz_int
-- Similarly, we can obtain `v`.
obtain ⟨v, hNeqZV, hv_frontier, hv_yz_symm, hv_sub_symm⟩ :=
exists_frontier_point_segment_to_interior hKIsOpen hy hz_int
-- Convert `v ∈ segment ℝ y z` to `v ∈ segment ℝ z y`
have hv_yz : v ∈ segment ℝ z y := by
simpa [segment_symm] using hv_yz_symm
-- From the above, we can derive that
-- `hNeqUV` : u ≠ v
-- `hOpenSegUVDecomp` : openSegment ℝ u v ⊆ openSegment ℝ u z ∪ {z} ∪ openSegment ℝ z v
obtain ⟨hNeqUV, hOpenSegUVDecomp⟩ := openSegment_uv_ordered hNeqUZ hNeqZV.symm hz_seg hu_xz hv_yz
-- Finally, we show the contradiction by showing
-- `uv` is a crosscut of `K`, which contradicts the assumption `hK`.
-- Now, the goal changes to show that `openSegment ℝ u v ⊆ interior K`,
-- which is the last condition for `uv` to be a crosscut of `K`.
refine hK u v ⟨hu_frontier, hv_frontier, hNeqUV, ?_⟩
-- We show it by saying that `w ∈ openSegment ℝ u v` implies `w ∈ interior K`.
intro w hw
-- By the decomposition of `openSegment ℝ u v`, we have three cases:
rcases hOpenSegUVDecomp hw with (hwuz | hwz) | hwzv
· -- w ∈ openSegment ℝ u z
exact hu_sub hwuz
· -- w ∈ {z}
rw [hwz]
exact hz_int
· -- w ∈ openSegment ℝ z v
apply hv_sub_symm
rw [openSegment_symm]
exact hwzv
そして、先ほど省略した補題が以下になります。ここが、正に記事の本文でも説明を省略した行間を埋める部分になります。
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.Convex.Between
open Set AffineMap Metric
open scoped Topology
variable {n : ℕ}
local notation "L" => EuclideanSpace ℝ (Fin n)
def segmentPath (x z : L) : ℝ → L :=
fun t => (1 - t) • x + t • z
lemma _exists_mem_tailSet_lt_one
{K : Set L} (hK : IsOpen K) {x z : L} (hzK : z ∈ K) :
∃ t, 0 ≤ t ∧ t < 1 ∧ ∀ s ∈ Ioc t 1, segmentPath x z s ∈ K := by
let γ := segmentPath x z
have hpre : {t : ℝ | γ t ∈ K} ∈ 𝓝 (1 : ℝ) := by
have hz : γ 1 ∈ K := by
simpa [γ, segmentPath] using hzK
have continuous_segXZ : Continuous γ := by
unfold γ segmentPath
continuity
exact (continuous_segXZ.continuousAt (x := 1)).preimage_mem_nhds
(hK.mem_nhds hz)
rcases Metric.mem_nhds_iff.mp hpre with ⟨ε, hεpos, hεsub⟩
let δ : ℝ := min 1 ε
use 1 - δ
have hδpos : 0 < δ := lt_min (by norm_num) (by linarith)
have hδle1 : δ ≤ 1 := min_le_left _ _
have hδleε : δ ≤ ε := min_le_right _ _
refine ⟨?_, ?_, ?_⟩
· simpa using hδle1
· simpa using hδpos
· intro s ⟨hst, hsle⟩
apply hεsub
rw [Metric.mem_ball, Real.dist_eq]
rw [abs_of_nonpos (by linarith : s - 1 ≤ 0)]
linarith
lemma _exists_frontier_point_segment_to_interior
{K : Set L} (hK : IsOpen K) {x z : L}
(hx : x ∈ compl K) (hz : z ∈ interior K) :
∃ u : L,
u ≠ z ∧
u ∈ frontier K ∧
u ∈ segment ℝ x z ∧
openSegment ℝ u z ⊆ interior K := by
let γ := segmentPath x z
let A : Set ℝ := {t : ℝ | t ∈ Icc (0 : ℝ) 1 ∧ ∀ s ∈ Ioc t 1, γ s ∈ K}
let a : ℝ := sInf A
let u : L := γ a
use u
have hxK : x ∉ K := by simpa using hx
have hzK : z ∈ K := by simpa [hK.interior_eq] using hz
have hγ_cont : Continuous γ := by
unfold γ segmentPath
continuity
rcases _exists_mem_tailSet_lt_one hK (x := x) hzK with ⟨t₀, ht₀_ge_zero, ht₀_lt_one, htail⟩
have ht₀A : t₀ ∈ A := by exact ⟨⟨ht₀_ge_zero, le_of_lt ht₀_lt_one⟩, htail⟩
have hAne : A.Nonempty := ⟨t₀, ht₀A⟩
clear hzK ht₀_ge_zero htail
have hAbdd : BddBelow A := by
refine ⟨0, ?_⟩
intro t ht
exact ht.1.1
have haIco : a ∈ Ico (0 : ℝ) 1 := by
constructor
· exact le_csInf hAne fun t ht => ht.1.1
· exact lt_of_le_of_lt (csInf_le hAbdd ht₀A) ht₀_lt_one
have htail : ∀ s ∈ Ioc a 1, γ s ∈ K := by
intro s hs
have hex : ∃ t ∈ A, t < s := by
by_contra hnone
push Not at hnone
have hsle : s ≤ a := by
refine le_csInf hAne ?_
intro t ht
exact hnone t ht
linarith [hs.1]
rcases hex with ⟨t, htA, hts⟩
exact htA.2 s ⟨hts, hs.2⟩
have htail_int : ∀ s ∈ Ioc a 1, γ s ∈ interior K := by
intro s hs
simpa [hK.interior_eq] using htail s hs
have hu_closure : u ∈ closure K := by
rw [mem_closure_iff_nhds]
intro V hV
have hpre : γ ⁻¹' V ∈ 𝓝 a := by
simpa [u] using hγ_cont.continuousAt hV
rcases Metric.mem_nhds_iff.mp hpre with ⟨ε, hεpos, hεsub⟩
let δ : ℝ := min (ε / 2) ((1 - a) / 2)
let t : ℝ := a + δ
have hδpos : 0 < δ := by
exact lt_min (by linarith) (by linarith [haIco.2])
have ht1 : t < 1 := by
have hδle : δ ≤ (1 - a) / 2 := by
exact min_le_right _ _
dsimp [t]
linarith
have ht_ball : t ∈ Metric.ball a ε := by
rw [Metric.mem_ball, Real.dist_eq]
have ht_sub : t - a = δ := by ring
rw [ht_sub, abs_of_nonneg (le_of_lt hδpos)]
have hδle : δ ≤ ε / 2 := by exact min_le_left _ _
linarith
have hsInf_lt_t : sInf A < t := by linarith
rcases (csInf_lt_iff hAbdd hAne).1 hsInf_lt_t with ⟨b, hbA, hbt⟩
exact ⟨γ t, hεsub ht_ball, hbA.2 t ⟨hbt, le_of_lt ht1⟩⟩
have hu_not_int : u ∉ interior K := by
intro hu_int
have huK : u ∈ K := by
simpa [hK.interior_eq] using hu_int
have hprea : {t : ℝ | γ t ∈ K} ∈ 𝓝 a := by
have hK_nhds_u : K ∈ 𝓝 (γ a) := by
simpa [u] using hK.mem_nhds huK
exact hγ_cont.continuousAt.preimage_mem_nhds hK_nhds_u
rcases Metric.mem_nhds_iff.mp hprea with ⟨ε, hεpos, hεsub⟩
have ha_pos : 0 < a := by
apply lt_of_le_of_ne haIco.1
intro ha0
have hx_in_K : x ∈ K := by
simpa [u, γ, segmentPath, ha0.symm] using huK
exact hxK hx_in_K
let δ : ℝ := min a ε
let b : ℝ := a - δ
have hδpos : 0 < δ := by exact lt_min (by linarith) hεpos
have hδle_a : δ ≤ a := by exact min_le_left _ _
have hδleε : δ ≤ ε := by exact min_le_right _ _
have hb_lt_a : b < a := by linarith [hδpos]
have hbA : b ∈ A := by
constructor
· constructor
· linarith [haIco.1, hδle_a]
· linarith [haIco.2, hδpos]
· intro s hs
by_cases hsa : s ≤ a
· apply hεsub
rw [Metric.mem_ball, Real.dist_eq]
have habs : |s - a| = a - s := by
have h_nonpos : s - a ≤ 0 := by linarith
rw [abs_of_nonpos h_nonpos]
linarith
rw [habs]
have h_as_lt_delta : a - s < δ := by
dsimp [b] at hs
linarith [hs.1]
linarith [h_as_lt_delta, hδleε]
· exact htail s ⟨lt_of_not_ge hsa, hs.2⟩
have ha_le_b : a ≤ b :=
csInf_le hAbdd hbA
linarith [hb_lt_a, ha_le_b]
refine ⟨?_, ?_, ?_, ?_⟩
· -- u ≠ z := by
intro huz
exact hu_not_int (by simpa [huz] using hz)
· -- u ∈ frontier K := by
rw [frontier]
exact ⟨hu_closure, hu_not_int⟩
· -- u ∈ segment ℝ x z := by
dsimp [u, γ, segmentPath]
refine ⟨1 - a, a, by linarith [haIco.2], by exact haIco.1, by ring, rfl⟩
· -- openSegment ℝ u z ⊆ interior K := by
intro w hw
rw [openSegment_eq_image'] at hw
rcases hw with ⟨t, ⟨ht0, ht1⟩, rfl⟩
simp
let s : ℝ := (1 - t) * a + t * 1
have hs : s ∈ Ioc a 1 := by
constructor <;> nlinarith [ht0, ht1, haIco.2]
have hγs : (1 - t) • u + t • z = γ s := by
ext i
simp [u, γ, segmentPath, s]
ring
have hγsInt : γ s ∈ interior K := by
exact htail_int s hs
have h_eq : u + t • (z - u) = (1 - t) • u + t • z := by
rw [smul_sub, sub_smul, one_smul]
abel
rw [h_eq, hγs]
exact hγsInt
/--
`x` -- `u` -- `z` -- `v` -- `y`
-/
lemma _openSegment_uv_ordered
{x y z u v : L}
(hNegUZ : u ≠ z)
(hNegZV : z ≠ v)
(hz : z ∈ openSegment ℝ x y)
(hu : u ∈ segment ℝ x z)
(hv : v ∈ segment ℝ z y) :
u ≠ v ∧
openSegment ℝ u v ⊆
openSegment ℝ u z ∪ {z} ∪ openSegment ℝ z v := by
have hZInUV : z ∈ range (lineMap u v : ℝ → L) := by
rw [openSegment_eq_image_lineMap] at hz
rw [segment_eq_image_lineMap] at hu hv
rcases hz with ⟨a, ⟨ha0, ha1⟩, rfl⟩
rcases hu with ⟨b, ⟨hb0, hb1⟩, rfl⟩
rcases hv with ⟨c, ⟨hc0, hc1⟩, rfl⟩
let α : ℝ := b * a
let β : ℝ := a + c * (1 - a)
refine ⟨(a - α) / (β - α), ?_⟩
have hden_ne : β - α ≠ 0 := by
have hc_pos : 0 < c := by
exact lt_of_le_of_ne hc0 fun hc_eq => hNegZV (by subst hc_eq; simp)
exact ne_of_gt <| by nlinarith
calc
lineMap
(lineMap x (lineMap x y a) b)
(lineMap (lineMap x y a) y c)
((a - α) / (β - α))
=
lineMap
(lineMap x y α)
(lineMap x y β)
((a - α) / (β - α)) := by
dsimp [α]
simp [lineMap_apply]
module
_ =
lineMap x y
((1 - (a - α) / (β - α)) * α
+ ((a - α) / (β - α)) * β) := by
simp [lineMap_apply]
module
_ = lineMap x y a := by
congr 1
field_simp [hden_ne]
ring
constructor
· intro hUV
subst v
simp at hZInUV
exact hNegUZ hZInUV
· intro w hw
have hSubset := openSegment_subset_union u v hZInUV
rcases hSubset hw with rfl | hWInUZ | hWInZV
· simp
· tauto
· tauto
Valentineの本について
本記事で参照させていただいたValentineの本は、今回東大の工学部6号館にある図書館の地下の可動式書庫を動かしてようやく読むことが出来ました。かなり古めかしい本で、ネット上に情報が少ないのも頷けます。
本書において、先ほどの crosscut に関する主張は、次のように証明されています。
Lean4による証明と比べて、めちゃくちゃ短いですね……。
個人的に、これは本当にいろいろなことに対して示唆的だと思っています。 人間がもつ数学的対象に対する直感の強さ、Lean4が持つ機械的な検証能力の豊かさ、そして一世紀近くも前に発表された数学の定理がその検証に耐えられるだけの厳密性をなお持っていることに対する衝撃を感じます。
本記事を執筆した動機の一つは、このような良書が誰にも知られずに朽ちていくのは非常に口惜しく感じたからでした。
本記事が過去と現在の数学の橋渡しの一助になれば良いなと思いつつ、ここで筆を置きたいと思います。