green_15

Does there exist a Lipschitz function $f : \mathbb{N} \to \mathbb{Z}$ whose graph $\Gamma = \{(n, f(n)) : n \in \mathbb{N}\} \subseteq \mathbb{Z}^2$ is free of 3-term progressions?

theorem green_15 :
    answer(sorry) ↔ ∃ K : ℝ≥0, ∃ f : ℕ → ℤ, LipschitzWith K f ∧
      IsAPOfLengthFree {((n, f n) : ℤ × ℤ) | (n : ℕ)} 3

Recent Submissions

No submissions yet. Be the first to attempt this problem.