def HyperplaneSeparates (n : ℕ) (H C₁ C₂ : Set (Fin n → ℝ)) : Prop

Text 11.0.1: Let C₁ and C₂ be non-empty sets in ℝ^n. A hyperplane H is said to separate C₁ and C₂ if C₁ is contained in one of the closed half-spaces associated with H and C₂ lies in the opposite closed half-space.

Equations

• One or more equations did not get rendered due to their size.

def HyperplaneSeparatesProperly (n : ℕ) (H C₁ C₂ : Set (Fin n → ℝ)) : Prop

Text 11.0.2: A hyperplane H is said to separate C₁ and C₂ properly if C₁ and C₂ are not both actually contained in H itself.

Equations

• HyperplaneSeparatesProperly n H C₁ C₂ = (HyperplaneSeparates n H C₁ C₂ ∧ ¬(C₁ ⊆ H ∧ C₂ ⊆ H))

theorem not_both_subset_of_hyperplaneSeparatesProperly {n : ℕ} {H C₁ C₂ : Set (Fin n → ℝ)} : HyperplaneSeparatesProperly n H C₁ C₂ → ¬(C₁ ⊆ H ∧ C₂ ⊆ H)

Extract the "properness" clause from HyperplaneSeparatesProperly: the two sets cannot both lie entirely in the separating hyperplane.

theorem subset_left_imp_not_subset_right {α : Type u_1} {A B H : Set α} (hnot : ¬(A ⊆ H ∧ B ⊆ H)) : A ⊆ H → ¬B ⊆ H

Pure-Prop helper: from ¬ (A ⊆ H ∧ B ⊆ H) we get A ⊆ H → ¬ B ⊆ H.

theorem subset_right_imp_not_subset_left {α : Type u_1} {A B H : Set α} (hnot : ¬(A ⊆ H ∧ B ⊆ H)) : B ⊆ H → ¬A ⊆ H

Pure-Prop helper: from ¬ (A ⊆ H ∧ B ⊆ H) we get B ⊆ H → ¬ A ⊆ H.

theorem hyperplaneSeparatesProperly_imp_atMostOne_subset_hyperplane (n : ℕ) (H C₁ C₂ : Set (Fin n → ℝ)) : HyperplaneSeparatesProperly n H C₁ C₂ → (C₁ ⊆ H → ¬C₂ ⊆ H) ∧ (C₂ ⊆ H → ¬C₁ ⊆ H)

Text 11.1.1: Proper separation allows that one (but not both) of the sets be contained in the separating hyperplane itself.

def HyperplaneSeparatesStrongly (n : ℕ) (H C₁ C₂ : Set (Fin n → ℝ)) : Prop

Text 11.0.3: A hyperplane H is said to separate C₁ and C₂ strongly if there exists ε > 0 such that C₁ + ε B is contained in one of the open half-spaces associated with H and C₂ + ε B is contained in the opposite open half-space, where B is the unit Euclidean ball {x | ‖x‖ ≤ 1}. (Here Cᵢ + ε B consists of points x such that ‖x - y‖ ≤ ε for at least one y ∈ Cᵢ.)

Equations

• One or more equations did not get rendered due to their size.

def C11_1_2_C1 : Set (Fin 2 → ℝ)

The set C₁ from Text 11.1.2 (a closed convex "hyperbola region").

Equations

• C11_1_2_C1 = {x : Fin 2 → ℝ | 0 ≤ x 0 ∧ 1 ≤ x 0 * x 1}

def C11_1_2_C2 : Set (Fin 2 → ℝ)

The set C₂ from Text 11.1.2 (a closed convex ray on the x-axis).

Equations

• C11_1_2_C2 = {x : Fin 2 → ℝ | 0 ≤ x 0 ∧ x 1 = 0}

theorem C11_1_2_C1_pos {x : Fin 2 → ℝ} (hx : x ∈ C11_1_2_C1) : 0 < x 0

Any point in C11_1_2_C1 has strictly positive first coordinate.

theorem inv_le_coord1_of_mem_C11_1_2_C1 {x : Fin 2 → ℝ} (hx : x ∈ C11_1_2_C1) : (x 0)⁻¹ ≤ x 1

Any point in C11_1_2_C1 satisfies the equivalent inequality x0⁻¹ ≤ x1.

theorem C11_1_2_closed_convex_disjoint : IsClosed C11_1_2_C1 ∧ IsClosed C11_1_2_C2 ∧ Convex ℝ C11_1_2_C1 ∧ Convex ℝ C11_1_2_C2 ∧ Disjoint C11_1_2_C1 C11_1_2_C2

The sets C11_1_2_C1 and C11_1_2_C2 are closed and convex and disjoint.

theorem C11_1_2_thickenings_intersect (ε : ℝ) : ε > 0 → have B := {x : Fin 2 → ℝ | ‖x‖ ≤ 1}; ∃ z ∈ C11_1_2_C1 + ε • B, z ∈ C11_1_2_C2 + ε • B

Any ε-thickening of C11_1_2_C1 and C11_1_2_C2 intersects (hence no strong separation).

theorem C11_1_2_not_hyperplaneSeparatesStrongly : ¬∃ (H : Set (Fin 2 → ℝ)), HyperplaneSeparatesStrongly 2 H C11_1_2_C1 C11_1_2_C2

The counterexample sets cannot be separated strongly by any hyperplane.

theorem exists_disjoint_closed_convex_not_hyperplaneSeparatesStrongly : ∃ (n : ℕ) (C₁ : Set (Fin n → ℝ)) (C₂ : Set (Fin n → ℝ)), IsClosed C₁ ∧ IsClosed C₂ ∧ Convex ℝ C₁ ∧ Convex ℝ C₂ ∧ Disjoint C₁ C₂ ∧ ¬∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesStrongly n H C₁ C₂

Text 11.1.2: Not every pair of disjoint closed convex sets can be separated strongly.

def HyperplaneSeparatesStrictly (n : ℕ) (H C₁ C₂ : Set (Fin n → ℝ)) : Prop

Text 11.0.4: Strict separation means that C₁ and C₂ are contained in opposing open half-spaces determined by a hyperplane H.

Equations

• One or more equations did not get rendered due to their size.

theorem hyperplaneSeparatesProperly_oriented (n : ℕ) (H C₁ C₂ : Set (Fin n → ℝ)) : HyperplaneSeparatesProperly n H C₁ C₂ → ∃ (b : Fin n → ℝ) (β : ℝ), b ≠ 0 ∧ H = {x : Fin n → ℝ | x ⬝ᵥ b = β} ∧ (∀ x ∈ C₁, β ≤ x ⬝ᵥ b) ∧ (∀ x ∈ C₂, x ⬝ᵥ b ≤ β) ∧ ¬(C₁ ⊆ H ∧ C₂ ⊆ H)

Put a properly separating hyperplane in a consistent "oriented" form: C₁ lies in {x | β ≤ x ⬝ᵥ b} and C₂ lies in {x | x ⬝ᵥ b ≤ β}.

theorem sInf_ge_sSup_of_pointwise_bounds_EReal {n : ℕ} {C₁ C₂ : Set (Fin n → ℝ)} (b : Fin n → ℝ) (β : ℝ) (hC₁ : ∀ x ∈ C₁, β ≤ x ⬝ᵥ b) (hC₂ : ∀ x ∈ C₂, x ⬝ᵥ b ≤ β) : sInf ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b)) '' C₁) ≥ sSup ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b)) '' C₂)

If C₁ lies in {x | β ≤ x ⬝ᵥ b} and C₂ lies in {x | x ⬝ᵥ b ≤ β}, then the extended infimum of x ⬝ᵥ b over C₁ is at least the extended supremum over C₂.

theorem sSup_gt_sInf_of_not_both_subset_levelset_EReal {n : ℕ} {C₁ C₂ : Set (Fin n → ℝ)} (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) (b : Fin n → ℝ) (β : ℝ) (hC₁ : ∀ x ∈ C₁, β ≤ x ⬝ᵥ b) (hC₂ : ∀ x ∈ C₂, x ⬝ᵥ b ≤ β) (hnot : ¬(C₁ ⊆ {x : Fin n → ℝ | x ⬝ᵥ b = β} ∧ C₂ ⊆ {x : Fin n → ℝ | x ⬝ᵥ b = β})) : sSup ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b)) '' C₁) > sInf ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b)) '' C₂)

Properness forces strict separation between the extended sSup on C₁ and extended sInf on C₂ under the same half-space inclusions.

theorem exists_hyperplaneSeparatesProperly_of_EReal_inf_sup_conditions (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) (hC₁ : C₁.Nonempty) (hC₂ : C₂.Nonempty) (b : Fin n → ℝ) (ha : sInf ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b)) '' C₁) ≥ sSup ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b)) '' C₂)) (hb : sSup ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b)) '' C₁) > sInf ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b)) '' C₂)) : ∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesProperly n H C₁ C₂

Build a properly separating hyperplane from EReal inf/sup inequalities (Theorem 11.1).

theorem exists_hyperplaneSeparatesProperly_iff (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) (hC₁ : C₁.Nonempty) (hC₂ : C₂.Nonempty) : (∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesProperly n H C₁ C₂) ↔ ∃ (b : Fin n → ℝ), sInf ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b)) '' C₁) ≥ sSup ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b)) '' C₂) ∧ sSup ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b)) '' C₁) > sInf ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b)) '' C₂)

Theorem 11.1: Let C₁ and C₂ be non-empty sets in ℝ^n.

There exists a hyperplane separating C₁ and C₂ properly if and only if there exists a vector b such that:

(a) inf {⟪x, b⟫ | x ∈ C₁} ≥ sup {⟪x, b⟫ | x ∈ C₂}, (b) sup {⟪x, b⟫ | x ∈ C₁} > inf {⟪x, b⟫ | x ∈ C₂}.

There exists a hyperplane separating C₁ and C₂ strongly if and only if there exists a vector b such that:

(c) inf {⟪x, b⟫ | x ∈ C₁} > sup {⟪x, b⟫ | x ∈ C₂}.

theorem exists_hyperplaneSeparatesStrongly_iff (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) (hC₁ : C₁.Nonempty) (hC₂ : C₂.Nonempty) : (∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesStrongly n H C₁ C₂) ↔ ∃ (b : Fin n → ℝ), sInf ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b)) '' C₁) > sSup ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b)) '' C₂)

Theorem 11.1 (strong separation): Let C₁ and C₂ be non-empty sets in ℝ^n. There exists a hyperplane separating C₁ and C₂ strongly if and only if there exists a vector b such that inf {⟪x, b⟫ | x ∈ C₁} > sup {⟪x, b⟫ | x ∈ C₂}.

theorem image_mkQ_affineSubspace_eq_singleton {n : ℕ} (M : AffineSubspace ℝ (Fin n → ℝ)) {m0 : Fin n → ℝ} (hm0 : m0 ∈ M) : ⇑M.direction.mkQ '' ↑M = {M.direction.mkQ m0}

The quotient map mkQ collapses an affine subspace to a singleton in the quotient.

theorem quotient_point_not_mem_image_of_disjoint {n : ℕ} {C : Set (Fin n → ℝ)} (M : AffineSubspace ℝ (Fin n → ℝ)) {m0 : Fin n → ℝ} (hm0 : m0 ∈ M) (hCM : Disjoint C ↑M) : M.direction.mkQ m0 ∉ ⇑M.direction.mkQ '' C

Disjointness forces the distinguished quotient point mkQ m0 (with m0 ∈ M) to lie outside mkQ '' C.

theorem exists_strictSep_point_of_not_mem_affineSpan {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsModuleTopology ℝ E] {S : Set E} (hS : S.Nonempty) {x0 : E} (hx0 : x0 ∉ affineSpan ℝ S) : ∃ (f : StrongDual ℝ E), ∀ x ∈ S, f x < f x0

If x₀ lies outside the affine span of a nonempty set S, there is a continuous linear functional which is constant on affineSpan ℝ S and strictly separates x₀ from S.

theorem isOpen_translate_in_direction_of_relOpen {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsModuleTopology ℝ E] {C : Set E} (hCrelopen : ∃ (U : Set E), IsOpen U ∧ C = U ∩ ↑(affineSpan ℝ C)) {c0 : E} (hc0 : c0 ∈ C) : IsOpen {v : ↥(affineSpan ℝ C).direction | ↑v + c0 ∈ C}

If C is relatively open in its affine span, then translating by a point c0 ∈ C yields an open subset of the direction submodule (affineSpan ℝ C).direction.

theorem isOpen_image_direction_mkQ_of_isOpen {n : ℕ} (C : Set (Fin n → ℝ)) (D : Submodule ℝ (Fin n → ℝ)) : let Q := (Fin n → ℝ) ⧸ D; let π := D.mkQ; have V0 := (affineSpan ℝ C).direction; let f0 := π ∘ₗ V0.subtype; let V := Submodule.map π V0; ∀ (O : Set ↥V0), IsOpen O → IsOpen ((fun (v : ↥V0) => ⟨f0 v, ⋯⟩) '' O)

If O is open in the direction submodule V0, then its image in the mapped direction Submodule.map π V0 is open. This is the key topological step in the hard case of Theorem 11.2.