Concentration of finite exchange samples

Pair differences find centres in the individual fibres. Product sampling then turns concentration of an exchange sum into a bounded relation among those centres.

theorem EGZ.Expansion.exists_center_of_pair_concentration {A : Type u_1} [Fintype A] [Nonempty A] {p W : ℕ} (v : A → ZMod p) {η : ℝ} (h : (finiteProb fun (x : A × A) => ¬HasBoundedRepresentative p W (v x.2 - v x.1)) ≤ η) : ∃ (r : ZMod p), (finiteProb fun (x : A) => ¬HasBoundedRepresentative p W (v x - r)) ≤ η

theorem EGZ.Expansion.bounded_center_sum_of_concentration {I : Type u_1} [Fintype I] [DecidableEq I] (A : I → Type u_2) [(i : I) → Fintype (A i)] [∀ (i : I), Nonempty (A i)] {p W : ℕ} (v : (i : I) → A i → ZMod p) (r : I → ZMod p) (a : I → ℤ) {η : ℝ} (hcoord : ∀ (i : I), (finiteProb fun (x : A i) => ¬HasBoundedRepresentative p W (v i x - r i)) ≤ η) (hsum : (finiteProb fun (x : (i : I) → A i) => ¬HasBoundedRepresentative p W (∑ i : I, ↑(a i) * v i (x i))) ≤ η) (hsmall : (↑(Fintype.card I) + 1) * η < 1) : HasBoundedRepresentative p ((1 + ∑ i : I, (a i).natAbs) * W) (∑ i : I, ↑(a i) * r i)

If the samples usually lie near their individual centres, and their signed sum usually lies in a central slab, then the same is true of the signed sum of centres, at a wider deterministic radius.