def IsAffineTransformation (n m : ℕ) (T : (Fin n → ℝ) → Fin m → ℝ) : Prop

Equations

• IsAffineTransformation n m T = ∀ (x y : Fin n → ℝ) (r : ℝ), T ((1 - r) • x + r • y) = (1 - r) • T x + r • T y

theorem isAffineTransformation_iff_exists_affineMap (n m : ℕ) (T : (Fin n → ℝ) → Fin m → ℝ) : IsAffineTransformation n m T ↔ ∃ (f : (Fin n → ℝ) →ᵃ[ℝ] Fin m → ℝ), ⇑f = T

Text 1.10 (mathlib): The book's notion is equivalent to an AffineMap after coercion.

theorem affineMap_decomp_point {n m : ℕ} (f : (Fin n → ℝ) →ᵃ[ℝ] Fin m → ℝ) (x : Fin n → ℝ) : f x = f.linear x + f 0

Decomposition of an affine map as a linear part plus a constant (pointwise).

theorem affineTransformation_exists_linearMap_add (n m : ℕ) (T : (Fin n → ℝ) → Fin m → ℝ) : IsAffineTransformation n m T → ∃ (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (a : Fin m → ℝ), ∀ (x : Fin n → ℝ), T x = A x + a

Any affine transformation has a linear part plus a constant vector.

theorem affineTransformation_of_linearMap_add (n m : ℕ) (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (a : Fin m → ℝ) : IsAffineTransformation n m fun (x : Fin n → ℝ) => A x + a

Any map of the form x ↦ A x + a is an affine transformation.

theorem affineTransformation_iff_eq_linearMap_add (n m : ℕ) (T : (Fin n → ℝ) → Fin m → ℝ) : IsAffineTransformation n m T ↔ ∃ (A : (Fin n → ℝ) →ₗ[ℝ] Fin m → ℝ) (a : Fin m → ℝ), ∀ (x : Fin n → ℝ), T x = A x + a

Theorem 1.5: The affine transformations from Real^n to Real^m are the mappings T of the form T x = A x + a, where A is a linear transformation and a ∈ Real^m.

theorem sumExtend_apply_inl {ι : Type u_1} {K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] {v : ι → V} (hs : LinearIndependent K v) (i : ι) : (Module.Basis.sumExtend hs) (Sum.inl i) = v i

sumExtend agrees with the original family on the left summand.

theorem linearEquiv_exists_of_linearIndependent (m n : ℕ) (v v' : Fin m → Fin n → ℝ) : LinearIndependent ℝ v → LinearIndependent ℝ v' → ∃ (A : (Fin n → ℝ) ≃ₗ[ℝ] Fin n → ℝ), ∀ (i : Fin m), A (v i) = v' i

Extend linearly independent families to bases and map one to the other.

theorem linearEquiv_exists_map_differences (m n : ℕ) (b b' : Fin (m + 1) → Fin n → ℝ) : IsAffinelyIndependent m n b → IsAffinelyIndependent m n b' → ∃ (A : (Fin n → ℝ) ≃ₗ[ℝ] Fin n → ℝ), ∀ (i : Fin m), A (b i.succ - b 0) = b' i.succ - b' 0

Construct a linear equivalence sending the difference vectors of two affinely independent families to each other.

theorem affineTransformation_bijective_of_linearEquiv_shift (n : ℕ) (A : (Fin n → ℝ) ≃ₗ[ℝ] Fin n → ℝ) (b0 b0' : Fin n → ℝ) : (IsAffineTransformation n n fun (x : Fin n → ℝ) => A (x - b0) + b0') ∧ Function.Bijective fun (x : Fin n → ℝ) => A (x - b0) + b0'

The affine map defined by a linear equivalence and a translation is affine and bijective.

theorem affineSpan_range_eq_top_of_isAffinelyIndependent_eq (n : ℕ) (b : Fin (n + 1) → Fin n → ℝ) : IsAffinelyIndependent n n b → affineSpan ℝ (Set.range b) = ⊤

Affinely independent families of size n + 1 in Real^n span the whole space.

theorem affineTransformation_exists_of_affineIndependent (m n : ℕ) (b b' : Fin (m + 1) → Fin n → ℝ) : IsAffinelyIndependent m n b → IsAffinelyIndependent m n b' → ∃ (T : (Fin n → ℝ) → Fin n → ℝ), IsAffineTransformation n n T ∧ Function.Bijective T ∧ (∀ (i : Fin (m + 1)), T (b i) = b' i) ∧ (m = n → ∀ (T' : (Fin n → ℝ) → Fin n → ℝ), IsAffineTransformation n n T' → Function.Bijective T' → (∀ (i : Fin (m + 1)), T' (b i) = b' i) → T' = T)

Theorem 1.6: Let {b_0, b_1, ..., b_m} and {b'_0, b'_1, ..., b'_m} be affinely independent sets in Real^n. Then there exists a one-to-one affine transformation T of Real^n onto itself such that T b_i = b'_i for i = 0, ..., m. If m = n, then T is unique.

theorem affineSetDim_eq_neg_one_iff_empty (n : ℕ) (M : Set (Fin n → ℝ)) (hM : IsAffineSet n M) : affineSetDim n M hM = -1 ↔ M = ∅

An affine set has dimension -1 if and only if it is empty.

theorem affineSetDim_eq_finrank_parallel (n : ℕ) (M : Set (Fin n → ℝ)) (hM : IsAffineSet n M) (hne : M.Nonempty) {L : Submodule ℝ (Fin n → ℝ)} (hL : IsParallelAffineSet n M ↑L) : affineSetDim n M hM = Int.ofNat (Module.finrank ℝ ↥L)

For a nonempty affine set, the dimension equals the finrank of any parallel submodule.

theorem range_fin_cases {m : ℕ} {α : Type u_1} (a : α) (b : Fin m → α) : (Set.range fun (i : Fin (m + 1)) => Fin.cases a b i) = {a} ∪ Set.range b

The range of Fin.cases is the union of the head and tail ranges.

theorem affineHull_zero_union_range_eq_submodule (n m : ℕ) (L : Submodule ℝ (Fin n → ℝ)) (v : Module.Basis (Fin m) ℝ ↥L) : affineHull n ({0} ∪ Set.range fun (i : Fin m) => ↑(v i)) = ↑L

The affine hull of {0} together with a basis of a submodule is that submodule.

theorem affinelyIndependent_family_of_basis (n m : ℕ) (L : Submodule ℝ (Fin n → ℝ)) (v : Module.Basis (Fin m) ℝ ↥L) (b0 : Fin n → ℝ) : ∃ (b : Fin (m + 1) → Fin n → ℝ), IsAffinelyIndependent m n b ∧ affineHull n (Set.range b) = SetTranslate n (↑L) b0

From a basis of a submodule and a base point, build affinely independent points spanning the translate.

theorem affineTransformation_map_affineCombination_univ {m n : ℕ} (T : (Fin n → ℝ) → Fin n → ℝ) (b : Fin (m + 1) → Fin n → ℝ) (coeffs : Fin (m + 1) → ℝ) (hT : IsAffineTransformation n n T) (hsum : ∑ i : Fin (m + 1), coeffs i = 1) : T (∑ i : Fin (m + 1), coeffs i • b i) = ∑ i : Fin (m + 1), coeffs i • T (b i)

Affine transformations preserve full-index affine combinations.

theorem affineTransformation_exists_of_affineSet_same_dim (n : ℕ) (M1 M2 : Set (Fin n → ℝ)) (hM1 : IsAffineSet n M1) (hM2 : IsAffineSet n M2) (hDim : affineSetDim n M1 hM1 = affineSetDim n M2 hM2) : ∃ (T : (Fin n → ℝ) → Fin n → ℝ), IsAffineTransformation n n T ∧ Function.Bijective T ∧ T '' M1 = M2

Corollary 1.6.1: Let M_1 and M_2 be affine sets in Real^n of the same dimension. Then there exists a one-to-one affine transformation T of Real^n onto itself such that T '' M_1 = M_2.

theorem affine_inverse_rewrite (n : ℕ) (A : (Fin n → ℝ) ≃ₗ[ℝ] Fin n → ℝ) (a : Fin n → ℝ) : (fun (x : Fin n → ℝ) => A.symm (x - a)) = fun (x : Fin n → ℝ) => ↑A.symm x + -A.symm a

Rewrite the inverse formula into linear-plus-constant form.

theorem affineTransformation_of_linearEquiv_symm_add (n : ℕ) (A : (Fin n → ℝ) ≃ₗ[ℝ] Fin n → ℝ) (a : Fin n → ℝ) : IsAffineTransformation n n fun (x : Fin n → ℝ) => ↑A.symm x + -A.symm a

The inverse formula is affine as a linear map plus translation.

theorem inverse_affineTransformation_of_linearEquiv (n : ℕ) (A : (Fin n → ℝ) ≃ₗ[ℝ] Fin n → ℝ) (a : Fin n → ℝ) : (IsAffineTransformation n n fun (x : Fin n → ℝ) => A x + a) → IsAffineTransformation n n fun (x : Fin n → ℝ) => A.symm (x - a)

The inverse of an affine map with linear part A is affine.

theorem affineTransformation_image_affineSet (n m : ℕ) (T : (Fin n → ℝ) → Fin m → ℝ) : IsAffineTransformation n m T → ∀ (M : Set (Fin n → ℝ)), IsAffineSet n M → IsAffineSet m (T '' M)

The image of an affine set under an affine transformation is affine.

theorem affineTransformation_preimage_affineSet (n m : ℕ) (T : (Fin n → ℝ) → Fin m → ℝ) : IsAffineTransformation n m T → ∀ (N : Set (Fin m → ℝ)), IsAffineSet m N → IsAffineSet n (T ⁻¹' N)

The preimage of an affine set under an affine transformation is affine.

theorem affineTransformation_image_affineSet_and_affineHull (n m : ℕ) (T : (Fin n → ℝ) → Fin m → ℝ) : IsAffineTransformation n m T → (∀ (M : Set (Fin n → ℝ)), IsAffineSet n M → IsAffineSet m (T '' M)) ∧ ∀ (S : Set (Fin n → ℝ)), affineHull m (T '' S) = T '' affineHull n S

Text 1.12: Let T : ℝ^n → ℝ^m be an affine transformation. Then for every affine set M ⊆ ℝ^n, the image T '' M is an affine set in ℝ^m. Consequently, for every set S ⊆ ℝ^n, affine transformations preserve affine hulls: affineHull m (T '' S) = T '' affineHull n S.

def IsTuckerRepresentation (n m : ℕ) (M : Set (Fin (n + m) → ℝ)) : Prop

Text 1.13: Let M ⊆ ℝ^N be an n-dimensional affine set with 0 < n < N and set m := N - n. A Tucker representation is a coordinate permutation so that x ∈ M iff the last m coordinates are affine functions of the first n, equivalently M is the graph of an affine map ℝ^n → ℝ^m; for linear subspaces the constants vanish.

Equations

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

theorem affineSet_eq_translate_submodule (n : ℕ) (C : Set (Fin n → ℝ)) (hC : IsAffineSet n C) (hne : C.Nonempty) : ∃ (L : Submodule ℝ (Fin n → ℝ)) (x0 : Fin n → ℝ), C = SetTranslate n (↑L) x0

A nonempty affine set is a translate of a submodule.

theorem exists_isCompl_submodule (n : ℕ) (L : Submodule ℝ (Fin n → ℝ)) : ∃ (W : Submodule ℝ (Fin n → ℝ)), IsCompl L W

Any submodule admits a complementary submodule.

theorem image_translate_under_prod_equiv (n : ℕ) (L W : Submodule ℝ (Fin n → ℝ)) (hLW : IsCompl L W) (x0 : Fin n → ℝ) : ⇑(L.prodEquivOfIsCompl W hLW).symm '' SetTranslate n (↑L) x0 = {p : ↥L × ↥W | p.2 = ((L.prodEquivOfIsCompl W hLW).symm x0).2}

In product coordinates given by a complement, a translate of L has constant W-part.

theorem affineSet_is_graph_of_affineMap (n : ℕ) (C : Set (Fin n → ℝ)) (hC : IsAffineSet n C) (hne : C.Nonempty) : ∃ (L : Submodule ℝ (Fin n → ℝ)) (W : Submodule ℝ (Fin n → ℝ)) (Φ : (Fin n → ℝ) ≃ₗ[ℝ] ↥L × ↥W) (f : ↥L →ᵃ[ℝ] ↥W), ⇑Φ '' C = {p : ↥L × ↥W | p.2 = f p.1}