Affine dimension of a sumset

The affine dimension of A + B is at least the affine dimensions of A and of B when both sets are nonempty, and at least the affine dimension of A ∪ B minus one.

Main statements

• Finset.affineDim_le_affineDim_add_right, Finset.affineDim_le_affineDim_add_left: the affine dimensions of A and B are at most that of A + B.
• Finset.affineDim_add_eq_of_left_eq: if A ⊆ ℝ^D has affine dimension D, so has A + B.
• Finset.affineDim_union_le_sum_add_one: the affine dimension of A ∪ B is at most that of A + B plus one.

theorem Finset.affineDim_le_affineDim_add_right {D : ℕ} (A : Finset (Fin D → ℝ)) {B : Finset (Fin D → ℝ)} (hB : B.Nonempty) : A.affineDim ≤ (A + B).affineDim

The affine dimension of A is at most that of A + B when B is nonempty.

theorem Finset.affineDim_le_affineDim_add_left {D : ℕ} {A : Finset (Fin D → ℝ)} (hA : A.Nonempty) (B : Finset (Fin D → ℝ)) : B.affineDim ≤ (A + B).affineDim

The affine dimension of B is at most that of A + B when A is nonempty.

theorem Finset.affineDim_add_eq_of_left_eq {D : ℕ} {A B : Finset (Fin D → ℝ)} (hB : B.Nonempty) (hA : A.affineDim = D) : (A + B).affineDim = D

If A ⊆ ℝ^D has affine dimension D and B is nonempty, then A + B has affine dimension D.

theorem Finset.affineDim_union_le_sum_add_one {D : ℕ} {A B : Finset (Fin D → ℝ)} (hA : A.Nonempty) (hB : B.Nonempty) : (A ∪ B).affineDim ≤ (A + B).affineDim + 1

The affine span of A ∪ B has dimension at most one more than the affine span of A + B.