Growth under translations

Translation boundaries are subadditive. Averaging overlaps with a finite set of translations supplies a large boundary, which can then be divided among short words in a set of generators. In particular this gives the basis growth estimate needed in relative expansion without using Loomis--Whitney.

def EGZ.Expansion.translate {G : Type u_1} [AddCommGroup G] (Y : Finset G) (a : G) : Finset G

Translate a finite set by an element of its ambient group.

Equations

• EGZ.Expansion.translate Y a = Finset.map (Equiv.toEmbedding (Equiv.addRight a)) Y

@[simp]

theorem EGZ.Expansion.mem_translate {G : Type u_1} [AddCommGroup G] {Y : Finset G} {a x : G} : x ∈ translate Y a ↔ x - a ∈ Y

@[simp]

theorem EGZ.Expansion.card_translate {G : Type u_1} [AddCommGroup G] (Y : Finset G) (a : G) : (translate Y a).card = Y.card

@[simp]

theorem EGZ.Expansion.translate_zero {G : Type u_1} [AddCommGroup G] (Y : Finset G) : translate Y 0 = Y

theorem EGZ.Expansion.translate_add {G : Type u_1} [AddCommGroup G] (Y : Finset G) (a b : G) : translate Y (a + b) = translate (translate Y a) b

theorem EGZ.Expansion.translate_sdiff {G : Type u_1} [AddCommGroup G] [DecidableEq G] (Y Z : Finset G) (a : G) : translate (Y \ Z) a = translate Y a \ translate Z a

def EGZ.Expansion.boundary {G : Type u_1} [AddCommGroup G] [DecidableEq G] (Y : Finset G) (a : G) : ℕ

The number of new points added by one translation.

Equations

• EGZ.Expansion.boundary Y a = (EGZ.Expansion.translate Y a \ Y).card

@[simp]

theorem EGZ.Expansion.boundary_zero {G : Type u_1} [AddCommGroup G] [DecidableEq G] (Y : Finset G) : boundary Y 0 = 0

theorem EGZ.Expansion.boundary_add_card {G : Type u_1} [AddCommGroup G] [DecidableEq G] (Y : Finset G) (a : G) : boundary Y a + Y.card = (translate Y a ∪ Y).card

theorem EGZ.Expansion.boundary_add_overlap {G : Type u_1} [AddCommGroup G] [DecidableEq G] (Y : Finset G) (a : G) : boundary Y a + (translate Y a ∩ Y).card = Y.card

theorem EGZ.Expansion.boundary_le_card {G : Type u_1} [AddCommGroup G] [DecidableEq G] (Y : Finset G) (a : G) : boundary Y a ≤ Y.card

theorem EGZ.Expansion.boundary_add_le {G : Type u_1} [AddCommGroup G] [DecidableEq G] (Y : Finset G) (a b : G) : boundary Y (a + b) ≤ boundary Y a + boundary Y b

theorem EGZ.Expansion.boundary_nsmul_le {G : Type u_1} [AddCommGroup G] [DecidableEq G] (Y : Finset G) (a : G) (n : ℕ) : boundary Y (n • a) ≤ n * boundary Y a

theorem EGZ.Expansion.boundary_sum_le {G : Type u_1} [AddCommGroup G] [DecidableEq G] {ι : Type u_2} (I : Finset ι) (Y : Finset G) (a : ι → G) : boundary Y (∑ i ∈ I, a i) ≤ ∑ i ∈ I, boundary Y (a i)

theorem EGZ.Expansion.sum_overlap_le {G : Type u_1} [AddCommGroup G] [DecidableEq G] (Y B : Finset G) : ∑ b ∈ B, (translate Y b ∩ Y).card ≤ Y.card * Y.card

A translation cannot overlap a set at more positions than the set has.

theorem EGZ.Expansion.exists_boundary_double_le {G : Type u_1} [AddCommGroup G] [DecidableEq G] (Y B : Finset G) (hB : B.Nonempty) (hlarge : 2 * Y.card ≤ B.card) : ∃ b ∈ B, Y.card ≤ 2 * boundary Y b

Among at least twice as many distinct translations as points of Y, one translation adds at least half the points of Y.

noncomputable def EGZ.Expansion.basisBox {p d : ℕ} [Fact (Nat.Prime p)] (E : Module.Basis (Fin d) (ZMod p) (FpCoord p d)) (m : ℕ) : Finset (FpCoord p d)

A box of short nonnegative words in a basis, before reduction wraps.

Equations

• EGZ.Expansion.basisBox E m = Finset.image (fun (a : Fin d → Fin m) => E.equivFun.symm fun (i : Fin d) => ↑↑(a i)) Finset.univ

theorem EGZ.Expansion.basisBox_injective {p d : ℕ} [Fact (Nat.Prime p)] (E : Module.Basis (Fin d) (ZMod p) (FpCoord p d)) {m : ℕ} (hm : m ≤ p) : Function.Injective fun (a : Fin d → Fin m) => E.equivFun.symm fun (i : Fin d) => ↑↑(a i)

theorem EGZ.Expansion.card_basisBox {p d : ℕ} [Fact (Nat.Prime p)] (E : Module.Basis (Fin d) (ZMod p) (FpCoord p d)) {m : ℕ} (hm : m ≤ p) : (basisBox E m).card = m ^ d

theorem EGZ.Expansion.basisBox_nonempty {p d : ℕ} [Fact (Nat.Prime p)] (E : Module.Basis (Fin d) (ZMod p) (FpCoord p d)) {m : ℕ} (hm : 0 < m) : (basisBox E m).Nonempty

theorem EGZ.Expansion.boundary_basisBox_le {p d : ℕ} [Fact (Nat.Prime p)] (E : Module.Basis (Fin d) (ZMod p) (FpCoord p d)) (Y : Finset (FpCoord p d)) {m : ℕ} {b : FpCoord p d} (hb : b ∈ basisBox E m) : boundary Y b ≤ m * ∑ i : Fin d, boundary Y (E i)

A member of a basis box adds at most the sum of the boundaries of its individual basis steps, counted with their multiplicities.

theorem EGZ.Expansion.exists_basis_boundary {p d : ℕ} [Fact (Nat.Prime p)] (E : Module.Basis (Fin d) (ZMod p) (FpCoord p d)) (hd : 0 < d) (Y : Finset (FpCoord p d)) {m : ℕ} (hmpos : 0 < m) (hmp : m ≤ p) (hsize : 2 * Y.card ≤ m ^ d) : ∃ (i : Fin d), Y.card ≤ 2 * m * d * boundary Y (E i)

Integer form of the basis growth estimate. Taking m = ceil (2 * |Y|^(1/d)) yields the usual power-size increment.

theorem EGZ.Expansion.exists_basis_boundary_real {p d : ℕ} [Fact (Nat.Prime p)] (E : Module.Basis (Fin d) (ZMod p) (FpCoord p d)) (hd : 0 < d) (Y : Finset (FpCoord p d)) (x : ℝ) (hx : 1 ≤ x) (hcard : ↑Y.card = x ^ d) (hxp : 2 * x ≤ ↑p) : ∃ (i : Fin d), x ^ (d - 1) ≤ 6 * ↑d * ↑(boundary Y (E i))