The Freiman dimension

The Freiman dimension of a finite subset X of an abelian group is the largest d ≤ |X| such that X is Freiman isomorphic of order 2 to a subset of ℚ^d that is not contained in a proper affine subspace. The affine dimension of the image is the Finset.affineDim of its inclusion in ℝ^d.

Main definitions

• rationalVectorToReal: the coordinatewise inclusion of ℚ^d into ℝ^d.
• freimanModelDim X d: X is Freiman isomorphic to a subset of ℚ^d of affine dimension d.
• freimanDim X: the Freiman dimension of X.

Main statements

• le_freimanDim_of_model: if d ≤ |X| and freimanModelDim X d, then d ≤ freimanDim X.
• freimanDim_add_one_le_card: a nonempty set X has Freiman dimension at most |X| - 1.

def SumOfSetsInSeveralDimensions.rationalVectorToReal {d : ℕ} (v : Fin d → ℚ) : Fin d → ℝ

The coordinatewise inclusion of rational vectors into real vectors.

Equations

• SumOfSetsInSeveralDimensions.rationalVectorToReal v i = ↑(v i)

def SumOfSetsInSeveralDimensions.freimanModelDim {G : Type u_1} [AddCommMonoid G] (X : Finset G) (d : ℕ) : Prop

The set X has a Freiman model of dimension d: there is a Freiman isomorphism of order 2 from X onto a subset of ℚ^d of affine dimension d.

Equations

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

noncomputable def SumOfSetsInSeveralDimensions.freimanDim {G : Type u_1} [AddCommMonoid G] (X : Finset G) : ℕ

The Freiman dimension of X: the largest d ≤ |X| such that X has a Freiman model of dimension d.

Equations

• SumOfSetsInSeveralDimensions.freimanDim X = Nat.findGreatest (SumOfSetsInSeveralDimensions.freimanModelDim X) X.card

theorem SumOfSetsInSeveralDimensions.le_freimanDim_of_model {G : Type u_1} [AddCommMonoid G] {X : Finset G} {d : ℕ} (hd : d ≤ X.card) (hmodel : freimanModelDim X d) : d ≤ freimanDim X

A Freiman model of X of dimension d ≤ |X| shows that d ≤ freimanDim X.

theorem SumOfSetsInSeveralDimensions.freimanDim_add_one_le_card {G : Type u_1} [AddCommMonoid G] {X : Finset G} (hX : X.Nonempty) : freimanDim X + 1 ≤ X.card

A nonempty set X has Freiman dimension at most |X| - 1.