Furstenberg–Sárközy theorem

DefinitionInitial segment count#✓fully proved

For a set \(A\) of natural numbers and a natural number \(N\), the initial segment count of \(A\) at \(N\) is the number of elements of \(A\) that are less than \(N\), that is, \(|A \cap \{0, 1, \dots, N - 1\}|\).

noncomputable def initialSegmentCount (A : Set ℕ) (N : ℕ) : ℕ :=
  by classical exact ((Finset.range N).filter (fun n => n ∈ A)).card

Used by 1

Used byFurstenberg–Sárközy theorem

TheoremFurstenberg–Sárközy theorem#✓fully proved

Let \(A\) be a set of natural numbers, and suppose there is a real number \(\delta > 0\) such that for every natural number \(M\) there is a natural number \(N \ge M\) with \(\delta N \le |A \cap \{0, 1, \dots, N - 1\}|\). Then there are \(a, b \in A\) and a natural number \(k > 0\) with \(a < b\) and \(b = a + k^2\).

public theorem furstenberg_sarkozy :
    ∀ A : Set ℕ,
      (∃ δ : ℝ, 0 < δ ∧ ∀ M : ℕ, ∃ N : ℕ, M ≤ N ∧
        δ * (N : ℝ) ≤ ((initialSegmentCount A N : ℕ) : ℝ)) →
      ∃ a b k : ℕ, a ∈ A ∧ b ∈ A ∧ 0 < k ∧ a < b ∧ b = a + k * k

Sources

• A. Sárközy, Acta Math. Acad. Sci. Hungar. 31 (1978) and H. Furstenberg, J. Analyse Math. 31 (1977); Lean states positive upper density via initialSegmentCount with arbitrarily large N.

Uses 1

Statement usesInitial segment count

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.