English
A nat-version of the corners theorem: for any ε > 0 and large enough n meeting cornersTheoremBound(ε/9) ≤ n, any A ⊆ range n × range n with ε n^2 ≤ #A is not corner-free in ℕ × ℕ.
Русский
Версия теоремы Корнера для натуральных чисел: при любом ε > 0 и достаточном большом n, удовлетворяющем cornersTheoremBound(ε/9) ≤ n, для любого A ⊆ range(n) × range(n) с ε n^2 ≤ |A| абсолютной величины, A не безугловой в ℕ × ℕ.
LaTeX
$$$\forall \varepsilon>0,\ h_{\varepsilon}: 0<\varepsilon,\ h_n: cornersTheoremBound(\varepsilon/9) \le n,\ A \subseteq range\ n \times range\ n,\ h_{A\varepsilon}: \varepsilon \cdot n^2 \le |A| \Rightarrow \neg IsCornerFree(A : Set(\mathbb{N}\times\mathbb{N})).$$$
Lean4
/-- The **corners theorem** for `ℕ`.
The maximum density of a corner-free set in `{1, ..., n} × {1, ..., n}` goes to zero as `n` tends to
infinity. -/
theorem corners_theorem_nat (hε : 0 < ε) (hn : cornersTheoremBound (ε / 9) ≤ n) (A : Finset (ℕ × ℕ))
(hAn : A ⊆ range n ×ˢ range n) (hAε : ε * n ^ 2 ≤ #A) : ¬IsCornerFree (A : Set (ℕ × ℕ)) :=
by
rintro hA
rw [← coe_subset, coe_product] at hAn
have :
A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' A : Set (Fin (2 * n).succ × Fin (2 * n).succ)) :=
by
rw [Set.image_image, Set.image_congr, Set.image_id]
simp only [mem_coe, Nat.succ_eq_add_one, Prod.map_apply, Fin.val_natCast, id_eq, Prod.forall, Prod.mk.injEq,
Nat.mod_succ_eq_iff_lt]
rintro a b hab
have := hAn hab
simp at this
omega
rw [this] at hA
have := Fin.isAddFreimanIso_Iio two_ne_zero (le_refl (2 * n))
have :=
hA.of_image this.isAddFreimanHom Fin.val_injective.injOn <|
by
refine Set.image_subset_iff.2 <| hAn.trans fun x hx ↦ ?_
simp only [coe_range, Set.mem_prod, Set.mem_Iio] at hx
exact ⟨Fin.natCast_strictMono (by cutsat) hx.1, Fin.natCast_strictMono (by cutsat) hx.2⟩
rw [← coe_image] at this
refine corners_theorem (ε / 9) (by positivity) (by simp; cutsat) _ ?_ this
calc
_ = ε / 9 * (2 * n + 1) ^ 2 := by simp
_ ≤ ε / 9 * (2 * n + n) ^ 2 := by gcongr; simp; unfold cornersTheoremBound at hn; cutsat
_ = ε * n ^ 2 := by ring
_ ≤ #A := hAε
_ = _ := by
rw [card_image_of_injOn]
have : Set.InjOn Nat.cast (range n) :=
(CharP.natCast_injOn_Iio (Fin (2 * n).succ) (2 * n).succ).mono (by simp; cutsat)
exact (this.prodMap this).mono hAn
