Relative expansion #
The thresholds are first chosen for a fixed finite lattice support, then made uniform over every support in the prescribed box. All sampling and deletion arguments retain the positions of repeated vectors.
theorem
EGZ.Expansion.relative_expansion_fixed_support
{r t : ℕ}
(ht : 0 < t)
(S : Finset (IntCoord r))
(hS : S.Nonempty)
(δ : ℝ)
(hδ : 0 < δ)
:
∃ (T₀ : ℕ) (p₀ : ℕ),
∀ (T : ℕ),
T₀ ≤ T →
∀ (p : ℕ),
Fact (Nat.Prime p) →
∀ (x : NeZero p),
p₀ ≤ p →
(Function.Injective fun (q : ↥S) => IntCoord.mod p ↑q) →
∀ (w : FpCoord p (r + t) → ℕ) (α : ↥S → ℤ),
(∀ (v : FpCoord p (r + t)), w v ≠ 0 → ∃ (q : ↥S), (Coord.first r t) v = IntCoord.mod p ↑q) →
∑ q : ↥S, α q • ↑q = 0 →
∑ q : ↥S, α q = ↑p →
(∀ (q : ↥S),
δ * ↑p ≤ ↑(α q) ∧ ↑(α q) ≤ ↑(pushWeight (⇑(Coord.first r t)) w (IntCoord.mod p ↑q)) - δ * ↑p) →
IsThickRelative w (⇑(Coord.first r t)) T δ → HasZeroSumMultiplicity w
For one fixed support, the analytic parameters are independent of the prime, the fibre multiplicities and the prescribed coefficients.
The relative expansion theorem, with uniform thresholds for all supports in a fixed integer box.