Rockafellar, §1: Affine Sets

Affine sets in ℝⁿ: the unique subspace each is parallel to, dimension, hyperplanes and the linear systems whose solution sets affine sets are, and affine transformations. All 8 numbered results of §1 are formalized. The content is linear algebra, so §1 specialises almost nothing from the backbone and is closed by Mathlib's affine-space and inner-product API.

Main definitions

• IsAffineSet M — (1-λ)x + λy ∈ M for all x, y ∈ M and all λ ∈ ℝ. Bridged to Mathlib by isAffineSet_iff_coe_affineSpan and IsAffineSet.toAffineSubspace, and to Submodule by IsAffineSet.toSubmodule when M contains the origin.
• dim S — the dimension of the subspace parallel to aff S. It is ℤ-valued because Rockafellar's convention is dim ∅ = -1; dim_eq_finrank_direction identifies it with the finrank of the direction otherwise. Later sections use this definition.
• IsHyperplane — an affine set of dimension n - 1.
• IsAffineMap — the book's affine transformation.

The converse half of theorem_1_3 carries 0 < n, which the book does not: in ℝ⁰ the empty set has dimension -1 = n - 1 and so is a hyperplane, yet there is no non-zero b ∈ ℝ⁰ to represent it with. For n ≥ 1 the hypothesis is vacuous, and corollary_1_4_1 needs none. Theorem 1.4's B is a linear map ℝⁿ →ₗ[ℝ] ℝᵐ rather than an m × n matrix; the row decomposition the book writes is what corollary_1_4_1 makes explicit, through a basis of L⊥.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §1.

Affine sets

def Rockafellar.IsAffineSet {n : ℕ} (M : Set (TdafSurface.Rn n)) : Prop

Rockafellar's affine set: M ⊆ ℝⁿ such that (1 - λ)x + λy ∈ M whenever x ∈ M, y ∈ M and λ ∈ ℝ.

Equations

• Rockafellar.IsAffineSet M = ∀ ⦃x : TdafSurface.Rn n⦄, x ∈ M → ∀ ⦃y : TdafSurface.Rn n⦄, y ∈ M → ∀ (l : ℝ), (1 - l) • x + l • y ∈ M

theorem Rockafellar.isAffineSet_coe {n : ℕ} (M : AffineSubspace ℝ (TdafSurface.Rn n)) : IsAffineSet ↑M

The underlying set of an AffineSubspace is an affine set.

theorem Rockafellar.mem_add_singleton {n : ℕ} {s : Set (TdafSurface.Rn n)} {a z : TdafSurface.Rn n} : z ∈ s + {a} ↔ z - a ∈ s

Membership in a translate, unfolded.

theorem Rockafellar.IsAffineSet.add_singleton {n : ℕ} {M : Set (TdafSurface.Rn n)} (h : IsAffineSet M) (a : TdafSurface.Rn n) : IsAffineSet (M + {a})

A translate of an affine set is affine.

def Rockafellar.IsAffineSet.toSubmodule {n : ℕ} {M : Set (TdafSurface.Rn n)} (h : IsAffineSet M) (h0 : 0 ∈ M) : Submodule ℝ (TdafSurface.Rn n)

Rockafellar's proof of Theorem 1.1: an affine set containing the origin is a subspace. This packages it as a Submodule.

Equations

• h.toSubmodule h0 = { carrier := M, add_mem' := ⋯, zero_mem' := h0, smul_mem' := ⋯ }

@[simp]

theorem Rockafellar.IsAffineSet.coe_toSubmodule {n : ℕ} {M : Set (TdafSurface.Rn n)} (h : IsAffineSet M) (h0 : 0 ∈ M) : ↑(h.toSubmodule h0) = M

The carrier of IsAffineSet.toSubmodule is the set it came from.

theorem Rockafellar.theorem_1_1 {n : ℕ} (M : Set (TdafSurface.Rn n)) : (∃ (L : Submodule ℝ (TdafSurface.Rn n)), ↑L = M) ↔ IsAffineSet M ∧ 0 ∈ M

Theorem 1.1. The subspaces of ℝⁿ are the affine sets which contain the origin.

def Rockafellar.IsAffineSet.toAffineSubspace {n : ℕ} {M : Set (TdafSurface.Rn n)} (h : IsAffineSet M) : AffineSubspace ℝ (TdafSurface.Rn n)

An affine set is the underlying set of an AffineSubspace.

Equations

• h.toAffineSubspace = { carrier := M, smul_vsub_vadd_mem' := ⋯ }

@[simp]

theorem Rockafellar.IsAffineSet.coe_toAffineSubspace {n : ℕ} {M : Set (TdafSurface.Rn n)} (h : IsAffineSet M) : ↑h.toAffineSubspace = M

The carrier of IsAffineSet.toAffineSubspace is the set it came from.

theorem Rockafellar.isAffineSet_iff_coe_affineSpan {n : ℕ} (M : Set (TdafSurface.Rn n)) : IsAffineSet M ↔ ↑(affineSpan ℝ M) = M

The bridge to Mathlib. A subset of ℝⁿ is affine in Rockafellar's sense exactly when it is its own affine hull.

Translates of subspaces, and Theorem 1.2

theorem Rockafellar.coe_mk'_eq {n : ℕ} (L : Submodule ℝ (TdafSurface.Rn n)) (a : TdafSurface.Rn n) : ↑(AffineSubspace.mk' a L) = ↑L + {a}

A translate of a subspace is the affine subspace through a in that direction.

theorem Rockafellar.isAffineSet_coe_add_singleton {n : ℕ} (L : Submodule ℝ (TdafSurface.Rn n)) (a : TdafSurface.Rn n) : IsAffineSet (↑L + {a})

A translate of a subspace is an affine set.

theorem Rockafellar.vectorSpan_coe_add_singleton {n : ℕ} (L : Submodule ℝ (TdafSurface.Rn n)) (a : TdafSurface.Rn n) : vectorSpan ℝ (↑L + {a}) = L

The direction of a translate of a subspace is that subspace.

theorem Rockafellar.eq_vectorSpan_add_singleton {n : ℕ} {M : Set (TdafSurface.Rn n)} (h : IsAffineSet M) {a : TdafSurface.Rn n} (ha : a ∈ M) : M = ↑(vectorSpan ℝ M) + {a}

A non-empty affine set is the translate of its direction by any one of its points. This is the existence half of Theorem 1.2, phrased through Mathlib's vectorSpan.

theorem Rockafellar.theorem_1_2 {n : ℕ} {M : Set (TdafSurface.Rn n)} (h : IsAffineSet M) (hne : M.Nonempty) : ∃! L : Submodule ℝ (TdafSurface.Rn n), ∃ (a : TdafSurface.Rn n), M = ↑L + {a}

Theorem 1.2. Each non-empty affine set M is parallel to a unique subspace L, that is, M = L + a for some a. The witness is vectorSpan ℝ M; theorem_1_2_sub identifies it with M - M.

theorem Rockafellar.theorem_1_2_sub {n : ℕ} {M : Set (TdafSurface.Rn n)} {L : Submodule ℝ (TdafSurface.Rn n)} {a : TdafSurface.Rn n} (hL : M = ↑L + {a}) : ↑L = M - M

Theorem 1.2, second sentence: a subspace parallel to M is M - M.

Dimension

noncomputable def Rockafellar.dim {n : ℕ} (S : Set (TdafSurface.Rn n)) : ℤ

Rockafellar's dimension of a subset of ℝⁿ: the dimension of the subspace parallel to its affine hull, with the convention dim ∅ = -1. It is therefore ℤ-valued.

For an affine set this is the dimension of the parallel subspace of Theorem 1.2, and for a convex set it is the dimension of aff C (§2).

Equations

• Rockafellar.dim S = ↑(Module.finrank ℝ ↥(vectorSpan ℝ S)) - if S = ∅ then 1 else 0

@[simp]

theorem Rockafellar.dim_empty {n : ℕ} : dim ∅ = -1

Rockafellar's convention: the empty set has dimension -1.

theorem Rockafellar.dim_of_nonempty {n : ℕ} {S : Set (TdafSurface.Rn n)} (h : S.Nonempty) : dim S = ↑(Module.finrank ℝ ↥(vectorSpan ℝ S))

On a non-empty set dim is the finrank of the direction.

theorem Rockafellar.dim_eq_finrank_direction {n : ℕ} {S : Set (TdafSurface.Rn n)} (h : S.Nonempty) : dim S = ↑(Module.finrank ℝ ↥(affineSpan ℝ S).direction)

On a non-empty set dim is the finrank of the direction of the affine hull.

theorem Rockafellar.vectorSpan_coe_submodule {n : ℕ} (L : Submodule ℝ (TdafSurface.Rn n)) : vectorSpan ℝ ↑L = L

The direction of a subspace, as a set, is the subspace itself — Theorem 1.1 in the form dim needs it.

@[simp]

theorem Rockafellar.dim_coe_submodule {n : ℕ} (L : Submodule ℝ (TdafSurface.Rn n)) : dim ↑L = ↑(Module.finrank ℝ ↥L)

The dimension of a subspace is its finrank.

@[simp]

theorem Rockafellar.dim_coe_add_singleton {n : ℕ} (L : Submodule ℝ (TdafSurface.Rn n)) (a : TdafSurface.Rn n) : dim (↑L + {a}) = ↑(Module.finrank ℝ ↥L)

The dimension of a translate of a subspace is the finrank of that subspace.

theorem Rockafellar.dim_le_dim_of_subset {n : ℕ} {S T : Set (TdafSurface.Rn n)} (hne : S.Nonempty) (hST : S ⊆ T) : dim S ≤ dim T

dim is monotone.

@[simp]

theorem Rockafellar.dim_univ {n : ℕ} : dim Set.univ = ↑n

dim ℝⁿ = n.

theorem Rockafellar.vectorSpan_eq_span_of_zero_mem {n : ℕ} {S : Set (TdafSurface.Rn n)} (h0 : 0 ∈ S) : vectorSpan ℝ S = Submodule.span ℝ S

Theorem 1.1 in the form §2's Theorem 2.7 needs it: for a set containing the origin, the direction of the affine hull is the linear span.

theorem Rockafellar.coe_affineSpan_of_zero_mem {n : ℕ} {S : Set (TdafSurface.Rn n)} (h0 : 0 ∈ S) : ↑(affineSpan ℝ S) = ↑(Submodule.span ℝ S)

Theorem 1.1: for a set containing the origin, the affine hull is the linear span.

Hyperplanes: Theorem 1.3

def Rockafellar.IsHyperplane {n : ℕ} (H : Set (TdafSurface.Rn n)) : Prop

Rockafellar's hyperplane: an (n-1)-dimensional affine set in ℝⁿ.

Equations

• Rockafellar.IsHyperplane H = (Rockafellar.IsAffineSet H ∧ Rockafellar.dim H = ↑n - 1)

theorem Rockafellar.sub_mem_orthogonal_span_singleton_iff {n : ℕ} (b x a : TdafSurface.Rn n) : x - a ∈ (ℝ ∙ b)ᗮ ↔ ((TdafSurface.pairing n) x) b = ((TdafSurface.pairing n) a) b

x - a ⊥ b says exactly that x and a have the same pairing against b.

theorem Rockafellar.setOf_pairing_eq {n : ℕ} (b : TdafSurface.Rn n) (hb : b ≠ 0) (β : ℝ) : {x : TdafSurface.Rn n | ((TdafSurface.pairing n) x) b = β} = ↑(ℝ ∙ b)ᗮ + {(β / ‖b‖ ^ 2) • b}

The level set ⟨·, b⟩ = β is the translate of (ℝb)ᗮ through (β/‖b‖²)b.

theorem Rockafellar.finrank_orthogonal_span_singleton_add_one {n : ℕ} (b : TdafSurface.Rn n) (hb : b ≠ 0) : Module.finrank ℝ ↥(ℝ ∙ b)ᗮ + 1 = n

The orthogonal complement of a line has dimension n - 1.

theorem Rockafellar.theorem_1_3 {n : ℕ} (b : TdafSurface.Rn n) (hb : b ≠ 0) (β : ℝ) : IsHyperplane {x : TdafSurface.Rn n | ((TdafSurface.pairing n) x) b = β}

Theorem 1.3, first sentence. Given β ∈ ℝ and a non-zero b ∈ ℝⁿ, the set H = {x | ⟨x, b⟩ = β} is a hyperplane in ℝⁿ.

theorem Rockafellar.theorem_1_3_exists {n : ℕ} (hn : 0 < n) {H : Set (TdafSurface.Rn n)} (h : IsHyperplane H) : ∃ (b : TdafSurface.Rn n) (β : ℝ), b ≠ 0 ∧ H = {x : TdafSurface.Rn n | ((TdafSurface.pairing n) x) b = β}

Theorem 1.3, second sentence: every hyperplane is of that form.

The hypothesis 0 < n is not in the book, and is genuinely needed: in ℝ⁰ the empty set has dimension -1 = n - 1, so it is a hyperplane in Rockafellar's sense, yet there is no non-zero b ∈ ℝ⁰. For n ≥ 1 a hyperplane is automatically non-empty.

theorem Rockafellar.theorem_1_3_unique {n : ℕ} {b b' : TdafSurface.Rn n} {β β' : ℝ} (hb : b ≠ 0) (hb' : b' ≠ 0) (h : {x : TdafSurface.Rn n | ((TdafSurface.pairing n) x) b = β} = {x : TdafSurface.Rn n | ((TdafSurface.pairing n) x) b' = β'}) : ∃ (l : ℝ), l ≠ 0 ∧ b' = l • b ∧ β' = l * β

Theorem 1.3, third sentence: b and β are unique up to a common non-zero multiple.

Linear systems: Theorem 1.4 and Corollary 1.4.1

theorem Rockafellar.theorem_1_4 {m n : ℕ} (B : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m) (b : TdafSurface.Rn m) : IsAffineSet {x : TdafSurface.Rn n | B x = b}

Theorem 1.4, first sentence. Given b ∈ ℝᵐ and a linear B : ℝⁿ → ℝᵐ, the solution set {x | Bx = b} is an affine set in ℝⁿ. The book writes B as an m × n matrix; a linear map is the same data.

theorem Rockafellar.theorem_1_4_exists {n : ℕ} {M : Set (TdafSurface.Rn n)} (h : IsAffineSet M) : ∃ (k : ℕ) (B : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn k) (b : TdafSurface.Rn k), M = {x : TdafSurface.Rn n | B x = b}

Theorem 1.4, second sentence: every affine set is such a solution set. The empty set and ℝⁿ are covered, by degenerate choices of B.

theorem Rockafellar.pairing_sub_eq_zero_iff {n : ℕ} (u x a : TdafSurface.Rn n) : ((TdafSurface.pairing n) u) (x - a) = 0 ↔ ((TdafSurface.pairing n) x) u = ((TdafSurface.pairing n) a) u

u ⊥ (x - a) says exactly that x and a have the same pairing against u.

theorem Rockafellar.mem_orthogonal_span_iff {n : ℕ} {S : Set (TdafSurface.Rn n)} {v : TdafSurface.Rn n} : v ∈ (Submodule.span ℝ S)ᗮ ↔ ∀ u ∈ S, ((TdafSurface.pairing n) u) v = 0

Orthogonality to a spanning set is orthogonality to the span.

theorem Rockafellar.corollary_1_4_1 {n : ℕ} {M : Set (TdafSurface.Rn n)} (h : IsAffineSet M) : ∃ (k : ℕ) (H : Fin k → Set (TdafSurface.Rn n)), (∀ (i : Fin k), IsHyperplane (H i)) ∧ M = ⋂ (i : Fin k), H i

Corollary 1.4.1. Every affine subset of ℝⁿ is an intersection of a finite collection of hyperplanes.

ℝⁿ itself is the intersection of the empty collection; ∅ is the intersection of two parallel hyperplanes when n ≥ 1, and is itself the unique hyperplane of ℝ⁰.

Affine transformations: Theorems 1.5 and 1.6

def Rockafellar.IsAffineMap {m n : ℕ} (T : TdafSurface.Rn n → TdafSurface.Rn m) : Prop

Rockafellar's affine transformation: a map T : ℝⁿ → ℝᵐ with T((1-λ)x + λy) = (1-λ)Tx + λTy for all x, y and λ ∈ ℝ.

Equations

• Rockafellar.IsAffineMap T = ∀ (x y : TdafSurface.Rn n) (l : ℝ), T ((1 - l) • x + l • y) = (1 - l) • T x + l • T y

theorem Rockafellar.theorem_1_5 {m n : ℕ} (T : TdafSurface.Rn n → TdafSurface.Rn m) : IsAffineMap T ↔ ∃ (A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m) (a : TdafSurface.Rn m), ∀ (x : TdafSurface.Rn n), T x = A x + a

Theorem 1.5. The affine transformations from ℝⁿ to ℝᵐ are the mappings T of the form Tx = Ax + a with A linear and a ∈ ℝᵐ.

theorem Rockafellar.isAffineMap_linear_translate {m n : ℕ} (A : TdafSurface.Rn n ≃ₗ[ℝ] TdafSurface.Rn m) (c : TdafSurface.Rn n) (d : TdafSurface.Rn m) : IsAffineMap fun (x : TdafSurface.Rn n) => A (x - c) + d

x ↦ A(x - c) + d is an affine transformation.

theorem Rockafellar.bijective_linear_translate {m n : ℕ} (A : TdafSurface.Rn n ≃ₗ[ℝ] TdafSurface.Rn m) (c : TdafSurface.Rn n) (d : TdafSurface.Rn m) : Function.Bijective fun (x : TdafSurface.Rn n) => A (x - c) + d

x ↦ A(x - c) + d is a bijection when A is.

theorem Rockafellar.exists_linearEquiv_apply_eq {n : ℕ} {ι : Type} {v v' : ι → TdafSurface.Rn n} (hv : LinearIndependent ℝ v) (hv' : LinearIndependent ℝ v') : ∃ (A : TdafSurface.Rn n ≃ₗ[ℝ] TdafSurface.Rn n), ∀ (i : ι), A (v i) = v' i

Two linearly independent families with the same index set are carried onto each other by a linear automorphism of ℝⁿ.

theorem Rockafellar.theorem_1_6 {n k : ℕ} {b b' : Fin (k + 1) → TdafSurface.Rn n} (hb : AffineIndependent ℝ b) (hb' : AffineIndependent ℝ b') : ∃ (T : TdafSurface.Rn n → TdafSurface.Rn n), IsAffineMap T ∧ Function.Bijective T ∧ ∀ (i : Fin (k + 1)), T (b i) = b' i

Theorem 1.6. Two affinely independent sets of m + 1 points of ℝⁿ are carried onto each other, in order, by a one-to-one affine transformation of ℝⁿ onto itself.

theorem Rockafellar.theorem_1_6_unique {n : ℕ} {b : Fin (n + 1) → TdafSurface.Rn n} (hb : AffineIndependent ℝ b) {T₁ T₂ : TdafSurface.Rn n → TdafSurface.Rn n} (h₁ : IsAffineMap T₁) (h₂ : IsAffineMap T₂) (hT : ∀ (i : Fin (n + 1)), T₁ (b i) = T₂ (b i)) : T₁ = T₂

Theorem 1.6, last sentence: when the affinely independent set has n + 1 points, the transformation is unique.

theorem Rockafellar.image_linear_translate {m n : ℕ} (A : TdafSurface.Rn n ≃ₗ[ℝ] TdafSurface.Rn m) (S : Set (TdafSurface.Rn n)) (c : TdafSurface.Rn n) (d : TdafSurface.Rn m) : (fun (x : TdafSurface.Rn n) => A (x - c) + d) '' (S + {c}) = (fun (x : TdafSurface.Rn n) => A x) '' S + {d}

The image of a translate under x ↦ A(x - c) + d.

theorem Rockafellar.corollary_1_6_1 {n : ℕ} {M₁ M₂ : Set (TdafSurface.Rn n)} (h₁ : IsAffineSet M₁) (h₂ : IsAffineSet M₂) (hdim : dim M₁ = dim M₂) : ∃ (T : TdafSurface.Rn n → TdafSurface.Rn n), IsAffineMap T ∧ Function.Bijective T ∧ T '' M₁ = M₂

Corollary 1.6.1. Any two affine sets of ℝⁿ of the same dimension are carried onto each other by a one-to-one affine transformation of ℝⁿ onto itself.

The orthogonal complement of a graph

theorem Rockafellar.orthogonal_graph_eq_graph_neg_adjoint {m n : ℕ} (A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m) : {z : TdafSurface.Rn n × TdafSurface.Rn m | ∀ (w : TdafSurface.Rn n × TdafSurface.Rn m), w.2 = A w.1 → ((TdafSurface.pairingProd n m) w) z = 0} = {z : TdafSurface.Rn n × TdafSurface.Rn m | z.1 = -(LinearMap.adjoint A) z.2}

Rockafellar, §1, unnumbered. The graph of a linear transformation A : ℝⁿ → ℝᵐ is a subspace L of ℝⁿ⁺ᵐ, and its orthogonal complement L⊥ is the graph of -A*.

The book works in ℝⁿ⁺ᵐ; here the ambient space is the product ℝⁿ × ℝᵐ with the product pairing pairingProd, which is the same bilinear form under the obvious identification. This identity is not numbered in the book, but §22 depends on it.