module
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.Data.Nat.Cast.Order.Field
public section
/-!
# USA Mathematical Olympiad 2002, Problem 6
I have an n×n sheet of stamps, from which I've been asked to tear out blocks
of three adjacent stamps in a single row or column. (I can only tear along the
perforations separating adjacent stamps, and each block must come out of the
sheet in one piece.) Let b(n) be the smallest number of blocks I can tear out
and make it impossible to tear out any more blocks. Prove that there are real
constants c and d such that
(1/7)n² - cn ≤ b(n) ≤ (1/5)n² - dn
for all n > 0.
-/
namespace Usa2002P6
/-- A horizontal block: three adjacent stamps in a single row. -/
def hblock (i j : ℕ) : Finset (ℕ × ℕ) := {(i, j), (i, j + 1), (i, j + 2)}
/-- A vertical block: three adjacent stamps in a single column. -/
def vblock (i j : ℕ) : Finset (ℕ × ℕ) := {(i, j), (i + 1, j), (i + 2, j)}
/-- A block that can be torn out of the n×n sheet. -/
def IsBlock (n : ℕ) (s : Finset (ℕ × ℕ)) : Prop :=
(∃ i j, i < n ∧ j + 2 < n ∧ s = hblock i j) ∨
(∃ i j, i + 2 < n ∧ j < n ∧ s = vblock i j)
/-- A tearing-out of pairwise disjoint blocks from the n×n sheet which makes it
impossible to tear out any more blocks. -/
def IsMaximalTearing (n : ℕ) (T : Finset (Finset (ℕ × ℕ))) : Prop :=
(∀ s ∈ T, IsBlock n s) ∧
(∀ s ∈ T, ∀ t ∈ T, s ≠ t → Disjoint s t) ∧
(∀ s, IsBlock n s → ∃ t ∈ T, ¬ Disjoint s t)
/-- A wasteful maximal tearing: fill the sheet with vertical blocks, column by
column, and fill the leftover bottom rows with horizontal blocks. Used to show
that a maximal tearing always exists (and for the upper bound at small `n`). -/
def trivialTearing (n : ℕ) : Finset (Finset (ℕ × ℕ)) :=
(Finset.range (n / 3) ×ˢ Finset.range n).image (fun p => vblock (3 * p.1) p.2) ∪
(Finset.range (n % 3) ×ˢ Finset.range (n / 3)).image
(fun p => hblock (3 * (n / 3) + p.1) (3 * p.2))
/-- The phase of row `i` in the efficient tearing pattern: in row `i`, the torn
blocks start at columns congruent to `phase i` modulo 5. -/
def phase (i : ℕ) : ℕ := i % 5
/-- The blocks torn out of row `i` in the efficient tearing pattern. -/
def patRowTearing (n i : ℕ) : Finset (Finset (ℕ × ℕ)) :=
((Finset.range (n / 5 + 1)).filter fun k => phase i + 5 * k + 2 < n).image
(fun k => hblock i (phase i + 5 * k)) ∪
(if 3 ≤ phase i then {hblock i 0} else ∅) ∪
(if 3 ≤ (n + 2 - phase i) % 5 then {hblock i (n - 3)} else ∅)
/-- The efficient maximal tearing, with asymptotic density n²/5. -/
def patTearing (n : ℕ) : Finset (Finset (ℕ × ℕ)) :=
(Finset.range n).biUnion fun i => patRowTearing n i
/-- `cov n i j` means that cell `(i, j)` is torn out by the efficient pattern. -/
def cov (n i j : ℕ) : Prop :=
(3 ≤ phase i ∧ j ≤ 2) ∨
(phase i ≤ j ∧ (j - phase i) % 5 ≤ 2 ∧ j - (j - phase i) % 5 + 2 < n) ∨
(3 ≤ (n + 2 - phase i) % 5 ∧ n - 3 ≤ j)
/-- `b n`: the smallest number of blocks one can tear out of an n×n sheet of
stamps (tearing out whole blocks of three adjacent stamps in a single row or
column) making it impossible to tear out any more blocks. -/
noncomputable def b (n : ℕ) : ℕ :=
open Classical in Nat.find (exists_maximalTearing n)
/-- **USAMO 2002, Problem 6.** There are real constants `c` and `d` such that
`(1/7)n² - cn ≤ b(n) ≤ (1/5)n² - dn` for all `n > 0`. Here we take `c = 2/7`
and `d = -3`. -/
theorem usa2002_p6 :
∃ c d : ℝ, ∀ n : ℕ, 0 < n →
(n : ℝ) ^ 2 / 7 - c * n ≤ (b n : ℝ) ∧ (b n : ℝ) ≤ (n : ℝ) ^ 2 / 5 - d * n := sorry
end Usa2002P6
This problem has a complete formalized solution.