Thickness and dilated translation growth #
The geometric sum estimate outside a central slab supplies a uniform spectral gap for short integer multiples of the available translations. Subadditivity then transfers growth back to an original translation.
theorem
EGZ.Expansion.exists_boundary_of_dilated_characters
{p d K m : ℕ}
[NeZero p]
(w : FpCoord p d → ℝ)
(hw : ∀ (v : FpCoord p d), 0 ≤ w v)
(hW : 0 < ∑ v : FpCoord p d, w v)
(hm : 0 < m)
{δ : ℝ}
(hδ : 0 ≤ δ)
(hthick : IsCentrallyThick w K δ)
(hchar : ∀ (r : ZMod p), ¬HasBoundedRepresentative p K r → ‖∑ j : Fin m, (AddChar.zmodAddEquiv r) ↑↑j‖ ≤ ↑m / 2)
(Y : Finset (FpCoord p d))
(hhalf : 2 * Y.card ≤ p ^ d)
:
The growth step, separated from the one-dimensional character-sum estimate so that the combinatorial and analytic arguments remain reusable.
theorem
EGZ.Expansion.exists_boundary_of_central_thickness
{p d K : ℕ}
[NeZero p]
(hK : 0 < K)
(hKp : K ≤ p)
(w : FpCoord p d → ℝ)
(hw : ∀ (v : FpCoord p d), 0 ≤ w v)
(hW : 0 < ∑ v : FpCoord p d, w v)
{δ : ℝ}
(hδ : 0 ≤ δ)
(hthick : IsCentrallyThick w K δ)
(Y : Finset (FpCoord p d))
(hhalf : 2 * Y.card ≤ p ^ d)
:
Central thickness forces a translation with a proportionate boundary.
The absolute constant 20 suffices; the paper uses the looser 200.
theorem
EGZ.Expansion.exists_translate_growth_of_central_thickness
{p d K : ℕ}
[NeZero p]
(hK : 0 < K)
(hKp : K ≤ p)
(w : FpCoord p d → ℝ)
(hw : ∀ (v : FpCoord p d), 0 ≤ w v)
(hW : 0 < ∑ v : FpCoord p d, w v)
{δ : ℝ}
(hδ : 0 ≤ δ)
(hthick : IsCentrallyThick w K δ)
(Y : Finset (FpCoord p d))
(hhalf : 2 * Y.card ≤ p ^ d)
:
Multiplicative form of the central-thickness growth lemma.