theorem unitBall_eq_closedBall (n : ℕ) : {x : Fin n → ℝ | ‖x‖ ≤ 1} = Metric.closedBall 0 1

The closed unit ball {x | ‖x‖ ≤ 1} in Fin n → ℝ agrees with Metric.closedBall 0 1.

theorem smul_unitBall_eq_closedBall (n : ℕ) {r : ℝ} (hr : 0 ≤ r) : r • {x : Fin n → ℝ | ‖x‖ ≤ 1} = Metric.closedBall 0 r

Scalar multiples of the unit ball are the corresponding centered closed balls (for r ≥ 0).

theorem exists_mem_unitBall_and_dotProduct_pos {n : ℕ} {b : Fin n → ℝ} : b ≠ 0 → ∃ v ∈ {x : Fin n → ℝ | ‖x‖ ≤ 1}, 0 < v ⬝ᵥ b

Given b ≠ 0, there is a unit-ball vector whose dot product with b is positive.

theorem strictify_halfspace_le_of_thickening {n : ℕ} {S : Set (Fin n → ℝ)} {b : Fin n → ℝ} {β δ : ℝ} (hb0 : b ≠ 0) (hδ : 0 < δ) (hS : S + δ • {x : Fin n → ℝ | ‖x‖ ≤ 1} ⊆ {x : Fin n → ℝ | x ⬝ᵥ b ≤ β}) : S ⊆ {x : Fin n → ℝ | x ⬝ᵥ b < β}

If a δ-thickening of S is contained in a closed half-space {x | x ⬝ᵥ b ≤ β}, then S is contained in the corresponding open half-space {x | x ⬝ᵥ b < β} (for δ > 0).

theorem strictify_halfspace_ge_of_thickening {n : ℕ} {S : Set (Fin n → ℝ)} {b : Fin n → ℝ} {β δ : ℝ} (hb0 : b ≠ 0) (hδ : 0 < δ) (hS : S + δ • {x : Fin n → ℝ | ‖x‖ ≤ 1} ⊆ {x : Fin n → ℝ | β ≤ x ⬝ᵥ b}) : S ⊆ {x : Fin n → ℝ | β < x ⬝ᵥ b}

If a δ-thickening of S is contained in a closed half-space {x | β ≤ x ⬝ᵥ b}, then S is contained in the corresponding open half-space {x | β < x ⬝ᵥ b} (for δ > 0).

theorem midpoint_mem_add_smul_unitBall_of_norm_sub_le {n : ℕ} {x₁ x₂ : Fin n → ℝ} {ε : ℝ} (hε : 0 ≤ ε) (h : ‖x₁ - x₂‖ ≤ 2 * ε) : ∃ z ∈ {x₁} + ε • {x : Fin n → ℝ | ‖x‖ ≤ 1}, z ∈ {x₂} + ε • {x : Fin n → ℝ | ‖x‖ ≤ 1}

If ‖x₁ - x₂‖ ≤ 2ε, then the midpoint lies in both ε-thickenings of {x₁} and {x₂}.

theorem exists_eps_disjoint_thickenings_iff_sInf_norm_sub_pos (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) : (∃ (ε : ℝ), 0 < ε ∧ have B := {x : Fin n → ℝ | ‖x‖ ≤ 1}; Disjoint (C₁ + ε • B) (C₂ + ε • B)) ↔ 0 < sInf (Set.image2 (fun (x₁ x₂ : Fin n → ℝ) => ‖x₁ - x₂‖) C₁ C₂)

Disjointness of ε-thickenings is equivalent to positivity of the infimum of pairwise distances.

theorem exists_hyperplaneSeparatesStrongly_iff_exists_eps_disjoint_thickenings (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) (hC₁conv : Convex ℝ C₁) (hC₂conv : Convex ℝ C₂) : (∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesStrongly n H C₁ C₂) ↔ ∃ (ε : ℝ), 0 < ε ∧ have B := {x : Fin n → ℝ | ‖x‖ ≤ 1}; Disjoint (C₁ + ε • B) (C₂ + ε • B)

Strong separation is equivalent to disjointness of some ε-thickenings.

theorem image2_norm_sub_eq_image_dist_sub (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) : Set.image2 (fun (x₁ x₂ : Fin n → ℝ) => ‖x₁ - x₂‖) C₁ C₂ = (fun (z : Fin n → ℝ) => dist 0 z) '' (C₁ - C₂)

The distance-set between C₁ and C₂ is the image of dist 0 on C₁ - C₂.

theorem sInf_norm_sub_pos_iff_zero_not_mem_closure_sub (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) : 0 < sInf (Set.image2 (fun (x₁ x₂ : Fin n → ℝ) => ‖x₁ - x₂‖) C₁ C₂) ↔ 0 ∉ closure (C₁ - C₂)

Positivity of the infimum distance-set is equivalent to 0 ∉ closure (C₁ - C₂).

theorem exists_hyperplaneSeparatesStrongly_iff_inf_sub_norm_pos (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) (hC₁conv : Convex ℝ C₁) (hC₂conv : Convex ℝ C₂) : (∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesStrongly n H C₁ C₂) ↔ 0 < sInf (Set.image2 (fun (x₁ x₂ : Fin n → ℝ) => ‖x₁ - x₂‖) C₁ C₂)

Theorem 11.4: Let C₁ and C₂ be non-empty convex sets in ℝ^n. In order that there exist a hyperplane separating C₁ and C₂ strongly, it is necessary and sufficient that

inf { ‖x₁ - x₂‖ | x₁ ∈ C₁, x₂ ∈ C₂ } > 0,

in other words that 0 ∉ closure (C₁ - C₂).

theorem exists_hyperplaneSeparatesStrongly_iff_zero_not_mem_closure_sub (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) (hC₁conv : Convex ℝ C₁) (hC₂conv : Convex ℝ C₂) : (∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesStrongly n H C₁ C₂) ↔ 0 ∉ closure (C₁ - C₂)

Theorem 11.4 (closure form): Let C₁ and C₂ be non-empty convex sets in ℝ^n. There exists a hyperplane separating C₁ and C₂ strongly if and only if 0 ∉ closure (C₁ - C₂).

theorem zero_not_mem_sub_of_disjoint {E : Type u_1} [AddGroup E] {C₁ C₂ : Set E} (hdisj : Disjoint C₁ C₂) : 0 ∉ C₁ - C₂

Disjointness implies 0 ∉ (C₁ - C₂).

theorem recessionCone_neg_set_iff {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Set E) (y : E) : y ∈ (-C).recessionCone ↔ -y ∈ C.recessionCone

Recession directions of a negated set are the negations of recession directions.

theorem mem_recessionCone_preimage_linearEquiv_iff {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (φ : E ≃ₗ[ℝ] F) (C : Set F) (y : E) : y ∈ (⇑φ ⁻¹' C).recessionCone ↔ φ y ∈ C.recessionCone

Membership in a recession cone is preserved under preimages by linear equivalences.

theorem isClosed_sub_of_noCommonRecessionDirections (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) (hC₁closed : IsClosed C₁) (hC₂closed : IsClosed C₂) (hC₁conv : Convex ℝ C₁) (hC₂conv : Convex ℝ C₂) (hrec : ∀ (y : Fin n → ℝ), y ≠ 0 → y ∈ C₁.recessionCone → y ∈ C₂.recessionCone → False) : IsClosed (C₁ - C₂)

Under the recession-condition hypothesis, the Minkowski difference C₁ - C₂ is closed.

theorem exists_hyperplaneSeparatesStrongly_of_disjoint_closed_convex_noCommonRecessionDirections (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) (hC₁closed : IsClosed C₁) (hC₂closed : IsClosed C₂) (hC₁conv : Convex ℝ C₁) (hC₂conv : Convex ℝ C₂) (hdisj : Disjoint C₁ C₂) (hrec : ∀ (y : Fin n → ℝ), y ≠ 0 → y ∈ C₁.recessionCone → y ∈ C₂.recessionCone → False) : ∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesStrongly n H C₁ C₂

Corollary 11.4.1. Let C₁ and C₂ be non-empty disjoint closed convex sets in ℝ^n having no common directions of recession. Then there exists a hyperplane separating C₁ and C₂ strongly.

theorem recessionCone_subset_singleton_of_bounded_fin {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (hCbdd : Bornology.IsBounded C) : C.recessionCone ⊆ {0}

Bounded sets in Fin n → ℝ have only the zero recession direction.

theorem noCommonRecessionDirections_closure_of_bounded_side {n : ℕ} {C₁ C₂ : Set (Fin n → ℝ)} (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) (hbounded : Bornology.IsBounded C₁ ∨ Bornology.IsBounded C₂) (y : Fin n → ℝ) : y ≠ 0 → y ∈ (closure C₁).recessionCone → y ∈ (closure C₂).recessionCone → False

If one of two sets is bounded, then their closures have no common nonzero recession direction.

theorem hyperplaneSeparatesStrongly_mono_sets {n : ℕ} {H A₁ A₂ B₁ B₂ : Set (Fin n → ℝ)} (hH : HyperplaneSeparatesStrongly n H A₁ A₂) (hB₁ : B₁ ⊆ A₁) (hB₂ : B₂ ⊆ A₂) (hB₁ne : B₁.Nonempty) (hB₂ne : B₂.Nonempty) : HyperplaneSeparatesStrongly n H B₁ B₂

Strong hyperplane separation is monotone under shrinking the separated sets.

theorem exists_hyperplaneSeparatesStrongly_of_disjoint_closure_convex_of_bounded (n : ℕ) (C₁ C₂ : Set (Fin n → ℝ)) (hC₁ne : C₁.Nonempty) (hC₂ne : C₂.Nonempty) (hC₁conv : Convex ℝ C₁) (hC₂conv : Convex ℝ C₂) (hdisj : Disjoint (closure C₁) (closure C₂)) (hbounded : Bornology.IsBounded C₁ ∨ Bornology.IsBounded C₂) : ∃ (H : Set (Fin n → ℝ)), HyperplaneSeparatesStrongly n H C₁ C₂

Corollary 11.4.2. Let C₁ and C₂ be non-empty convex sets in ℝ^n whose closures are disjoint. If either set is bounded, there exists a hyperplane separating C₁ and C₂ strongly.

theorem isClosed_setOf_dotProduct_le {n : ℕ} (b : Fin n → ℝ) (β : ℝ) : IsClosed {x : Fin n → ℝ | x ⬝ᵥ b ≤ β}

A single dot-product inequality defines a closed half-space.

theorem convex_setOf_dotProduct_le {n : ℕ} (b : Fin n → ℝ) (β : ℝ) : Convex ℝ {x : Fin n → ℝ | x ⬝ᵥ b ≤ β}

A single dot-product inequality defines a convex half-space.

theorem setOf_forall_dotProduct_le_eq_iInter (n : ℕ) (I : Type u_1) (b : I → Fin n → ℝ) (β : I → ℝ) : {x : Fin n → ℝ | ∀ (i : I), x ⬝ᵥ b i ≤ β i} = ⋂ (i : I), {x : Fin n → ℝ | x ⬝ᵥ b i ≤ β i}

A system of dot-product inequalities is the intersection of the corresponding half-spaces.

theorem isClosed_and_convex_setOf_dotProduct_le (n : ℕ) (I : Type u_1) (b : I → Fin n → ℝ) (β : I → ℝ) : IsClosed {x : Fin n → ℝ | ∀ (i : I), x ⬝ᵥ b i ≤ β i} ∧ Convex ℝ {x : Fin n → ℝ | ∀ (i : I), x ⬝ᵥ b i ≤ β i}

Text 11.2.1: The solution set S of a system of weak linear inequalities ⟪x, b i⟫ ≤ β i (i.e. x ⬝ᵥ b i ≤ β i, for all i ∈ I) is a closed convex set.

def IsClosedHalfspace (n : ℕ) (H : Set (Fin n → ℝ)) : Prop

Text 11.3.1: Let C be a convex set in ℝ^n. A supporting half-space to C is a closed half-space which contains C and has a point of C in its boundary.

Equations

• IsClosedHalfspace n H = ∃ (b : Fin n → ℝ) (β : ℝ), b ≠ 0 ∧ (H = {x : Fin n → ℝ | x ⬝ᵥ b ≤ β} ∨ H = {x : Fin n → ℝ | β ≤ x ⬝ᵥ b})

def IsSupportingHalfspace (n : ℕ) (C H : Set (Fin n → ℝ)) : Prop

Text 11.3.1: Let C be a convex set in ℝ^n. A supporting half-space to C is a closed half-space which contains C and has a point of C in its boundary.

Equations

• IsSupportingHalfspace n C H = (Convex ℝ C ∧ IsClosedHalfspace n H ∧ C ⊆ H ∧ ∃ x ∈ C, x ∈ frontier H)

def IsSupportingHyperplane (n : ℕ) (C H : Set (Fin n → ℝ)) : Prop

Text 11.3.2: A supporting hyperplane to C is a hyperplane which is the boundary of a supporting half-space to C. Equivalently, a supporting hyperplane has the form H = {x | x ⬝ᵥ b = β} with b ≠ 0, such that x ⬝ᵥ b ≤ β for every x ∈ C and x ⬝ᵥ b = β for at least one x ∈ C.

Equations

• IsSupportingHyperplane n C H = ∃ (b : Fin n → ℝ) (β : ℝ), b ≠ 0 ∧ H = {x : Fin n → ℝ | x ⬝ᵥ b = β} ∧ (∀ x ∈ C, x ⬝ᵥ b ≤ β) ∧ ∃ x ∈ C, x ⬝ᵥ b = β

theorem direction_ne_top_of_ne_top_of_nonempty {n : ℕ} {A : AffineSubspace ℝ (Fin n → ℝ)} (hAne : (↑A).Nonempty) (hA : A ≠ ⊤) : A.direction ≠ ⊤

If a nonempty affine subspace is not ⊤, then its direction is a proper submodule.

theorem affineSubspace_subset_setOf_apply_eq_of_le_ker_direction {V : Type u_1} [AddCommGroup V] [Module ℝ V] (A : AffineSubspace ℝ V) {x0 : V} (hx0 : x0 ∈ A) (f : Module.Dual ℝ V) (hdir : A.direction ≤ LinearMap.ker f) : ↑A ⊆ {x : V | f x = f x0}

If a linear functional vanishes on the direction of an affine subspace, then it is constant on that affine subspace.

theorem empty_case_choose_nonzero_b {n : ℕ} (hn : 0 < n) : ∃ (b : Fin n → ℝ), b ≠ 0

In Fin n → ℝ with 0 < n, one can choose an explicit nonzero vector.

theorem exists_hyperplane_superset_affineSpan_of_affineSpan_ne_top (n : ℕ) (hn : 0 < n) (C : Set (Fin n → ℝ)) (hC : affineSpan ℝ C ≠ ⊤) : ∃ (b : Fin n → ℝ) (β : ℝ), b ≠ 0 ∧ C ⊆ {x : Fin n → ℝ | x ⬝ᵥ b = β} ∧ ↑(affineSpan ℝ C) ⊆ {x : Fin n → ℝ | x ⬝ᵥ b = β}

Text 11.3.3: If C is not n-dimensional (so that affineSpan ℝ C ≠ ⊤), then there exists a hyperplane containing (and hence extending) affineSpan ℝ C, and therefore containing all of C.

def IsNontrivialSupportingHyperplane (n : ℕ) (C H : Set (Fin n → ℝ)) : Prop

Text 11.3.4: We usually speak only of non-trivial supporting hyperplanes to C, i.e. those supporting hyperplanes H which do not contain C itself.

Equations

• IsNontrivialSupportingHyperplane n C H = (IsSupportingHyperplane n C H ∧ ¬C ⊆ H)

noncomputable def dotProduct_strongDual {n : ℕ} (b : Fin n → ℝ) : StrongDual ℝ (Fin n → ℝ)

The dot product with b as a continuous linear functional, viewed in the StrongDual.

Equations

• dotProduct_strongDual b = LinearMap.toContinuousLinearMap (IsLinearMap.mk' (fun (x : Fin n → ℝ) => x ⬝ᵥ b) ⋯)

@[simp]

theorem dotProduct_strongDual_apply {n : ℕ} (b x : Fin n → ℝ) : (dotProduct_strongDual b) x = x ⬝ᵥ b

theorem exists_strongDual_strict_sep_point_of_not_mem_isClosed_convex {n : ℕ} {a : Fin n → ℝ} {C : Set (Fin n → ℝ)} (hCconv : Convex ℝ C) (hCclosed : IsClosed C) (hCne : C.Nonempty) (ha : a ∉ C) : ∃ (l : StrongDual ℝ (Fin n → ℝ)), ∀ y ∈ C, l y < l a

If a ∉ C and C is a nonempty closed convex set in ℝ^n, then there exists a continuous linear functional that strictly separates a from C.