Ben Green's Open Problem 40

References:

• [Gr24] Ben Green's Open Problem 40
• [Da90] Davydov, Alexander Abramovich. "Construction of linear covering codes." Problemy Peredachi Informatsii 26.4 (1990): 38-55.
• [CHL97] Cohen, G., Honkala, I., Litsyn, S., & Lobstein, A. (1997). Covering codes (Vol. 54). Elsevier.
• [St94] R. Struik, Covering codes, PhD Thesis, Eindhoven University of Technology, the Netherlands, 106 pp, 1994.

@[reducible, inline]

abbrev Green40.𝔽₂ (n : ℕ) : Type

The vector space $\mathbb{F}_2^n$.

Equations

• Green40.𝔽₂ n = (Fin n → ZMod 2)

def Green40.hammingBall (n r : ℕ) : Set (𝔽₂ n)

The Hamming ball of radius $r$ in $\mathbb{F}_2^n$.

Equations

• Green40.hammingBall n r = {x : Green40.𝔽₂ n | hammingNorm x ≤ r}

def Green40.IsCoveringSubspace (n r : ℕ) (V : Submodule (ZMod 2) (𝔽₂ n)) : Prop

$V$ is a covering subspace of $\mathbb{F}_2^n$ by $H(r)$ if $V + H(r) = \mathbb{F}_2^n$.

Equations

• Green40.IsCoveringSubspace n r V = (↑V + Green40.hammingBall n r = Set.univ)

noncomputable def Green40.minDensity (n r : ℕ) : ENNReal

The minimal covering density over all covering subspaces for a given n and r. We compute in ℝ≥0∞ (ENNReal) to gracefully handle any potential divergence.

Equations

• Green40.minDensity n r = ⨅ (V : Submodule (ZMod 2) (Green40.𝔽₂ n)), ⨅ (_ : Green40.IsCoveringSubspace n r V), ↑(Nat.card ↥V) * ↑(Nat.card ↑(Green40.hammingBall n r)) / 2 ^ n

noncomputable def Green40.f (r : ℕ) : ENNReal

Let $f(r)$ be the smallest constant such that there exists an infinite sequence of $n$'s together with subspaces $V_n \leq \mathbb{F}_2^n$ with $V_n + H(r) = \mathbb{F}_2^n$ and $|V_n| = \left(f(r) + o(1)\right) \frac{2^n}{|H(r)|}$.

Equations

• Green40.f r = Filter.liminf (fun (n : ℕ) => Green40.minDensity n r) Filter.atTop

theorem Green40.green_40 : True ↔ Filter.Tendsto f Filter.atTop (nhds ⊤)

Does $f(r) \to \infty$? [Gr24]

theorem Green40.green_40.sanity_f_one : f 1 = 1

The only value known is $f(1) = 1$, which follows from the existence of the Hamming code [Gr24].

theorem Green40.green_40.upper_bound (r : ℕ) : f r ≤ ↑r ^ r / ↑r.factorial

$f(r) \le r^r / r! \sim e^r$ [Gr24].

theorem Green40.green_40.f_eq_one_for_all : True ↔ ∀ (r : ℕ), f r = 1

The possibility that f(r) = 1 for all r has not been ruled out [Gr24]

theorem Green40.green_40.f_two_eq_one : True ↔ f 2 = 1

It is not known whether f(2) = 1 [Gr24]

theorem Green40.green_40.upper_bound_f_two : f 2 ≤ 1.4238

The best-known upper bound for $f(2)$ is $1.4238$ [CHL97].

def Green40.hammingBallFinset (n r : ℕ) : Finset (𝔽₂ n)

Equations

• Green40.hammingBallFinset n r = {x : Green40.𝔽₂ n | hammingNorm x ≤ r}

def Green40.IsCoveringFinset (n r : ℕ) (V : Finset (𝔽₂ n)) : Prop

Equations

• Green40.IsCoveringFinset n r V = (V + Green40.hammingBallFinset n r = Finset.univ)

noncomputable def Green40.minDensityFinset (n r : ℕ) : ENNReal

Equations

• Green40.minDensityFinset n r = ⨅ (V : Finset (Green40.𝔽₂ n)), ⨅ (_ : Green40.IsCoveringFinset n r V), ↑V.card * ↑(Nat.card ↑(Green40.hammingBall n r)) / 2 ^ n

noncomputable def Green40.f_tilde (r : ℕ) : ENNReal

Equations

• Green40.f_tilde r = Filter.liminf (fun (n : ℕ) => Green40.minDensityFinset n r) Filter.atTop

theorem Green40.green_40.variants.arbitrary_subsets : True ↔ Filter.Tendsto f_tilde Filter.atTop (nhds ⊤)

Does $\tilde{f}(r) \to \infty$? [Gr24]

theorem Green40.green_40.variants.arbitrary_subsets_sanity_f_tilde_two : f_tilde 2 = 1

It is known that $\tilde{f}(2) = 1$ [St94].

theorem Green40.green_40.f_tilde_le_f (r : ℕ) : f_tilde r ≤ f r

We evidently have $\tilde{f}(r) \le f(r)$ [Gr24].

noncomputable def Green40.f_all (r : ℕ) : ENNReal

Equations

• Green40.f_all r = Filter.limsup (fun (n : ℕ) => Green40.minDensity n r) Filter.atTop

theorem Green40.green_40.variants.all_n : True ↔ Filter.Tendsto f_all Filter.atTop Filter.atTop

Does $f_{\text{all}}(r) \to \infty$? [Gr24]