Prescribed quotient counts

The integer coefficients give a natural multiplicity on the quotient. For a zero-dimensional fibre, this already proves relative expansion.

theorem EGZ.Expansion.mod_injective_on_support {p r K : ℕ} [NeZero p] (S : Finset (IntCoord r)) (hbox : ∀ q ∈ S, latticeSupNorm q ≤ K) (hKp : 2 * K < p) : Function.Injective fun (q : ↥S) => IntCoord.mod p ↑q

theorem EGZ.Expansion.pushWeight_le_of_injective {A : Type u_1} {B : Type u_2} [Fintype A] (f : A → B) (hf : Function.Injective f) (u : A → ℕ) (w : B → ℕ) (hu : ∀ (a : A), u a ≤ w (f a)) : pushWeight f u ≤ w

theorem EGZ.Expansion.prescribed_quotient_counts {p r t K : ℕ} [NeZero p] (S : Finset (IntCoord r)) (w : FpCoord p (r + t) → ℕ) (α : ↥S → ℤ) (hbox : ∀ q ∈ S, latticeSupNorm q ≤ K) (hKp : 2 * K < p) (hz : ∑ q : ↥S, α q • ↑q = 0) (hm : ∑ q : ↥S, α q = ↑p) (ha : ∀ (q : ↥S), 0 ≤ α q ∧ α q ≤ ↑(pushWeight (⇑(Coord.first r t)) w (IntCoord.mod p ↑q))) : ∃ a ≤ pushWeight (⇑(Coord.first r t)) w, natMass a = p ∧ vectorSum a = 0

theorem EGZ.Expansion.relativeExpansionAt_zero_fibre {p r K T : ℕ} [NeZero p] {δ : ℝ} (hδ : 0 < δ) (hKp : 2 * K < p) : RelativeExpansionAt r 0 K δ T p