Reconstructing relative thinness from concentrated exchanges

Concentration of the individual exchange components gives centres in each fibre. Integer affine relations turn these centres into one affine slab.

theorem EGZ.Expansion.finiteProb_sigma_le {I : Type u_1} [Fintype I] [Nonempty I] (A : I → Type u_2) [(i : I) → Fintype (A i)] [∀ (i : I), Nonempty (A i)] (P : (i : I) × A i → Prop) {η : ℝ} (h : ∀ (i : I), (finiteProb fun (a : A i) => P ⟨i, a⟩) ≤ η) : finiteProb P ≤ η

theorem EGZ.Expansion.finiteProb_eq_natMassOn {A : Type u_1} [Fintype A] (P : A → Prop) : finiteProb P = ↑(natMassOn (fun (x : A) => 1) {a : A | P a}) / ↑(Fintype.card A)

theorem EGZ.Expansion.isThinAlong_pushWeight_of_finiteProb {A : Type u_1} [Fintype A] [Nonempty A] {p n K : ℕ} [NeZero p] (point : A → FpCoord p n) (ξ : FpCoord p n →ᵃ[ZMod p] ZMod p) {η : ℝ} (h : (finiteProb fun (a : A) => ¬HasBoundedRepresentative p K (ξ (point a))) ≤ η) : IsThinAlong (pushWeight point fun (x : A) => 1) ξ K η

theorem EGZ.Expansion.sum_signed_slots {S : Type u_1} {I : Type u_2} {R : Type u_3} [Fintype S] [DecidableEq S] [Fintype I] [CommRing R] (label : I → S) (sign : I → ℤ) (coeff : S → ℤ) (hcoeff : ∀ (q : S), (∑ i : I, if label i = q then sign i else 0) = coeff q) (v : S → R) : ∑ i : I, ↑(sign i) * v (label i) = ∑ q : S, ↑(coeff q) * v q

Grouping the signed slots of a relation by their labels.

theorem EGZ.Expansion.relative_concentration {p r t N B W : ℕ} [Fact (Nat.Prime p)] (S : Finset (IntCoord r)) [Nonempty ↥S] (X : ↥S → Type u_1) [(q : ↥S) → Fintype (X q)] [∀ (q : ↥S), Nonempty (X q)] (point : (q : ↥S) → X q → FpCoord p (r + t)) (hlabel : ∀ (q : ↥S) (x : X q), (Coord.first r t) (point q x) = IntCoord.mod p ↑q) (M : Matrix (↥S) (Option (Fin r)) ℤ) (Q : Matrix ↥S ↥S ℤ) (hQ : Q = ↑N • 1 - M * affineConstraintMatrix S) (hsize : ∀ (q : ↥S), ∑ z : ↥S, (Q z q).natAbs ≤ B) (hN : 0 < N) (hNp : N < p) (ξ : FpCoord p t →ₗ[ZMod p] ZMod p) (hξ : ξ ≠ 0) {η : ℝ} (hη : 0 ≤ η) (hsmall : (↑B + 1) * η < 1) (hpair : ∀ (q : ↥S), (finiteProb fun (x : X q × X q) => ¬HasBoundedRepresentative p W (ξ ((Coord.last r t) (point q x.2)) - ξ ((Coord.last r t) (point q x.1)))) ≤ η) (hsum : ∀ (q : ↥S), (finiteProb fun (x : (ExchangePattern.ofRelation fun (z : ↥S) => Q z q).Sample X) => ¬HasBoundedRepresentative p W ((ExchangePattern.ofRelation fun (z : ↥S) => Q z q).sampleSum (fun (z : ↥S) (a : X z) => ξ ((Coord.last r t) (point z a))) x)) ≤ η) : ∃ (ψ : FpCoord p (r + t) →ᵃ[ZMod p] ZMod p), NonconstantOnFibers (⇑(Coord.first r t)) ψ ∧ (finiteProb fun (x : (q : ↥S) × X q) => ¬HasBoundedRepresentative p ((N + B + 1) * W) (ψ (point x.fst x.snd))) ≤ η

If every diagonal exchange and every chosen affine-relation exchange is concentrated, all positions lie mostly in one affine slab that varies in a fibre direction.