Thick distributions of available disjoint exchanges #
An equal mixture of diagonal and affine-relation samples is thick. The collision estimate permits restriction to injective samples, which are actual exchanges on the unused atom positions.
theorem
EGZ.Expansion.exists_thick_exchange_weight
{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)]
{A : Type u_2}
[Finite A]
(point : A → FpCoord p (r + t))
(encode : (q : ↥S) → X q → A)
(hinj : ∀ (q : ↥S), Function.Injective (encode q))
(hlabel : ∀ (q : ↥S) (x : X q), (Coord.first r t) (point (encode q x)) = IntCoord.mod p ↑q)
(U : Finset A)
(hU : ∀ (q : ↥S) (x : X q), encode q x ∉ U)
(D : Matrix (↥S) (Option (Fin r)) ℤ)
(Q : Matrix ↥S ↥S ℤ)
(hQ : Q = ↑N • 1 - D * affineConstraintMatrix S)
(hAQ : affineConstraintMatrix S * Q = 0)
(hsize : ∀ (q : ↥S), ∑ z : ↥S, (Q z q).natAbs ≤ B)
(hB : 2 ≤ B)
(hN : 0 < N)
(hNp : N < p)
{η δ m : ℝ}
(hη : 0 < η)
(hηone : η ≤ 1)
(hηδ : η ≤ δ)
(hsmall : (↑B + 1) * η < 1)
(hm : 0 < m)
(hcard : ∀ (q : ↥S), m ≤ ↑(Fintype.card (X q)))
(hcollision : ↑B ^ 2 / m ≤ η / 2)
(hthick :
IsThickRelative (pushWeight (fun (z : (q : ↥S) × X q) => point (encode z.fst z.snd)) fun (x : (q : ↥S) × X q) => 1)
(⇑(Coord.first r t)) ((N + B + 1) * W) δ)
: