Finite exchanges and their consumed positions

An exchange uses two disjoint sets of atom positions, with equal sizes and equal first-coordinate sums. Its shift lies in the remaining coordinates. Injective samples of a balanced pattern produce such exchanges.

def EGZ.Expansion.Exchange {p r t : ℕ} {A : Type u_1} (point : A → FpCoord p (r + t)) (B : ℕ) : Type u_1

The finite collection of exchanges of bounded size in a fixed atom family. Multiplicity is represented by distinct atom positions.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance EGZ.Expansion.instFintypeExchange {p r t : ℕ} {A : Type u_1} [Fintype A] (point : A → FpCoord p (r + t)) (B : ℕ) : Fintype (Exchange point B)

Equations

• EGZ.Expansion.instFintypeExchange point B = id inferInstance

def EGZ.Expansion.Exchange.left {p r t : ℕ} {A : Type u_1} {point : A → FpCoord p (r + t)} {B : ℕ} (E : Exchange point B) : Finset A

The finite set of atoms on the left side of an exchange.

Equations

• E.left = (↑E).1

def EGZ.Expansion.Exchange.right {p r t : ℕ} {A : Type u_1} {point : A → FpCoord p (r + t)} {B : ℕ} (E : Exchange point B) : Finset A

The finite set of atoms on the right side of an exchange.

Equations

• E.right = (↑E).2

noncomputable def EGZ.Expansion.Exchange.support {p r t : ℕ} {A : Type u_1} {point : A → FpCoord p (r + t)} {B : ℕ} (E : Exchange point B) : Finset A

The atoms used by either side of an exchange.

Equations

• E.support = E.left ∪ E.right

noncomputable def EGZ.Expansion.Exchange.difference {p r t : ℕ} {A : Type u_1} {point : A → FpCoord p (r + t)} {B : ℕ} (E : Exchange point B) : FpCoord p (r + t)

The difference between the vector sums of the left and right sides of an exchange.

Equations

• E.difference = ∑ x ∈ E.left, point x - ∑ x ∈ E.right, point x

noncomputable def EGZ.Expansion.Exchange.shift {p r t : ℕ} {A : Type u_1} {point : A → FpCoord p (r + t)} {B : ℕ} (E : Exchange point B) : FpCoord p t

The final coordinate block of the exchange difference.

Equations

• E.shift = (EGZ.Coord.last r t) E.difference

theorem EGZ.Expansion.Exchange.disjoint {p r t : ℕ} {A : Type u_1} {point : A → FpCoord p (r + t)} {B : ℕ} (E : Exchange point B) : Disjoint E.left E.right

theorem EGZ.Expansion.Exchange.card_eq {p r t : ℕ} {A : Type u_1} {point : A → FpCoord p (r + t)} {B : ℕ} (E : Exchange point B) : E.left.card = E.right.card

theorem EGZ.Expansion.Exchange.first_sum_eq {p r t : ℕ} {A : Type u_1} {point : A → FpCoord p (r + t)} {B : ℕ} (E : Exchange point B) : ∑ x ∈ E.left, (Coord.first r t) (point x) = ∑ x ∈ E.right, (Coord.first r t) (point x)

theorem EGZ.Expansion.Exchange.size_le {p r t : ℕ} {A : Type u_1} {point : A → FpCoord p (r + t)} {B : ℕ} (E : Exchange point B) : E.left.card + E.right.card ≤ B

theorem EGZ.Expansion.Exchange.support_card_le {p r t : ℕ} {A : Type u_1} {point : A → FpCoord p (r + t)} {B : ℕ} (E : Exchange point B) : E.support.card ≤ B

theorem EGZ.Expansion.Exchange.first_difference {p r t : ℕ} {A : Type u_1} {point : A → FpCoord p (r + t)} {B : ℕ} (E : Exchange point B) : (Coord.first r t) E.difference = 0

theorem EGZ.Expansion.Exchange.shift_eq_zero_of_support_eq_empty {p r t : ℕ} {A : Type u_1} {point : A → FpCoord p (r + t)} {B : ℕ} (E : Exchange point B) (h : E.support = ∅) : E.shift = 0

noncomputable def EGZ.Expansion.Exchange.ofPair {p r t : ℕ} {A : Type u_1} (point : A → FpCoord p (r + t)) {B : ℕ} (x y : A) (hxy : x ≠ y) (hfirst : (Coord.first r t) (point y) = (Coord.first r t) (point x)) (hB : 2 ≤ B) : Exchange point B

Exchange one atom for a distinct atom in the same first-coordinate fibre. The shift has the orientation point y - point x.

Equations

• EGZ.Expansion.Exchange.ofPair point x y hxy hfirst hB = ⟨({y}, {x}), ⋯⟩

@[simp]

theorem EGZ.Expansion.Exchange.ofPair_shift {p r t : ℕ} {A : Type u_1} (point : A → FpCoord p (r + t)) {B : ℕ} (x y : A) (hxy : x ≠ y) (hfirst : (Coord.first r t) (point y) = (Coord.first r t) (point x)) (hB : 2 ≤ B) : (ofPair point x y hxy hfirst hB).shift = (Coord.last r t) (point y - point x)

theorem EGZ.Expansion.Exchange.ofPair_support_avoids {p r t : ℕ} {A : Type u_1} (point : A → FpCoord p (r + t)) {B : ℕ} (x y : A) (hxy : x ≠ y) (hfirst : (Coord.first r t) (point y) = (Coord.first r t) (point x)) (hB : 2 ≤ B) (U : Finset A) (hx : x ∉ U) (hy : y ∉ U) : Disjoint (ofPair point x y hxy hfirst hB).support U

noncomputable def EGZ.Expansion.Exchange.positiveAtoms {A : Type u_1} {S : Type u_2} [Fintype S] (P : ExchangePattern S) (atom : P.Position → A) : Finset A

The atoms chosen at the positive positions of the exchange pattern.

Equations

• EGZ.Expansion.Exchange.positiveAtoms P atom = Finset.image (fun (i : (q : S) × Fin (P.positive q)) => atom (Sum.inl i)) Finset.univ

noncomputable def EGZ.Expansion.Exchange.negativeAtoms {A : Type u_1} {S : Type u_2} [Fintype S] (P : ExchangePattern S) (atom : P.Position → A) : Finset A

The atoms chosen at the negative positions of the exchange pattern.

Equations

• EGZ.Expansion.Exchange.negativeAtoms P atom = Finset.image (fun (i : (q : S) × Fin (P.negative q)) => atom (Sum.inr i)) Finset.univ

theorem EGZ.Expansion.Exchange.positiveAtoms_card {A : Type u_1} {S : Type u_2} [Fintype S] (P : ExchangePattern S) (atom : P.Position → A) (hinj : Function.Injective atom) : (positiveAtoms P atom).card = ∑ q : S, P.positive q

theorem EGZ.Expansion.Exchange.negativeAtoms_card {A : Type u_1} {S : Type u_2} [Fintype S] (P : ExchangePattern S) (atom : P.Position → A) (hinj : Function.Injective atom) : (negativeAtoms P atom).card = ∑ q : S, P.negative q

theorem EGZ.Expansion.Exchange.pattern_atoms_disjoint {A : Type u_1} {S : Type u_2} [Fintype S] (P : ExchangePattern S) (atom : P.Position → A) (hinj : Function.Injective atom) : Disjoint (positiveAtoms P atom) (negativeAtoms P atom)

theorem EGZ.Expansion.Exchange.positiveAtoms_sum {A : Type u_1} {S : Type u_2} [Fintype S] (P : ExchangePattern S) (atom : P.Position → A) (hinj : Function.Injective atom) {G : Type u_3} [AddCommMonoid G] (f : A → G) : ∑ a ∈ positiveAtoms P atom, f a = ∑ i : (q : S) × Fin (P.positive q), f (atom (Sum.inl i))

theorem EGZ.Expansion.Exchange.negativeAtoms_sum {A : Type u_1} {S : Type u_2} [Fintype S] (P : ExchangePattern S) (atom : P.Position → A) (hinj : Function.Injective atom) {G : Type u_3} [AddCommMonoid G] (f : A → G) : ∑ a ∈ negativeAtoms P atom, f a = ∑ i : (q : S) × Fin (P.negative q), f (atom (Sum.inr i))

noncomputable def EGZ.Expansion.Exchange.ofPattern {p r t : ℕ} {A : Type u_1} {S : Type u_2} [Fintype S] (P : ExchangePattern S) (point : A → FpCoord p (r + t)) (atom : P.Position → A) (hinj : Function.Injective atom) (label : S → FpCoord p r) (hatom : ∀ (i : P.Position), (Coord.first r t) (point (atom i)) = label (P.label i)) (hmass : ∑ q : S, P.positive q = ∑ q : S, P.negative q) (hlabel : ∑ q : S, P.positive q • label q = ∑ q : S, P.negative q • label q) {B : ℕ} (hsize : P.size ≤ B) : Exchange point B

Every injective balanced pattern is an actual exchange.

Equations

• EGZ.Expansion.Exchange.ofPattern P point atom hinj label hatom hmass hlabel hsize = ⟨(EGZ.Expansion.Exchange.positiveAtoms P atom, EGZ.Expansion.Exchange.negativeAtoms P atom), ⋯⟩

theorem EGZ.Expansion.Exchange.ofPattern_shift {p r t : ℕ} {A : Type u_1} {S : Type u_2} [Fintype S] (P : ExchangePattern S) (point : A → FpCoord p (r + t)) (atom : P.Position → A) (hinj : Function.Injective atom) (label : S → FpCoord p r) (hatom : ∀ (i : P.Position), (Coord.first r t) (point (atom i)) = label (P.label i)) (hmass : ∑ q : S, P.positive q = ∑ q : S, P.negative q) (hlabel : ∑ q : S, P.positive q • label q = ∑ q : S, P.negative q • label q) {B : ℕ} (hsize : P.size ≤ B) : (ofPattern P point atom hinj label hatom hmass hlabel hsize).shift = ∑ i : P.Position, P.sign i • (Coord.last r t) (point (atom i))

theorem EGZ.Expansion.Exchange.ofPattern_support_avoids {p r t : ℕ} {A : Type u_1} {S : Type u_2} [Fintype S] (P : ExchangePattern S) (point : A → FpCoord p (r + t)) (atom : P.Position → A) (hinj : Function.Injective atom) (label : S → FpCoord p r) (hatom : ∀ (i : P.Position), (Coord.first r t) (point (atom i)) = label (P.label i)) (hmass : ∑ q : S, P.positive q = ∑ q : S, P.negative q) (hlabel : ∑ q : S, P.positive q • label q = ∑ q : S, P.negative q • label q) {B : ℕ} (hsize : P.size ≤ B) (U : Finset A) (hU : ∀ (i : P.Position), atom i ∉ U) : Disjoint (ofPattern P point atom hinj label hatom hmass hlabel hsize).support U

theorem EGZ.Expansion.Exchange.relation_mass_eq {S : Type u_2} [Fintype S] (b : S → ℤ) (hb : ∑ q : S, b q = 0) : ∑ q : S, (ExchangePattern.ofRelation b).positive q = ∑ q : S, (ExchangePattern.ofRelation b).negative q

theorem EGZ.Expansion.Exchange.relation_label_eq {S : Type u_2} [Fintype S] {G : Type u_3} [AddCommGroup G] (b : S → ℤ) (label : S → G) (hb : ∑ q : S, b q • label q = 0) : ∑ q : S, (ExchangePattern.ofRelation b).positive q • label q = ∑ q : S, (ExchangePattern.ofRelation b).negative q • label q

theorem EGZ.Expansion.Exchange.relation_mod_sum {p r : ℕ} {S : Type u_2} [Fintype S] (b : S → ℤ) (label : S → IntCoord r) (hb : ∑ q : S, b q • label q = 0) : ∑ q : S, b q • IntCoord.mod p (label q) = 0

noncomputable def EGZ.Expansion.Exchange.ofRelation {p r t : ℕ} {A : Type u_1} {S : Type u_2} [Fintype S] (point : A → FpCoord p (r + t)) (b : S → ℤ) (label : S → IntCoord r) (atom : (ExchangePattern.ofRelation b).Position → A) (hinj : Function.Injective atom) (hb : ∑ q : S, b q = 0) (hlabel : ∑ q : S, b q • label q = 0) (hatom : ∀ (i : (ExchangePattern.ofRelation b).Position), (Coord.first r t) (point (atom i)) = IntCoord.mod p (label ((ExchangePattern.ofRelation b).label i))) {B : ℕ} (hsize : ∑ q : S, (b q).natAbs ≤ B) : Exchange point B

An injective sample of an integer affine relation gives a bounded exchange in the original atom family.

Equations

• One or more equations did not get rendered due to their size.

theorem EGZ.Expansion.Exchange.ofRelation_shift {p r t : ℕ} {A : Type u_1} {S : Type u_2} [Fintype S] [Finite A] (point : A → FpCoord p (r + t)) (b : S → ℤ) (label : S → IntCoord r) (atom : (ExchangePattern.ofRelation b).Position → A) (hinj : Function.Injective atom) (hb : ∑ q : S, b q = 0) (hlabel : ∑ q : S, b q • label q = 0) (hatom : ∀ (i : (ExchangePattern.ofRelation b).Position), (Coord.first r t) (point (atom i)) = IntCoord.mod p (label ((ExchangePattern.ofRelation b).label i))) {B : ℕ} (hsize : ∑ q : S, (b q).natAbs ≤ B) : (ofRelation point b label atom hinj hb hlabel hatom hsize).shift = ∑ i : (ExchangePattern.ofRelation b).Position, (ExchangePattern.ofRelation b).sign i • (Coord.last r t) (point (atom i))

theorem EGZ.Expansion.Exchange.ofRelation_support_avoids {p r t : ℕ} {A : Type u_1} {S : Type u_2} [Fintype S] [Finite A] (point : A → FpCoord p (r + t)) (b : S → ℤ) (label : S → IntCoord r) (atom : (ExchangePattern.ofRelation b).Position → A) (hinj : Function.Injective atom) (hb : ∑ q : S, b q = 0) (hlabel : ∑ q : S, b q • label q = 0) (hatom : ∀ (i : (ExchangePattern.ofRelation b).Position), (Coord.first r t) (point (atom i)) = IntCoord.mod p (label ((ExchangePattern.ofRelation b).label i))) {B : ℕ} (hsize : ∑ q : S, (b q).natAbs ≤ B) (U : Finset A) (hU : ∀ (i : (ExchangePattern.ofRelation b).Position), atom i ∉ U) : Disjoint (ofRelation point b label atom hinj hb hlabel hatom hsize).support U