The Bannai-Bannai-Stanton bound on distance sets

Formalizes the Bannai-Bannai-Stanton theorem bounding the size of a distance set S in ℝ^d with s distinct distances by Nat.choose (d + s) s, following the short proof of Petrov and Pohoata via the Croot-Lev-Pach lemma.

def BannaiBannaiStanton.distanceSet {M : Type u_1} [MetricSpace M] (S : Set M) : Set ℝ

The set of distances realized between distinct points of a set S.

Equations

• BannaiBannaiStanton.distanceSet S = {r : ℝ | ∃ x ∈ S, ∃ y ∈ S, x ≠ y ∧ r = dist x y}

noncomputable def BannaiBannaiStanton.distPoly {R : Type u_1} [CommRing R] (d : ℕ) : MvPolynomial (Fin (2 * d)) R

The squared-distance polynomial used to encode pairwise distances of a distance set.

Equations

• BannaiBannaiStanton.distPoly d = ∑ i : Fin d, (MvPolynomial.X (Fin.castLE ⋯ i) - MvPolynomial.X ⟨d + ↑i, ⋯⟩) ^ 2

noncomputable def BannaiBannaiStanton.distPolyFrom {R : Type u_1} [CommRing R] {d : ℕ} (y : EuclideanSpace R (Fin d)) : MvPolynomial (Fin d) R

The squared-distance polynomial expressed from a fixed reference point.

Equations

• BannaiBannaiStanton.distPolyFrom y = ∑ i : Fin d, (MvPolynomial.X i - MvPolynomial.C (y.ofLp i)) ^ 2

noncomputable def BannaiBannaiStanton.productDistPoly {R : Type u_1} [CommRing R] (d : ℕ) (D : Finset R) : MvPolynomial (Fin (2 * d)) R

The product over a finite distance set of the shifted squared-distance polynomials.

Equations

• BannaiBannaiStanton.productDistPoly d D = ∏ r ∈ D, (MvPolynomial.C (r ^ 2) - BannaiBannaiStanton.distPoly d)

noncomputable def BannaiBannaiStanton.productDistPolyFrom {R : Type u_1} [CommRing R] {d : ℕ} (y : EuclideanSpace R (Fin d)) (D : Finset R) : MvPolynomial (Fin d) R

The product form of productDistPoly taken from a fixed reference point.

Equations

• BannaiBannaiStanton.productDistPolyFrom y D = ∏ r ∈ D, (MvPolynomial.C (r ^ 2) - BannaiBannaiStanton.distPolyFrom y)

theorem BannaiBannaiStanton.degree_distPolyFrom_le {R : Type u_1} [CommRing R] {d : ℕ} (y : EuclideanSpace R (Fin d)) : (distPolyFrom y).totalDegree ≤ 2

theorem BannaiBannaiStanton.degree_distPoly {R : Type u_1} [CommRing R] (d : ℕ) : (distPoly d).totalDegree ≤ 2

theorem BannaiBannaiStanton.degree_productDistPoly_le {R : Type u_1} [CommRing R] {d : ℕ} (D : Finset R) : (productDistPoly d D).totalDegree ≤ 2 * D.card

theorem BannaiBannaiStanton.degree_productDistPolyFrom_le {R : Type u_1} [CommRing R] {d : ℕ} (y : EuclideanSpace R (Fin d)) (D : Finset R) : (productDistPolyFrom y D).totalDegree ≤ 2 * D.card

theorem BannaiBannaiStanton.eval_distPoly_eq_eval_distPolyFrom {R : Type u_1} [CommRing R] {d : ℕ} (x y : EuclideanSpace R (Fin d)) : (MvPolynomial.eval (Fin.append x.ofLp y.ofLp ∘ Fin.cast ⋯)) (distPoly d) = (MvPolynomial.eval x.ofLp) (distPolyFrom y)

theorem BannaiBannaiStanton.eval_productDistPolyFrom_eq {R : Type u_1} [CommRing R] {d : ℕ} [IsDomain R] (y : EuclideanSpace R (Fin d)) (D : Finset R) (h_nul : 0 ∉ D) : (MvPolynomial.eval y.ofLp) (productDistPolyFrom y D) ≠ 0

theorem BannaiBannaiStanton.eval_productDistPolyFrom_ne {d : ℕ} (x y : EuclideanSpace ℝ (Fin d)) (D : Finset ℝ) (h_dist : dist x y ∈ D) : (MvPolynomial.eval x.ofLp) (productDistPolyFrom y D) = 0

theorem BannaiBannaiStanton.linearIndependent_of_eval_eq_zero {R : Type u_1} [CommRing R] {d : ℕ} [IsDomain R] {ι : Type u_2} (f : ι → MvPolynomial (Fin d) R) (p : ι → EuclideanSpace R (Fin d)) (h_diag : ∀ (i : ι), (MvPolynomial.eval (p i).ofLp) (f i) ≠ 0) (h_off : ∀ (i j : ι), i ≠ j → (MvPolynomial.eval (p j).ofLp) (f i) = 0) : LinearIndependent R f

theorem BannaiBannaiStanton.finite_distance_set_imp_finite_set {d : ℕ} (S : Set (EuclideanSpace ℝ (Fin d))) (hdis_fin : (distanceSet S).Finite) : S.Finite

noncomputable def BannaiBannaiStanton.evalMapRestricted {F : Type u_1} [Field F] {d : ℕ} (A : Finset (EuclideanSpace F (Fin d))) (s : ℕ) : ↥(MvPolynomial.restrictTotalDegree (Fin d) F s) →ₗ[F] ↥A → F

Evaluation of restricted polynomials as a linear map on bounded-degree monomials.

Equations

• BannaiBannaiStanton.evalMapRestricted A s = { toFun := fun (p : ↥(MvPolynomial.restrictTotalDegree (Fin d) F s)) (a : ↥A) => (MvPolynomial.eval (↑a).ofLp) ↑p, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def BannaiBannaiStanton.dim {F : Type u_1} [Field F] {d : ℕ} (A : Finset (EuclideanSpace F (Fin d))) (s : ℕ) : ℕ

The dimension of the space of polynomials of bounded total degree used in the rank bound.

Equations

• BannaiBannaiStanton.dim A s = Module.finrank F ↥(BannaiBannaiStanton.evalMapRestricted A s).range

noncomputable def BannaiBannaiStanton.finsuppToMultisetRestricted {d s : ℕ} : ↑{f : Fin d →₀ ℕ | (f.sum fun (x : Fin d) (n : ℕ) => n) ≤ s} ≃ { m : Multiset (Fin d) // m.card ≤ s }

Sends a bounded-degree monomial exponent vector to its multiset of variables.

Equations

• BannaiBannaiStanton.finsuppToMultisetRestricted = Multiset.toFinsupp.symm.subtypeEquiv ⋯

theorem BannaiBannaiStanton.card_filterMap_eq_countP {α : Type u_2} {β : Type u_3} (f : α → Option β) (s : Multiset α) : (Multiset.filterMap f s).card = Multiset.countP (fun (a : α) => (f a).isSome = true) s

theorem BannaiBannaiStanton.multiset_decomposition_option {α : Type u_2} [DecidableEq α] (m : Multiset (Option α)) : m = Multiset.map some (Multiset.filterMap id m) + Multiset.replicate (Multiset.count none m) none

def BannaiBannaiStanton.multisetToSymOption {d s : ℕ} : { m : Multiset (Fin d) // m.card ≤ s } ≃ Sym (Option (Fin d)) s

Encodes a degree-s multiset over Fin d in a symmetric power of Option (Fin d).

Equations

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

@[implicit_reducible]

noncomputable instance BannaiBannaiStanton.fintypeMonomialsBoundedDegree {d s : ℕ} : Fintype ↑{f : Fin d →₀ ℕ | (f.sum fun (x : Fin d) (n : ℕ) => n) ≤ s}

Equations

• BannaiBannaiStanton.fintypeMonomialsBoundedDegree = Fintype.ofEquiv (Sym (Option (Fin d)) s) (BannaiBannaiStanton.finsuppToMultisetRestricted.trans BannaiBannaiStanton.multisetToSymOption).symm

theorem BannaiBannaiStanton.restrictTotalDegree_finrank {F : Type u_1} [Field F] {d : ℕ} (s : ℕ) : Module.finrank F ↥(MvPolynomial.restrictTotalDegree (Fin d) F s) = (d + s).choose s

theorem BannaiBannaiStanton.dim_le_min_card_and_binom {F : Type u_1} [Field F] {d : ℕ} (A : Finset (EuclideanSpace F (Fin d))) (s : ℕ) : dim A s ≤ (d + s).choose s

theorem BannaiBannaiStanton.orthogonal_complement_dimension {F : Type u_1} [Field F] {d : ℕ} [DecidableEq (EuclideanSpace F (Fin d))] (A : Finset (EuclideanSpace F (Fin d))) (s : ℕ) : have Ω_F_A_s := (evalMapRestricted A s).range; have B := (Matrix.toBilin (Pi.basisFun F ↥A)) 1; A.card = Module.finrank F ↥(Submodule.comap B Ω_F_A_s.dualAnnihilator) + dim A s

theorem BannaiBannaiStanton.eval_split {F : Type u_1} [Field F] {d : ℕ} (m : Fin (2 * d) →₀ ℕ) (a b : EuclideanSpace F (Fin d)) : have h_cast := ⋯; have m_left := fun (m : Fin (2 * d) →₀ ℕ) => Finsupp.equivFunOnFinite.symm fun (i : Fin d) => m (Fin.cast ⋯ (Fin.castAdd d i)); have m_right := fun (m : Fin (2 * d) →₀ ℕ) => Finsupp.equivFunOnFinite.symm fun (i : Fin d) => m (Fin.cast ⋯ (Fin.natAdd d i)); (MvPolynomial.eval (Fin.append a.ofLp b.ofLp ∘ Fin.cast ⋯)) ((MvPolynomial.monomial m) 1) = (MvPolynomial.eval a.ofLp) ((MvPolynomial.monomial (m_left m)) 1) * (MvPolynomial.eval b.ofLp) ((MvPolynomial.monomial (m_right m)) 1)

theorem BannaiBannaiStanton.bilinear_form_vanishes_on_orthogonal_complement {F : Type u_1} [Field F] {d : ℕ} [DecidableEq (EuclideanSpace F (Fin d))] (A : Finset (EuclideanSpace F (Fin d))) (s : ℕ) (p : MvPolynomial (Fin (2 * d)) F) (hp_deg : p.totalDegree ≤ 2 * s + 1) : have B := (Matrix.toBilin (Pi.basisFun F ↥A)) 1; have Ω_F_A_s_orth := Submodule.comap B (evalMapRestricted A s).range.dualAnnihilator; have M := fun (a b : ↥A) => (MvPolynomial.eval (Fin.append (↑a).ofLp (↑b).ofLp ∘ Fin.cast ⋯)) p; have Φ_P_A := (Matrix.toBilin (Pi.basisFun F ↥A)) M; ∀ f ∈ Ω_F_A_s_orth, ∀ g ∈ Ω_F_A_s_orth, (Φ_P_A f) g = 0

theorem BannaiBannaiStanton.matrix_rank_add_le {F : Type u_1} [Field F] {n : Type u_2} [Fintype n] (A B : Matrix n n F) : (A + B).rank ≤ A.rank + B.rank

theorem BannaiBannaiStanton.Croot_Lev_Pach_lemma_generalised_1st_part {F : Type u_1} [Field F] {d : ℕ} (A : Finset (EuclideanSpace F (Fin d))) (s : ℕ) (p : MvPolynomial (Fin (2 * d)) F) (hp_deg : p.totalDegree ≤ 2 * s + 1) : have M := fun (a b : ↥A) => (MvPolynomial.eval (Fin.append (↑a).ofLp (↑b).ofLp ∘ Fin.cast ⋯)) p; M.rank ≤ 2 * dim A s

theorem BannaiBannaiStanton.Croot_Lev_Pach_lemma_generalised_2nd_part {F : Type u_1} [Field F] {d : ℕ} [LinearOrder F] [IsStrictOrderedRing F] (A : Finset (EuclideanSpace F (Fin d))) {s : ℕ} (p : MvPolynomial (Fin (2 * d)) F) (hp_deg : p.totalDegree ≤ 2 * s + 1) : have M := fun (a b : ↥A) => (MvPolynomial.eval (Fin.append (↑a).ofLp (↑b).ofLp ∘ Fin.cast ⋯)) p; have Q := fun (v : ↥A → F) => ∑ a : ↥A, ∑ b : ↥A, v a * M a b * v b; (∀ (V : Submodule F (↥A → F)), (∀ v ∈ V, v ≠ 0 → Q v > 0) → Module.finrank F ↥V ≤ dim A s) ∧ ∀ (V : Submodule F (↥A → F)), (∀ v ∈ V, v ≠ 0 → Q v < 0) → Module.finrank F ↥V ≤ dim A s

theorem BannaiBannaiStanton.bannai_bannai_stanton_bound {d s : ℕ} (S : Set (EuclideanSpace ℝ (Fin d))) (hdis : (distanceSet S).Finite) (hs : s = hdis.toFinset.card) : S.encard ≤ ↑((d + s).choose s)