English
If s ⊆ E is closed and strictly convex, then the frontier of s contains no nontrivial 3-term arithmetic progressions; i.e., the frontier is ThreeAPFree.
Русский
Если s ⊆ E замкнуто и строго выпукло, то граница s не содержит ненулевых арифметических прогрессий из трех членов; то есть frontier(s) является ThreeAPFree.
LaTeX
$$$$ \text{ThreeAPFree}(\mathrm{frontier}(s)) $$$$
Lean4
/-- The frontier of a closed strictly convex set only contains trivial arithmetic progressions.
The idea is that an arithmetic progression is contained on a line and the frontier of a strictly
convex set does not contain lines. -/
theorem threeAPFree_frontier {𝕜 E : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace E]
[AddCommMonoid E] [Module 𝕜 E] {s : Set E} (hs₀ : IsClosed s) (hs₁ : StrictConvex 𝕜 s) : ThreeAPFree (frontier s) :=
by
intro a ha b hb c hc habc
obtain rfl : (1 / 2 : 𝕜) • a + (1 / 2 : 𝕜) • c = b := by
rwa [← smul_add, one_div, inv_smul_eq_iff₀ (show (2 : 𝕜) ≠ 0 by simp), two_smul]
have := hs₁.eq (hs₀.frontier_subset ha) (hs₀.frontier_subset hc) one_half_pos one_half_pos (add_halves _) hb.2
simp [this, ← add_smul]
ring_nf
simp
