Translating a set so that its lexicographic minimum is the origin

Order ℝ^D lexicographically. The translate normalize S of a nonempty finite set S by minus its least element contains 0, and its other elements are positive. Cardinalities of sets and sumsets and the affine dimension of a sumset do not change under this translation.

noncomputable def SumOfSetsInSeveralDimensions.normalize {D : ℕ} (S : Finset (Fin D → ℝ)) (hS : S.Nonempty) : Finset (Fin D → ℝ)

The translate of a nonempty finite set S ⊆ ℝ^D by minus its lexicographically least element.

Equations

• SumOfSetsInSeveralDimensions.normalize S hS = Finset.image (fun (x : Fin D → ℝ) => x - SumOfSetsInSeveralDimensions.lexMin✝ S hS) S

theorem SumOfSetsInSeveralDimensions.normalize_card {D : ℕ} {S : Finset (Fin D → ℝ)} (hS : S.Nonempty) : (normalize S hS).card = S.card

Translation does not change the number of points.

theorem SumOfSetsInSeveralDimensions.zero_mem_normalize {D : ℕ} {S : Finset (Fin D → ℝ)} (hS : S.Nonempty) : 0 ∈ normalize S hS

The translated set contains the origin.

theorem SumOfSetsInSeveralDimensions.normalize_nonempty {D : ℕ} {S : Finset (Fin D → ℝ)} (hS : S.Nonempty) : (normalize S hS).Nonempty

The translated set is nonempty.

theorem SumOfSetsInSeveralDimensions.normalize_pos_of_ne_zero {D : ℕ} {S : Finset (Fin D → ℝ)} (hS : S.Nonempty) {x : Fin D → ℝ} (hx : x ∈ normalize S hS) (hx0 : x ≠ 0) : 0 < toLex x

The nonzero elements of the translated set are lexicographically positive.

theorem SumOfSetsInSeveralDimensions.normalize_add_card {D : ℕ} {A B : Finset (Fin D → ℝ)} (hA : A.Nonempty) (hB : B.Nonempty) : (normalize A hA + normalize B hB).card = (A + B).card

The sum of the translates of A and B has as many points as A + B.

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

The sum of the translates of A and B has the affine dimension of A + B.