def IsAffineSet (n : ℕ) (M : Set (Fin n → ℝ)) : Prop

Text 1.1: A subset M of Real^n is affine if for all x, y ∈ M and all r : Real, (1 - r) • x + r • y is in M.

theorem lineMap_mem_of_isAffineSet {n : ℕ} {M : Set (Fin n → ℝ)} (hM : IsAffineSet n M) {x y : Fin n → ℝ} (hx : x ∈ M) (hy : y ∈ M) (r : ℝ) : (AffineMap.lineMap x y) r ∈ M

Affine combinations of two points in an affine set are in the set, written as a line map.

theorem affine_combo_three_as_double_lineMap {n : ℕ} (c : ℝ) (x y z : Fin n → ℝ) : c • (x - y) + z = (AffineMap.lineMap ((AffineMap.lineMap z x) (2 * c)) ((AffineMap.lineMap z y) (-2 * c))) (1 / 2)

A three-point affine combination as a line map of two line maps.

theorem smul_sub_add_mem_of_isAffineSet {n : ℕ} {M : Set (Fin n → ℝ)} (hM : IsAffineSet n M) {x y z : Fin n → ℝ} (hx : x ∈ M) (hy : y ∈ M) (hz : z ∈ M) (c : ℝ) : c • (x - y) + z ∈ M

An affine set is closed under expressions of the form c • (x - y) + z.

theorem isAffineSet_iff_affineSubspace (n : ℕ) (M : Set (Fin n → ℝ)) : IsAffineSet n M ↔ ∃ (s : AffineSubspace ℝ (Fin n → ℝ)), ↑s = M

Helper lemma: an affine set is the carrier of some affine subspace.

theorem isAffineSet_of_submodule (n : ℕ) (S : Submodule ℝ (Fin n → ℝ)) : IsAffineSet n ↑S

Submodules are affine sets.

theorem affineSet_smul_closed_of_origin {n : ℕ} {M : Set (Fin n → ℝ)} (hM : IsAffineSet n M) (h0 : 0 ∈ M) (x : Fin n → ℝ) : x ∈ M → ∀ (r : ℝ), r • x ∈ M

An affine set containing the origin is closed under scalar multiplication.

theorem affineSet_add_closed_of_origin {n : ℕ} {M : Set (Fin n → ℝ)} (hM : IsAffineSet n M) (h0 : 0 ∈ M) (x : Fin n → ℝ) : x ∈ M → ∀ y ∈ M, x + y ∈ M

An affine set containing the origin is closed under addition.

theorem submodule_of_affineSet_origin (n : ℕ) (M : Set (Fin n → ℝ)) (hM : IsAffineSet n M) (h0 : 0 ∈ M) : ∃ (S : Submodule ℝ (Fin n → ℝ)), ↑S = M

An affine set containing the origin is the carrier of a submodule.

theorem subspace_iff_affineSet_and_origin (n : ℕ) (M : Set (Fin n → ℝ)) : (∃ (S : Submodule ℝ (Fin n → ℝ)), ↑S = M) ↔ IsAffineSet n M ∧ 0 ∈ M

Theorem 1.1: The subspaces of Real^n are exactly the affine sets which contain the origin.

def SetTranslate (n : ℕ) (M : Set (Fin n → ℝ)) (a : Fin n → ℝ) : Set (Fin n → ℝ)

Text 1.2: For M ⊆ Real^n and a ∈ Real^n, the translate of M by a is the set M + a = {x + a | x ∈ M}.

theorem translate_affine_combo {n : ℕ} (x y a : Fin n → ℝ) (r : ℝ) : (1 - r) • (x + a) + r • (y + a) = (1 - r) • x + r • y + a

Translation commutes with affine combinations.

theorem isAffineSet_translate (n : ℕ) (M : Set (Fin n → ℝ)) (a : Fin n → ℝ) : IsAffineSet n M → IsAffineSet n (SetTranslate n M a)

Text 1.2.1: If M ⊆ Real^n is affine and a ∈ Real^n, then the translate a + M is an affine set.

def IsParallelAffineSet (n : ℕ) (M L : Set (Fin n → ℝ)) : Prop

Text 1.3: An affine set M is parallel to an affine set L if M = L + a for some a.

theorem setTranslate_eq_sub_single (n : ℕ) (M : Set (Fin n → ℝ)) (y : Fin n → ℝ) : SetTranslate n M (-y) = {x : Fin n → ℝ | ∃ a ∈ M, x = a - y}

Translating by -y gives the set of differences with y.

theorem setTranslate_submodule_eq_self (n : ℕ) (L : Submodule ℝ (Fin n → ℝ)) (v : Fin n → ℝ) (hv : v ∈ L) : SetTranslate n (↑L) v = ↑L

Translating a submodule by one of its elements gives the same set.

theorem parallel_submodule_unique (n : ℕ) (M : Set (Fin n → ℝ)) (L1 L2 : Submodule ℝ (Fin n → ℝ)) (h1 : IsParallelAffineSet n M ↑L1) (h2 : IsParallelAffineSet n M ↑L2) : L1 = L2

Parallel submodules to the same affine set are equal.

theorem parallel_submodule_unique_of_affine (n : ℕ) (M : Set (Fin n → ℝ)) : IsAffineSet n M → M.Nonempty → ∃! L : Submodule ℝ (Fin n → ℝ), IsParallelAffineSet n M ↑L ∧ ↑L = {x : Fin n → ℝ | ∃ a ∈ M, ∃ b ∈ M, x = a - b}

Theorem 1.2: Each non-empty affine set M is parallel to a unique subspace L; this L is given by L = M - M = {x - y | x ∈ M, y ∈ M}.

noncomputable def affineSetDim (n : ℕ) (M : Set (Fin n → ℝ)) (hM : IsAffineSet n M) : ℤ

Text 1.4: The dimension of a non-empty affine set is defined as the dimension of the subspace parallel to it. (The dimension of ∅ is -1 by convention.)

def IsPoint (n : ℕ) (M : Set (Fin n → ℝ)) : Prop

Text 1.5: An affine set of dimension 0 is called a point.

def IsLine (n : ℕ) (M : Set (Fin n → ℝ)) : Prop

Text 1.5: An affine set of dimension 1 is called a line.

def IsPlane (n : ℕ) (M : Set (Fin n → ℝ)) : Prop

Text 1.5: An affine set of dimension 2 is called a plane.

def IsHyperplane (n : ℕ) (M : Set (Fin n → ℝ)) : Prop

Text 1.5: An (n - 1)-dimensional affine set in Real^n is called a hyperplane.

def orthogonalComplement (n : ℕ) (L : Submodule ℝ (Fin n → ℝ)) : Submodule ℝ (Fin n → ℝ)

Text 1.6: Given a subspace L of Real^n, the orthogonal complement L^⊥ is the set of vectors x such that x ⟂ y for every y ∈ L.

def dotProductLinear (n : ℕ) (b : Fin n → ℝ) : Module.Dual ℝ (Fin n → ℝ)

The linear functional x ↦ x ⬝ᵥ b.

theorem dotProductLinear_ker_eq (n : ℕ) (b : Fin n → ℝ) : ↑(LinearMap.ker (dotProductLinear n b)) = {x : Fin n → ℝ | x ⬝ᵥ b = 0}

The kernel of dotProductLinear is the zero dot-product set.

theorem dotProductLinear_ne_zero (n : ℕ) {b : Fin n → ℝ} (hb : b ≠ 0) : dotProductLinear n b ≠ 0

A nonzero vector gives a nonzero dot-product functional.

theorem dual_eq_dotProductLinear (n : ℕ) (f : Module.Dual ℝ (Fin n → ℝ)) (hf : f ≠ 0) : ∃ (b : Fin n → ℝ), b ≠ 0 ∧ f = dotProductLinear n b

Any nonzero linear functional on Fin n → ℝ is a dot-product functional.

theorem dotProduct_levelset_isAffine (n : ℕ) (β : ℝ) (b : Fin n → ℝ) : IsAffineSet n {x : Fin n → ℝ | x ⬝ᵥ b = β}

A dot-product level set is affine.

theorem exists_point_and_translate_kernel (n : ℕ) (β : ℝ) (b : Fin n → ℝ) (hb : b ≠ 0) : ∃ (x0 : Fin n → ℝ), x0 ⬝ᵥ b = β ∧ {x : Fin n → ℝ | x ⬝ᵥ b = β} = SetTranslate n {x : Fin n → ℝ | x ⬝ᵥ b = 0} x0

A nonzero normal gives a point on the level set and a translation by the kernel.

theorem finrank_kernel_dotProduct (n : ℕ) (b : Fin n → ℝ) (hb : b ≠ 0) : Module.finrank ℝ ↥(LinearMap.ker (dotProductLinear n b)) = n - 1

The kernel of a nonzero dot-product functional has dimension n - 1.

theorem codim_one_submodule_eq_dotProduct (n : ℕ) (L : Submodule ℝ (Fin n → ℝ)) (hL : Module.finrank ℝ ↥L = n - 1) (hn : 0 < n) : ∃ (b : Fin n → ℝ), b ≠ 0 ∧ ↑L = {x : Fin n → ℝ | x ⬝ᵥ b = 0}

Codimension-one submodules are dot-product kernels.

theorem hyperplane_kernels_eq (n : ℕ) (b b' : Fin n → ℝ) (β β' : ℝ) (x0 : Fin n → ℝ) (hx0 : x0 ⬝ᵥ b = β) (hH : {x : Fin n → ℝ | x ⬝ᵥ b = β} = {x : Fin n → ℝ | x ⬝ᵥ b' = β'}) : {x : Fin n → ℝ | x ⬝ᵥ b = 0} = {x : Fin n → ℝ | x ⬝ᵥ b' = 0}

Equality of dot-product level sets gives equality of the zero-level kernels.

theorem linear_functional_eq_smul_of_ker_eq (n : ℕ) (f g : Module.Dual ℝ (Fin n → ℝ)) (hf : f ≠ 0) (hg : g ≠ 0) (hker : LinearMap.ker f = LinearMap.ker g) : ∃ (c : ℝ), c ≠ 0 ∧ g = c • f

Nonzero linear functionals with the same kernel are scalar multiples.

theorem hyperplane_normal_unique (n : ℕ) (b b' : Fin n → ℝ) (β β' : ℝ) (hb : b ≠ 0) (hb' : b' ≠ 0) (hH : {x : Fin n → ℝ | x ⬝ᵥ b = β} = {x : Fin n → ℝ | x ⬝ᵥ b' = β'}) : ∃ (c : ℝ), c ≠ 0 ∧ b' = c • b ∧ β' = c * β

If two nonzero normals define the same hyperplane, they are scalar multiples.

theorem hyperplane_iff_eq_dotProduct (n : ℕ) (hn : 0 < n) : (∀ (β : ℝ) (b : Fin n → ℝ), b ≠ 0 → IsHyperplane n {x : Fin n → ℝ | x ⬝ᵥ b = β}) ∧ ∀ (H : Set (Fin n → ℝ)), IsHyperplane n H → ∃ (b : Fin n → ℝ) (β : ℝ), b ≠ 0 ∧ H = {x : Fin n → ℝ | x ⬝ᵥ b = β} ∧ ∀ (b' : Fin n → ℝ) (β' : ℝ), b' ≠ 0 → H = {x : Fin n → ℝ | x ⬝ᵥ b' = β'} → ∃ (c : ℝ), c ≠ 0 ∧ b' = c • b ∧ β' = c * β

Theorem 1.3: Given β : Real and non-zero b : Real^n, the set {x | ⟪x, b⟫ = β} is a hyperplane in Real^n. Moreover, every hyperplane admits such a representation, with b and β unique up to a common non-zero multiple.

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

Text 1.7: In Theorem 1.3, the vector b is called a normal to the hyperplane H.

def affineHull (n : ℕ) (S : Set (Fin n → ℝ)) : Set (Fin n → ℝ)

Text 1.8: For any S ⊆ R^n there is a unique smallest affine set containing S, namely the intersection of all affine sets containing S. This set is called the affine hull of S and is denoted aff S.

theorem affineHull_subset_of_affineSet {n : ℕ} {S M : Set (Fin n → ℝ)} (hM : IsAffineSet n M) (hS : S ⊆ M) : affineHull n S ⊆ M

The affine hull is contained in any affine set that contains S.

theorem isAffineSet_affineHull (n : ℕ) (S : Set (Fin n → ℝ)) : IsAffineSet n (affineHull n S)

The affine hull of a set is itself affine.

theorem affineHull_mem_affineSets (n : ℕ) (S : Set (Fin n → ℝ)) : affineHull n S ∈ {M : Set (Fin n → ℝ) | IsAffineSet n M ∧ S ⊆ M}

The affine hull is an affine set containing S.

theorem affineHull_eq_sInter_affineSets (n : ℕ) (S : Set (Fin n → ℝ)) : affineHull n S = ⋂₀ {M : Set (Fin n → ℝ) | IsAffineSet n M ∧ S ⊆ M}

Text 1.8: The affine hull is the intersection of all affine sets containing S.

theorem affineCombination_eq_linear_combination_univ {n m : ℕ} (xs : Fin m → Fin n → ℝ) (w : Fin m → ℝ) (hw : ∑ i : Fin m, w i = 1) : (Finset.affineCombination ℝ Finset.univ xs) w = ∑ i : Fin m, w i • xs i

On Fin m, an affine combination with total weight 1 is just the sum of smuls.

theorem affineSpan_mono_range {n m : ℕ} {S : Set (Fin n → ℝ)} (xs : Fin m → Fin n → ℝ) (hxs : ∀ (i : Fin m), xs i ∈ S) : affineSpan ℝ (Set.range xs) ≤ affineSpan ℝ S

If all points of a family lie in S, then the affine span of its range is contained in the affine span of S.

theorem exists_fin_family_of_finset_affineCombination {n : ℕ} {S : Set (Fin n → ℝ)} {v : Fin n → ℝ} (fs : Finset { x : Fin n → ℝ // x ∈ S }) (w : { x : Fin n → ℝ // x ∈ S } → ℝ) (hw : ∑ i ∈ fs, w i = 1) (hv : v = (Finset.affineCombination ℝ fs fun (x : { x : Fin n → ℝ // x ∈ S }) => ↑x) w) : ∃ (m : ℕ) (xs : Fin m → Fin n → ℝ) (coeffs : Fin m → ℝ), (∀ (i : Fin m), xs i ∈ S) ∧ ∑ i : Fin m, coeffs i = 1 ∧ ∑ i : Fin m, coeffs i • xs i = v

Reindex a finset affine combination into a Fin m-indexed one.

theorem mem_affineHull_iff_finset_affineCombination (n : ℕ) (S : Set (Fin n → ℝ)) (v : Fin n → ℝ) : v ∈ affineHull n S ↔ ∃ (m : ℕ) (xs : Fin m → Fin n → ℝ) (coeffs : Fin m → ℝ), (∀ (i : Fin m), xs i ∈ S) ∧ ∑ i : Fin m, coeffs i = 1 ∧ ∑ i : Fin m, coeffs i • xs i = v

Text 1.8.1: aff S consists of all vectors of the form λ₁ x₁ + ⋯ + λₘ xₘ with xᵢ ∈ S and λ₁ + ⋯ + λₘ = 1.

theorem isAffineSet_mulVec_eq (m n : ℕ) (b : Fin m → ℝ) (B : Matrix (Fin m) (Fin n) ℝ) : IsAffineSet n {x : Fin n → ℝ | B.mulVec x = b}

A fiber of a matrix mulVec map is an affine set.

theorem translate_eq_linear_fiber {n m : ℕ} (L : Submodule ℝ (Fin n → ℝ)) (a : Fin n → ℝ) (f : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (hker : LinearMap.ker f = L) : SetTranslate n (↑L) a = {x : Fin n → ℝ | f x = f a}

A translate of a submodule is a fiber of a linear map with that kernel.

theorem exists_linearMap_with_ker (n : ℕ) (L : Submodule ℝ (Fin n → ℝ)) : ∃ (m : ℕ) (f : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ), LinearMap.ker f = L

Any submodule is the kernel of a linear map to Fin m → Real.

theorem linearMap_toMatrix_mulVec {m n : ℕ} (f : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (x : Fin n → ℝ) : ((LinearMap.toMatrix (Pi.basisFun ℝ (Fin n)) (Pi.basisFun ℝ (Fin m))) f).mulVec x = f x

The matrix of a linear map acts by mulVec in the standard basis.