Converting exchange coverage to multiplicity bounds

noncomputable def EGZ.Expansion.selectionWeight {A : Type u_1} {G : Type u_2} [Fintype A] (point : A → G) (J : Finset A) : G → ℕ

The multiplicity of each point among the atoms of a finite selection.

Equations

• EGZ.Expansion.selectionWeight point J = EGZ.Expansion.pushWeight point fun (a : A) => if a ∈ J then 1 else 0

theorem EGZ.Expansion.natMass_selectionWeight {A : Type u_1} {G : Type u_2} [Fintype A] [Fintype G] (point : A → G) (J : Finset A) : natMass (selectionWeight point J) = J.card

theorem EGZ.Expansion.vectorSum_selectionWeight {A : Type u_1} {G : Type u_2} [Fintype A] [Fintype G] [AddCommMonoid G] (point : A → G) (J : Finset A) : vectorSum (selectionWeight point J) = ∑ a ∈ J, point a

theorem EGZ.Expansion.exchange_position_capacity {A : Type u_1} [Finite A] {p r t B : ℕ} (point : A → FpCoord p (r + t)) (F : Finset (Exchange point B)) (hF : (↑F).Pairwise fun (e f : Exchange point B) => Disjoint e.support f.support) : ((∑ e : ↥F, fun (a : A) => if a ∈ (↑e).left then 1 else 0) + ∑ e : ↥F, fun (a : A) => if a ∈ (↑e).right then 1 else 0) ≤ fun (a : A) => if a ∈ usedAtoms Exchange.support F then 1 else 0

theorem EGZ.Expansion.exchange_weight_capacity {A : Type u_1} [Fintype A] {p r t B : ℕ} (point : A → FpCoord p (r + t)) (F : Finset (Exchange point B)) (hF : (↑F).Pairwise fun (e f : Exchange point B) => Disjoint e.support f.support) : ∑ e : ↥F, selectionWeight point (↑e).left + ∑ e : ↥F, selectionWeight point (↑e).right ≤ selectionWeight point (usedAtoms Exchange.support F)

theorem EGZ.Expansion.exchange_difference_coverage {A : Type u_1} [Fintype A] {p r t B : ℕ} [NeZero p] (point : A → FpCoord p (r + t)) (F : Finset (Exchange point B)) (hF : binarySums Exchange.shift F = Finset.univ) (v : FpCoord p (r + t)) : (Coord.first r t) v = 0 → ∃ (c : ↥F → Bool), (∑ e : ↥F, if c e = true then vectorSum (selectionWeight point (↑e).left) - vectorSum (selectionWeight point (↑e).right) else 0) = v

theorem EGZ.Expansion.pushWeight_le_natMass {X : Type u_1} {Y : Type u_2} [Fintype X] (f : X → Y) (u : X → ℕ) (y : Y) : pushWeight f u y ≤ natMass u

Each quotient fibre contains at most the total mass.

theorem EGZ.Expansion.selectionWeight_le_all {A : Type u_1} {G : Type u_2} [Fintype A] (point : A → G) (J : Finset A) : selectionWeight point J ≤ pushWeight point fun (x : A) => 1

theorem EGZ.Expansion.complete_exchange_resources {A : Type u_1} [Fintype A] {p r t B : ℕ} [NeZero p] (point : A → FpCoord p (r + t)) (w : FpCoord p (r + t) → ℕ) (hpoint : (pushWeight point fun (x : A) => 1) ≤ w) (F : Finset (Exchange point B)) (hF : (↑F).Pairwise fun (e f : Exchange point B) => Disjoint e.support f.support) (hcover : binarySums Exchange.shift F = Finset.univ) (a : FpCoord p r → ℕ) (hale : a ≤ pushWeight (⇑(Coord.first r t)) w) (ham : natMass a = p) (haz : vectorSum a = 0) {R : ℝ} (hused : ↑(usedAtoms Exchange.support F).card ≤ R) (hmargin : ∀ (q : Fin r → ZMod p), pushWeight (⇑(Coord.first r t)) w q ≠ 0 → R ≤ ↑(a q) ∧ ↑(a q) + R ≤ ↑(pushWeight (⇑(Coord.first r t)) w q)) : HasZeroSumMultiplicity w

Full coverage by disjoint exchanges gives a zero-sum submultiset when the reserved positions fit inside the margins of the prescribed counts.

theorem EGZ.Expansion.prescribed_quotient_counts_with_margin {p r t : ℕ} [NeZero p] (S : Finset (IntCoord r)) (w : FpCoord p (r + t) → ℕ) (α : ↥S → ℤ) (hinj : Function.Injective fun (q : ↥S) => IntCoord.mod p ↑q) (hsupport : ∀ (v : FpCoord p (r + t)), w v ≠ 0 → ∃ q ∈ S, (Coord.first r t) v = IntCoord.mod p q) (hz : ∑ q : ↥S, α q • ↑q = 0) (hm : ∑ q : ↥S, α q = ↑p) {R : ℝ} (hR : 0 ≤ R) (hmargin : ∀ (q : ↥S), R ≤ ↑(α q) ∧ ↑(α q) + R ≤ ↑(pushWeight (⇑(Coord.first r t)) w (IntCoord.mod p ↑q))) : ∃ a ≤ pushWeight (⇑(Coord.first r t)) w, natMass a = p ∧ vectorSum a = 0 ∧ ∀ (q : Fin r → ZMod p), pushWeight (⇑(Coord.first r t)) w q ≠ 0 → R ≤ ↑(a q) ∧ ↑(a q) + R ≤ ↑(pushWeight (⇑(Coord.first r t)) w q)

The prescribed integer coefficients give quotient multiplicities with the same real margins on every nonempty quotient fibre.