Maybe an Erdos problem

Stream: general

[Nick_adfor]

Problem Set 2 B15

Let $S \subseteq \mathbb{Z}^2$. Define

$d_k(S) = \max_{\substack{A,B \subseteq \mathbb{Z} \\ |A| = |B| = k}} \frac{|S \cap (A \times B)|}{|A||B|}.$

Prove that $\lim_{k \to \infty} d_k(S)$ exists and always equals $0$ or $1$.

Source: Course Graph Theory and Additive Combinatorics by Yufei Zhao.

The problem I think might be like something already solved in Erdos problem but in fact it is from Yufei Zhao with no solution yet. As I'm trying to formalize something in combinatorics, I'd like to formalize this in Lean.

The most important work I'm focusing on is to formalize the article "The Polynomial Method and Restricted Sums of Congruence Classes" (https://web.math.princeton.edu/~nalon/PDFS/anrf3.pdf). Some related problems like this in combinatorics are seen as some juicy exercises.

[Kenny Lau]

$$double dollar signs$$

[Kevin Buzzard]

What does this have to do with Lean? (Edit:Question has since been edited)

[Riccardo Brasca]

Do you have a very precise pen and paper proof?

[Riccardo Brasca]

Anyway you can always start to formalize the statement

[Nick_adfor]

Kenny Lau said:

$$double dollar signs$$

Okay, I've fixed. I always forget zulip does not use $ but $$ (not like the one I'm familiar with on LaTeX)

[Nick_adfor]

Riccardo Brasca said:

Do you have a very precise pen and paper proof?

maybe

Existence of the limit:
The key is to show that the sequence $\log d_k(S)$ is approximately subadditive. By taking tensor products of two optimal $k \times k$ submatrices, one can construct a larger submatrix whose density is at least the product of the original densities. By Fekete’s lemma, the limit of $-\log d_k(S) / k$ exists, implying the limit of $d_k(S)$ also exists.

0–1 law:
Suppose the limit $\delta$ lies strictly between 0 and 1. Repeatedly applying the tensor product construction allows us to amplify the density arbitrarily close to 1, leading to a contradiction. Hence, the limit must be either 0 or 1.

[Nick_adfor]

And for the statement

import Mathlib

open Set Finset Filter

/-- For S ⊆ ℤ² and k ∈ ℕ, d_k(S) is the maximum density of S in a k × k grid. -/
noncomputable def density (S : ℤ × ℤ → Prop) [DecidablePred S] (k : ℕ) : ℝ :=
  if h : k = 0 then 0 else
  let sizeKSets := ((Finset.Icc (-(k : ℤ)) k).powerset.filter (λ A => A.card = k))
  have h_nonempty : sizeKSets.Nonempty := by sorry
  sizeKSets.sup' h_nonempty (λ A =>
    sizeKSets.sup' h_nonempty (λ B =>
      ((A ×ˢ B).filter S).card / ((k : ℝ) ^ 2)))

/-- The theorem: the limit of d_k(S) as k → ∞ exists and is either 0 or 1. -/
theorem limit_density_01 (S : ℤ × ℤ → Prop) [DecidablePred S] :
    ∃ L : ℝ, Tendsto (λ k => density S k) atTop (nhds L) ∧ (L = 0 ∨ L = 1) := by
  sorry

[Aaron Liu]

seems to be a slightly different statement (restricted to a square from -k to k)

[Nick_adfor]

Aaron Liu said:

seems to be a slightly different statement (restricted to a square from -k to k)

It is from a trick to fix the set in [-k, k] and let k->∞ in maths. But in fact now I don't know if it can work to let k->∞ in Lean

[Aaron Liu]

see this is why we need to be precise