Statement of relative expansion

RelativeExpansionStatement is the proposition corresponding to the paper's Theorem thexp. Its proof is relative_expansion_theorem in EGZ.Expansion.RelativeProof. This separate statement module also lets the main assembly expose its analytic dependencies explicitly.

The multisets X_q are encoded by one multiplicity function on the product coordinates. The first-coordinate support condition records their labels. The harmless condition 2 * K < p makes those integer labels distinct modulo p; it can always be absorbed into the prime threshold.

The paper's "linear functions" are affine functionals, consistently with its slab definition and with the functional constructed in its proof.

def EGZ.Expansion.RelativeExpansionAt (r t K : ℕ) (δ : ℝ) (T p : ℕ) [NeZero p] : Prop

A single instance of the relative expansion conclusion, at the stated dimension, box, thickness, width, and prime.

Equations

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

def EGZ.Expansion.RelativeExpansionStatement : Prop

The relative expansion theorem, with its uniform quantifier order. Neither threshold depends on T, p, the support, the multiplicities, or the selected coefficients.

Equations

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

theorem EGZ.Expansion.RelativeExpansionStatement.thresholds (h : RelativeExpansionStatement) (r t K : ℕ) (hK : 1 ≤ K) (δ : ℝ) (hδ : 0 < δ) : ∃ (T₀ : ℕ) (p₀ : ℕ), 2 * K < p₀ ∧ ∀ (T : ℕ), T₀ ≤ T → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (x : NeZero p), p₀ ≤ p → RelativeExpansionAt r t K δ T p

A usable threshold can include injectivity of reduction on the box.

theorem EGZ.Expansion.RelativeExpansionAt.mono_width {r t K T T' p : ℕ} [NeZero p] {δ : ℝ} (h : RelativeExpansionAt r t K δ T p) (hT : T ≤ T') : RelativeExpansionAt r t K δ T' p

A theorem at a smaller slab width applies at every larger width.

theorem EGZ.Expansion.RelativeExpansionAt.of_nat_coefficients {r t K T p : ℕ} [NeZero p] {δ : ℝ} (h : RelativeExpansionAt r t K δ T p) (S : Finset (IntCoord r)) (w : FpCoord p (r + t) → ℕ) (α : ↥S → ℕ) (hbox : ∀ q ∈ S, latticeSupNorm q ≤ K) (hs : ∀ (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) (ha : ∀ (q : ↥S), δ * ↑p ≤ ↑(α q) ∧ ↑(α q) ≤ ↑(pushWeight (⇑(Coord.first r t)) w (IntCoord.mod p ↑q)) - δ * ↑p) (hthick : IsThickRelative w (⇑(Coord.first r t)) T δ) : HasZeroSumMultiplicity w

Natural coefficients, as produced by balanced convex combinations, are a special case of the integer coefficients in the paper.