Polynomial triangle removal in vector spaces

DefinitionTriangle-free subsets of \(\mathbb{F}_2^n\)#✓fully proved

A set \(A \subseteq \mathbb{F}_2^n\) is triangle-free if there are no \(x, y \in A\) with \(x + y \in A\) (the case \(x = y\) is allowed).

def IsTriangleFree {n : ℕ} (A : Finset (Fin n → ZMod 2)) : Prop :=
  ∀ x ∈ A, ∀ y ∈ A, x + y ∉ A

Used by 1

Used byPolynomial triangle removal in \(\mathbb{F}_2^n\)

DefinitionNumber of triangles in a subset of \(\mathbb{F}_2^n\)#✓fully proved

For \(A \subseteq \mathbb{F}_2^n\), the triangle count of \(A\) is the number of ordered pairs \((x, y) \in A \times A\) with \(x + y \in A\). Divided by \(4^n\), it is the probability that \(x, y, x + y \in A\) for independent uniform \(x, y \in \mathbb{F}_2^n\).

def triangleCount {n : ℕ} (A : Finset (Fin n → ZMod 2)) : ℕ :=
  ((A ×ˢ A).filter fun p => p.1 + p.2 ∈ A).card

Used by 1

Used byPolynomial triangle removal in \(\mathbb{F}_2^n\)

DefinitionPolynomial triangle removal in \(\mathbb{F}_2^n\)#✓fully proved

This is the statement that there are real constants \(c > 0\) and \(C > 0\) such that for every \(n\), every \(A \subseteq \mathbb{F}_2^n\) and every real \(\varepsilon\) with \(0 < \varepsilon \le 1\): if every triangle-free \(B \subseteq A\) misses at least \(\varepsilon 2^n\) elements of \(A\), then the triangle count of \(A\) is at least \(c \varepsilon^C 4^n\), that is, \(\Pr_{x,y}[x, y, x + y \in A] \ge c \varepsilon^C\) for independent uniform \(x, y \in \mathbb{F}_2^n\).

This is Green's question as posed by O'Donnell (Problem 14); the answer is yes.

def polynomialTriangleRemoval : Prop :=
  ∃ c C : ℝ, 0 < c ∧ 0 < C ∧ ∀ (n : ℕ) (A : Finset (Fin n → ZMod 2)) (ε : ℝ), 0 < ε → ε ≤ 1 →
    (∀ B ⊆ A, IsTriangleFree B → ε * 2 ^ n ≤ ((A \ B).card : ℝ)) →
      c * ε ^ C * 4 ^ n ≤ (triangleCount A : ℝ)

Uses 2 · Used by 1

Statement usesTriangle-free subsets of \(\mathbb{F}_2^n\) · Number of triangles in a subset of \(\mathbb{F}_2^n\)

Used byPolynomial triangle removal holds in \(\mathbb{F}_2^n\)

TheoremPolynomial triangle removal holds in \(\mathbb{F}_2^n\)#●ready to prove

There are real constants \(c > 0\) and \(C > 0\) such that for every natural number \(n\), every finite set \(A \subseteq \mathbb{F}_2^n\) and every real number \(\varepsilon\) with \(0 < \varepsilon \le 1\) the following holds: if every triangle-free \(B \subseteq A\) misses at least \(\varepsilon 2^n\) elements of \(A\), then the triangle count of \(A\) is at least \(c \varepsilon^C 4^n\). Here a set \(B \subseteq \mathbb{F}_2^n\) is triangle-free when there are no \(x, y \in B\) with \(x + y \in B\) (the case \(x = y\) is allowed), and the triangle count of \(A\) is the number of ordered pairs \((x, y) \in A \times A\) with \(x + y \in A\), so that it divided by \(4^n\) is the probability that \(x, y, x + y \in A\) for independent uniform \(x, y \in \mathbb{F}_2^n\).

This answers O'Donnell's Problem 14 in the affirmative. Fox and Lovász proved it with the essentially tight exponent \(C = 1 + 1/(5/3 - \log_2 3) \approx 13.239\).

public theorem_wanted polynomialTriangleRemoval_holds : polynomialTriangleRemoval

Sources

• R. O'Donnell, Open Problems in Analysis of Boolean Functions (2012), arXiv:1204.6447, Problem 14 (Triangle Removal in 𝔽₂ⁿ); resolution: J. Fox and L. M. Lovász, A tight bound for Green's arithmetic triangle removal lemma in vector spaces, Adv. Math. 321 (2017), 287-297, arXiv:1606.01230, Theorem 1: for 0 < ε < 1 and δ = (ε/3)^{C_p}, if X, Y, Z ⊆ 𝔽_pⁿ span fewer than δ N² triangles (N = pⁿ) then removing εN elements of X ∪ Y ∪ Z kills all triangles; C₂ = 1 + 1/(5/3 - log₂ 3) ≈ 13.239 (applied with X = Y = Z = A and p = 2; the case ε = 1 follows from ε < 1), https://arxiv.org/abs/1606.01230.

Uses 1

Statement usesPolynomial triangle removal in \(\mathbb{F}_2^n\)

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.