Bounded exchange patterns and their independent samples

A pattern prescribes the number of positive and negative positions in each fibre. Sampling all these positions independently gives exact uniform marginals; injective samples are the disjoint exchanges used later.

structure EGZ.Expansion.ExchangePattern (S : Type u_1) : Type u_1

The positive and negative multiplicities specifying a signed exchange pattern.

• positive : S → ℕ

  The number of positive positions carrying each label.

• negative : S → ℕ

  The number of negative positions carrying each label.

def EGZ.Expansion.ExchangePattern.Position {S : Type u_1} (P : ExchangePattern S) : Type u_1

The labelled positions of an exchange pattern, separated into positive and negative copies.

Equations

• P.Position = ((q : S) × Fin (P.positive q) ⊕ (q : S) × Fin (P.negative q))

@[instance_reducible]

instance EGZ.Expansion.ExchangePattern.instFintypePosition {S : Type u_1} [Fintype S] (P : ExchangePattern S) : Fintype P.Position

Equations

• P.instFintypePosition = { elems := EGZ.Expansion.ExchangePattern.instFintypePosition._aux_1 P, complete := ⋯ }

@[instance_reducible]

instance EGZ.Expansion.ExchangePattern.instDecidableEqPosition {S : Type u_1} [DecidableEq S] (P : ExchangePattern S) : DecidableEq P.Position

Equations

• P.instDecidableEqPosition = EGZ.Expansion.ExchangePattern.instDecidableEqPosition._aux_1 P

def EGZ.Expansion.ExchangePattern.label {S : Type u_1} (P : ExchangePattern S) : P.Position → S

The label carried by a position of the exchange pattern.

Equations

• P.label = Sum.elim Sigma.fst Sigma.fst

def EGZ.Expansion.ExchangePattern.sign {S : Type u_1} (P : ExchangePattern S) : P.Position → ℤ

The integer sign of a position: one for a positive copy and minus one for a negative copy.

Equations

• P.sign = Sum.elim (fun (x : (q : S) × Fin (P.positive q)) => 1) fun (x : (q : S) × Fin (P.negative q)) => -1

@[reducible, inline]

abbrev EGZ.Expansion.ExchangePattern.Sample {S : Type u_1} (P : ExchangePattern S) (X : S → Type u_2) : Type (max u_2 u_1)

A choice of a sample from the prescribed fibre at every labelled position.

Equations

• P.Sample X = ((i : P.Position) → X (P.label i))

def EGZ.Expansion.ExchangePattern.size {S : Type u_1} [Fintype S] (P : ExchangePattern S) : ℕ

The total number of positive and negative positions in the pattern.

Equations

• P.size = ∑ q : S, P.positive q + ∑ q : S, P.negative q

@[simp]

theorem EGZ.Expansion.ExchangePattern.card_position {S : Type u_1} [Fintype S] (P : ExchangePattern S) : Fintype.card P.Position = P.size

@[simp]

theorem EGZ.Expansion.ExchangePattern.sign_natAbs {S : Type u_1} (P : ExchangePattern S) (i : P.Position) : (P.sign i).natAbs = 1

theorem EGZ.Expansion.ExchangePattern.sum_sign_smul {S : Type u_1} [Fintype S] {G : Type u_2} [AddCommGroup G] (P : ExchangePattern S) (r : S → G) : ∑ i : P.Position, P.sign i • r (P.label i) = ∑ q : S, P.positive q • r q - ∑ q : S, P.negative q • r q

noncomputable def EGZ.Expansion.ExchangePattern.sampleSum {S : Type u_1} [Fintype S] {G : Type u_2} [AddCommGroup G] (P : ExchangePattern S) {X : S → Type u_3} (v : (q : S) → X q → G) (x : P.Sample X) : G

The signed sum of the vectors selected by a sample of the exchange pattern.

Equations

• P.sampleSum v x = ∑ i : P.Position, P.sign i • v (P.label i) (x i)

def EGZ.Expansion.ExchangePattern.ofRelation {S : Type u_1} (b : S → ℤ) : ExchangePattern S

The exchange pattern obtained by separating an integral relation into positive and negative parts.

Equations

• EGZ.Expansion.ExchangePattern.ofRelation b = { positive := fun (q : S) => (b q).toNat, negative := fun (q : S) => (-b q).toNat }

theorem EGZ.Expansion.ExchangePattern.ofRelation_sum {S : Type u_1} [Fintype S] {G : Type u_2} [AddCommGroup G] (b : S → ℤ) (r : S → G) : ∑ i : (ofRelation b).Position, (ofRelation b).sign i • r ((ofRelation b).label i) = ∑ q : S, b q • r q

theorem EGZ.Expansion.ExchangePattern.ofRelation_size {S : Type u_1} [Fintype S] (b : S → ℤ) : (ofRelation b).size = ∑ q : S, (b q).natAbs

theorem EGZ.Expansion.ExchangePattern.center_sum_bounded {S : Type u_1} [Fintype S] [DecidableEq S] (P : ExchangePattern S) {X : S → Type u_2} [(q : S) → Fintype (X q)] [∀ (q : S), Nonempty (X q)] {p W : ℕ} (v : (q : S) → X q → ZMod p) (r : S → ZMod p) {η : ℝ} (hcoord : ∀ (q : S), (finiteProb fun (x : X q) => ¬HasBoundedRepresentative p W (v q x - r q)) ≤ η) (hsum : (finiteProb fun (x : P.Sample X) => ¬HasBoundedRepresentative p W (P.sampleSum v x)) ≤ η) (hsmall : (↑P.size + 1) * η < 1) : HasBoundedRepresentative p ((1 + P.size) * W) (∑ q : S, P.positive q • r q - ∑ q : S, P.negative q • r q)

Product-sample concentration yields a deterministic bound for the corresponding sum of fibre centres.