Documentation

LeanPool.SumOfSetsInSeveralDimensions.AffineDim

Affine dimension of a finite set #

The affine dimension of a finite set S ⊆ ℝ^D is the dimension of the direction of its affine span. The direction of the affine span of S is the vector span of S, the subspace spanned by the differences of the points of S.

Main definitions #

Main statements #

source
noncomputable def Finset.affineDim {D : ℕ} (S : Finset (Fin D → ℝ)) :
ℕ

The affine dimension of a finite set S ⊆ ℝ^D: the dimension of the direction of the affine span of S.

Equations
Instances For
    source
    theorem Finset.affineDim_eq_finrank_vectorSpan {D : ℕ} (S : Finset (Fin D → ℝ)) :
    S.affineDim = Module.finrank ℝ ↥(vectorSpan ℝ ↑S)

    The affine dimension of S is the dimension of the vector span of S.

    source
    theorem Finset.affineDim_eq_finrank_span_sub {D : ℕ} (S : Finset (Fin D → ℝ)) :
    S.affineDim = Module.finrank ℝ ↥(Submodule.span ℝ (↑S - ↑S))

    The affine dimension of S is the dimension of the span of S - S.

    source
    theorem Finset.affineDim_mono {D : ℕ} {S T : Finset (Fin D → ℝ)} (hST : S ⊆ T) :
    S.affineDim ≤ T.affineDim

    Affine dimension is monotone under inclusion of finite sets.

    source
    theorem Finset.affineDim_le {D : ℕ} (S : Finset (Fin D → ℝ)) :
    S.affineDim ≤ D

    The affine dimension of a subset of ℝ^D is at most D.

    source
    @[simp]
    theorem Finset.affineDim_empty {D : ℕ} :
    ∅.affineDim = 0
    source
    @[simp]
    theorem Finset.affineDim_singleton {D : ℕ} (x : Fin D → ℝ) :
    {x}.affineDim = 0
    source
    @[simp]
    theorem Finset.affineDim_vadd_finset {D : ℕ} (c : Fin D → ℝ) (S : Finset (Fin D → ℝ)) :
    (c +ᵥ S).affineDim = S.affineDim

    The affine dimension is invariant under translation.

    source
    theorem Finset.affineDim_image_add_left {D : ℕ} (c : Fin D → ℝ) (S : Finset (Fin D → ℝ)) :
    (image (fun (x : Fin D → ℝ) => c + x) S).affineDim = S.affineDim

    The affine dimension of c + S is that of S.

    source
    theorem Finset.affineDim_image_add_right {D : ℕ} (c : Fin D → ℝ) (S : Finset (Fin D → ℝ)) :
    (image (fun (x : Fin D → ℝ) => x + c) S).affineDim = S.affineDim

    The affine dimension of S + c is that of S.

    source
    theorem Finset.affineDim_image_sub {D : ℕ} (S : Finset (Fin D → ℝ)) (c : Fin D → ℝ) :
    (image (fun (x : Fin D → ℝ) => x - c) S).affineDim = S.affineDim

    The affine dimension of S - c is that of S.

    source
    theorem Finset.affineDim_add_one_le_card {D : ℕ} {S : Finset (Fin D → ℝ)} (hS : S.Nonempty) :
    S.affineDim + 1 ≤ S.card

    A nonempty finite set of affine dimension d contains at least d + 1 points.

    source
    theorem Finset.affineDim_le_card {D : ℕ} (S : Finset (Fin D → ℝ)) :
    S.affineDim ≤ S.card

    The affine dimension of a finite set is at most its number of points.