Checked proofs of the independent Palomar statements

This module deliberately does not import Challenge. The definitions below are the same independent definitions, and the bridge lemmas identify their constants with the ones used by the full EGZ proof.

def PalomarEGZ.zeroSumProperty (p d n : ℕ) : Prop

Every length-n sequence in (ZMod p)^d has p distinct positions whose vectors sum to zero. Repeated vector values are allowed.

Equations

• PalomarEGZ.zeroSumProperty p d n = ∀ (a : Fin n → Fin d → ZMod p), ∃ (I : Finset (Fin n)), I.card = p ∧ ∑ i ∈ I, a i = 0

def PalomarEGZ.isHollow (p : ℕ) {d s : ℕ} (v : Fin s → Fin d → ZMod p) : Prop

A family is p-hollow if a nonnegative integer combination of total weight p sums to zero exactly when one member receives all the weight. At primes this condition forces the family to have no repeated vectors.

Equations

• PalomarEGZ.isHollow p v = ∀ (α : Fin s → ℕ), ∑ i : Fin s, α i = p → (∑ i : Fin s, α i • v i = 0 ↔ ∃ (i : Fin s), α i = p)

noncomputable def PalomarEGZ.egzConstant (p d : ℕ) : ℕ

The Erdős–Ginzburg–Ziv constant: the least length at which every sequence has a p-term zero sum. For prime p this defining set is nonempty, by pigeonhole with the bound (p-1) * p^d + 1.

Equations

• PalomarEGZ.egzConstant p d = sInf {n : ℕ | PalomarEGZ.zeroSumProperty p d n}

noncomputable def PalomarEGZ.hollowConstant (p d : ℕ) : ℕ

The maximum size of a p-hollow family. For prime p, admitted lengths are nonempty and bounded by p^d, so this natural supremum is attained. Only prime values are used below; Mathlib's total natural supremum also assigns a value at degenerate moduli where these lengths may be unbounded.

Equations

• PalomarEGZ.hollowConstant p d = sSup {s : ℕ | ∃ (v : Fin s → Fin d → ZMod p), PalomarEGZ.isHollow p v}

def PalomarEGZ.atTopAlongPrimes : Filter ℕ

Tending to infinity through prime natural numbers.

Equations

• PalomarEGZ.atTopAlongPrimes = Filter.atTop ⊓ Filter.principal {p : ℕ | Nat.Prime p}

theorem PalomarEGZ.egzConstant_eq (p d : ℕ) : egzConstant p d = EGZ.egzConstant p d

theorem PalomarEGZ.hollowConstant_eq {p d : ℕ} (hp : Nat.Prime p) : hollowConstant p d = EGZ.hollowConstant p d

theorem PalomarEGZ.theorem_1_2 (d : ℕ) (hd : 0 < d) : (fun (p : ℕ) => ↑(egzConstant p d) - ↑p * ↑(hollowConstant p d)) =o[atTopAlongPrimes] fun (p : ℕ) => ↑p

Theorem 1.2: for each fixed positive dimension, s((F_p)^d) = p * w((F_p)^d) + o(p) as p tends to infinity through primes.

theorem PalomarEGZ.main_upper_bound (d : ℕ) (hd : 0 < d) (ε : ℝ) : 0 < ε → ∀ᶠ (p : ℕ) in atTopAlongPrimes, ↑(egzConstant p d) ≤ (↑(hollowConstant p d) + ε) * ↑p

The corresponding upper estimate: for each positive error ε, every sufficiently large prime satisfies s((F_p)^d) ≤ (w((F_p)^d) + ε) p.