feat(combinatorics/additive/salem_spencer): The sphere does not conta…

…in arithmetic progressions (#13259)

Prove that the frontier of a strictly convex closed set is Salem-Spencer. For this we need
* simple lemmas about `same_ray`. This involves renaming `same_ray.exists_right_eq_smul`/`same_ray.exists_left_eq_smul` to `same_ray.exists_nonneg_left`/`same_ray.exists_nonneg_right`.
* that the norm in a real normed space is injective on rays.
* that the midpoint of two points of equal norm has smaller norm, in a strictly convex space

src/analysis/convex/strict.lean

@@ -36,7 +36,7 @@ interior. This basically means "convex and not flat on the boundary". -/
 def strict_convex : Prop :=
 s.pairwise $ λ x y, ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ interior s
 
-variables {𝕜 s} {x y : E}
+variables {𝕜 s} {x y : E} {a b : 𝕜}
 
 lemma strict_convex_iff_open_segment_subset :
   strict_convex 𝕜 s ↔ s.pairwise (λ x y, open_segment 𝕜 x y ⊆ interior s) :=
@@ -56,6 +56,10 @@ begin
   exact mem_univ _,
 end
 
+protected lemma strict_convex.eq (hs : strict_convex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) (ha : 0 < a)
+  (hb : 0 < b) (hab : a + b = 1) (h : a • x + b • y ∉ interior s) : x = y :=
+hs.eq hx hy $ λ H, h $ H ha hb hab
+
 protected lemma strict_convex.inter {t : set E} (hs : strict_convex 𝕜 s) (ht : strict_convex 𝕜 t) :
   strict_convex 𝕜 (s ∩ t) :=
 begin

src/analysis/convex/strict_convex_space.lean

@@ -156,8 +156,18 @@ inequality for `x` and `y` becomes an equality. -/
 lemma same_ray_iff_norm_add : same_ray ℝ x y ↔ ∥x + y∥ = ∥x∥ + ∥y∥ :=
 ⟨same_ray.norm_add, λ h, not_not.1 $ λ h', (norm_add_lt_of_not_same_ray h').ne h⟩
 
+/-- In a strictly convex space, two vectors `x`, `y` are not in the same ray if and only if the
+triangle inequality for `x` and `y` is strict. -/
+lemma not_same_ray_iff_norm_add_lt : ¬ same_ray ℝ x y ↔ ∥x + y∥ < ∥x∥ + ∥y∥ :=
+same_ray_iff_norm_add.not.trans (norm_add_le _ _).lt_iff_ne.symm
+
 /-- In a strictly convex space, the triangle inequality turns into an equality if and only if the
 middle point belongs to the segment joining two other points. -/
 lemma dist_add_dist_eq_iff : dist x y + dist y z = dist x z ↔ y ∈ [x -[ℝ] z] :=
 by simp only [mem_segment_iff_same_ray, same_ray_iff_norm_add, dist_eq_norm',
   sub_add_sub_cancel', eq_comm]
+
+lemma norm_midpoint_lt_iff (h : ∥x∥ = ∥y∥) : ∥(1/2 : ℝ) • (x + y)∥ < ∥x∥ ↔ x ≠ y :=
+by rw [norm_smul, real.norm_of_nonneg (one_div_nonneg.2 zero_le_two), ←inv_eq_one_div,
+    ←div_eq_inv_mul, div_lt_iff (@zero_lt_two ℝ _ _), mul_two, ←not_same_ray_iff_of_norm_eq h,
+    not_same_ray_iff_norm_add_lt, h]

src/analysis/normed_space/ray.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yury Kudryashov
+Authors: Yury Kudryashov, Yaël Dillies
 -/
 import linear_algebra.ray
 import analysis.normed_space.basic
@@ -14,6 +14,8 @@ this case, for two vectors `x y` in the same ray, the norm of their sum is equal
 norms and `∥y∥ • x = ∥x∥ • y`.
 -/
 
+open real
+
 variables {E : Type*} [semi_normed_group E] [normed_space ℝ E]
   {F : Type*} [normed_group F] [normed_space ℝ F]
 
@@ -51,14 +53,32 @@ end
 
 end same_ray
 
-lemma same_ray_iff_norm_smul_eq {x y : F} :
-  same_ray ℝ x y ↔ ∥x∥ • y = ∥y∥ • x :=
+variables {x y : F}
+
+lemma norm_inj_on_ray_left (hx : x ≠ 0) : {y | same_ray ℝ x y}.inj_on norm :=
+begin
+  rintro y hy z hz h,
+  obtain rfl | hz' := eq_or_ne z 0,
+  { rwa [norm_zero, norm_eq_zero] at h },
+  have hy' : y ≠ 0,
+  { rwa [←norm_ne_zero_iff, ←h, norm_ne_zero_iff] at hz' },
+  obtain ⟨r, hr, rfl⟩ := hy.exists_pos_left hx hy',
+  obtain ⟨s, hs, rfl⟩ := hz.exists_pos_left hx hz',
+  simp_rw [norm_smul, mul_left_inj' (norm_ne_zero_iff.2 hx), norm_of_nonneg hr.le,
+    norm_of_nonneg hs.le] at h,
+  rw h,
+end
+
+lemma norm_inj_on_ray_right (hy : y ≠ 0) : {x | same_ray ℝ x y}.inj_on norm :=
+by simpa only [same_ray_comm] using norm_inj_on_ray_left hy
+
+lemma same_ray_iff_norm_smul_eq : same_ray ℝ x y ↔ ∥x∥ • y = ∥y∥ • x :=
 ⟨same_ray.norm_smul_eq, λ h, or_iff_not_imp_left.2 $ λ hx, or_iff_not_imp_left.2 $ λ hy,
   ⟨∥y∥, ∥x∥, norm_pos_iff.2 hy, norm_pos_iff.2 hx, h.symm⟩⟩
 
 /-- Two nonzero vectors `x y` in a real normed space are on the same ray if and only if the unit
 vectors `∥x∥⁻¹ • x` and `∥y∥⁻¹ • y` are equal. -/
-lemma same_ray_iff_inv_norm_smul_eq_of_ne {x y : F} (hx : x ≠ 0) (hy : y ≠ 0) :
+lemma same_ray_iff_inv_norm_smul_eq_of_ne (hx : x ≠ 0) (hy : y ≠ 0) :
   same_ray ℝ x y ↔ ∥x∥⁻¹ • x = ∥y∥⁻¹ • y :=
 begin
   have : ∥x∥⁻¹ * ∥y∥⁻¹ ≠ 0, by simp *,
@@ -71,10 +91,20 @@ alias same_ray_iff_inv_norm_smul_eq_of_ne ↔ same_ray.inv_norm_smul_eq _
 
 /-- Two vectors `x y` in a real normed space are on the ray if and only if one of them is zero or
 the unit vectors `∥x∥⁻¹ • x` and `∥y∥⁻¹ • y` are equal. -/
-lemma same_ray_iff_inv_norm_smul_eq {x y : F} :
-  same_ray ℝ x y ↔ x = 0 ∨ y = 0 ∨ ∥x∥⁻¹ • x = ∥y∥⁻¹ • y :=
+lemma same_ray_iff_inv_norm_smul_eq : same_ray ℝ x y ↔ x = 0 ∨ y = 0 ∨ ∥x∥⁻¹ • x = ∥y∥⁻¹ • y :=
 begin
   rcases eq_or_ne x 0 with rfl|hx, { simp [same_ray.zero_left] },
   rcases eq_or_ne y 0 with rfl|hy, { simp [same_ray.zero_right] },
   simp only [same_ray_iff_inv_norm_smul_eq_of_ne hx hy, *, false_or]
 end
+
+lemma same_ray_iff_of_norm_eq (h : ∥x∥ = ∥y∥) : same_ray ℝ x y ↔ x = y :=
+begin
+  obtain rfl | hy := eq_or_ne y 0,
+  { rw [norm_zero, norm_eq_zero] at h,
+    exact iff_of_true (same_ray.zero_right _) h },
+  { exact ⟨λ hxy, norm_inj_on_ray_right hy hxy same_ray.rfl h, λ hxy, hxy ▸ same_ray.rfl⟩ }
+end
+
+lemma not_same_ray_iff_of_norm_eq (h : ∥x∥ = ∥y∥) : ¬ same_ray ℝ x y ↔ x ≠ y :=
+(same_ray_iff_of_norm_eq h).not

src/combinatorics/additive/salem_spencer.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
 import analysis.asymptotics.asymptotics
+import analysis.convex.strict_convex_space
 
 /-!
 # Salem-Spencer sets and Roth numbers
@@ -35,9 +36,9 @@ Can `add_salem_spencer_iff_eq_right` be made more general?
 Salem-Spencer, Roth, arithmetic progression, average, three-free
 -/
 
-open finset nat
+open finset metric nat
 
-variables {α β : Type*}
+variables {α β 𝕜 E : Type*}
 
 section salem_spencer
 section monoid
@@ -219,6 +220,31 @@ begin
 end
 
 end nat
+
+/-- 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. -/
+lemma add_salem_spencer_frontier [linear_ordered_field 𝕜] [topological_space E] [add_comm_monoid E]
+  [module 𝕜 E] {s : set E} (hs₀ : is_closed s) (hs₁ : strict_convex 𝕜 s) :
+  add_salem_spencer (frontier s) :=
+begin
+  intros a b c ha hb hc habc,
+  obtain rfl : (1 / 2 : 𝕜) • a + (1 / 2 : 𝕜) • b = c,
+  { rwa [←smul_add, one_div, inv_smul_eq_iff₀ (show (2 : 𝕜) ≠ 0, by norm_num), two_smul] },
+  exact hs₁.eq (hs₀.frontier_subset ha) (hs₀.frontier_subset hb) one_half_pos one_half_pos
+    (add_halves _) hc.2,
+end
+
+lemma add_salem_spencer_sphere [normed_group E] [normed_space ℝ E] [strict_convex_space ℝ E] (x : E)
+  (r : ℝ) : add_salem_spencer (sphere x r) :=
+begin
+  obtain rfl | hr := eq_or_ne r 0,
+  { rw sphere_zero,
+    exact add_salem_spencer_singleton _ },
+  { convert add_salem_spencer_frontier is_closed_ball (strict_convex_closed_ball ℝ x r),
+    exact (frontier_closed_ball _ hr).symm }
+end
+
 end salem_spencer
 
 section roth_number

src/linear_algebra/ray.lean

@@ -59,6 +59,8 @@ begin
   exact or.inr (or.inr $ ⟨1, 1, zero_lt_one, zero_lt_one, rfl⟩)
 end
 
+protected lemma rfl : same_ray R x x := refl _
+
 /-- `same_ray` is symmetric. -/
 @[symm] lemma symm (h : same_ray R x y) : same_ray R y x :=
 (or.left_comm.1 h).imp_right $ or.imp_right $ λ ⟨r₁, r₂, h₁, h₂, h⟩, ⟨r₂, r₁, h₂, h₁, h.symm⟩
@@ -472,24 +474,30 @@ end linear_ordered_comm_ring
 namespace same_ray
 
 variables {R : Type*} [linear_ordered_field R]
-variables {M : Type*} [add_comm_group M] [module R M] {v₁ v₂ : M}
+variables {M : Type*} [add_comm_group M] [module R M] {x y v₁ v₂ : M}
+
+lemma exists_pos_left (h : same_ray R x y) (hx : x ≠ 0) (hy : y ≠ 0) :
+  ∃ r : R, 0 < r ∧ r • x = y :=
+let ⟨r₁, r₂, hr₁, hr₂, h⟩ := h.exists_pos hx hy in
+  ⟨r₂⁻¹ * r₁, mul_pos (inv_pos.2 hr₂) hr₁, by rw [mul_smul, h, inv_smul_smul₀ hr₂.ne']⟩
+
+lemma exists_pos_right (h : same_ray R x y) (hx : x ≠ 0) (hy : y ≠ 0) :
+  ∃ r : R, 0 < r ∧ x = r • y :=
+(h.symm.exists_pos_left hy hx).imp $ λ _, and.imp_right eq.symm
 
 /-- If a vector `v₂` is on the same ray as a nonzero vector `v₁`, then it is equal to `c • v₁` for
 some nonnegative `c`. -/
-lemma exists_right_eq_smul (h : same_ray R v₁ v₂) (h₀ : v₁ ≠ 0) :
-  ∃ c : R, 0 ≤ c ∧ v₂ = c • v₁ :=
+lemma exists_nonneg_left (h : same_ray R x y) (hx : x ≠ 0) : ∃ r : R, 0 ≤ r ∧ r • x = y :=
 begin
-  rcases h.resolve_left h₀ with (rfl|⟨r₁, r₂, hr₁, hr₂, H⟩),
-  { exact ⟨0, le_rfl, (zero_smul _ _).symm⟩ },
-  { refine ⟨r₁ / r₂, div_nonneg hr₁.le hr₂.le, _⟩,
-    rwa [div_eq_inv_mul, mul_smul, H, inv_smul_smul₀ hr₂.ne'] }
+  obtain rfl | hy := eq_or_ne y 0,
+  { exact ⟨0, le_rfl, zero_smul _ _⟩ },
+  { exact (h.exists_pos_left hx hy).imp (λ _, and.imp_left le_of_lt) }
 end
 
 /-- If a vector `v₁` is on the same ray as a nonzero vector `v₂`, then it is equal to `c • v₂` for
 some nonnegative `c`. -/
-lemma exists_left_eq_smul (h : same_ray R v₁ v₂) (h₀ : v₂ ≠ 0) :
-  ∃ c : R, 0 ≤ c ∧ v₁ = c • v₂ :=
-h.symm.exists_right_eq_smul h₀
+lemma exists_nonneg_right (h : same_ray R x y) (hy : y ≠ 0) : ∃ r : R, 0 ≤ r ∧ x = r • y :=
+(h.symm.exists_nonneg_left hy).imp $ λ _, and.imp_right eq.symm
 
 /-- If vectors `v₁` and `v₂` are on the same ray, then for some nonnegative `a b`, `a + b = 1`, we
 have `v₁ = a • (v₁ + v₂)` and `v₂ = b • (v₁ + v₂)`. -/

src/topology/basic.lean

@@ -529,6 +529,9 @@ by rw [closure_compl, frontier, diff_eq]
 
 lemma frontier_subset_closure {s : set α} : frontier s ⊆ closure s := diff_subset _ _
 
+lemma is_closed.frontier_subset (hs : is_closed s) : frontier s ⊆ s :=
+frontier_subset_closure.trans hs.closure_eq.subset
+
 lemma frontier_closure_subset {s : set α} : frontier (closure s) ⊆ frontier s :=
 diff_subset_diff closure_closure.subset $ interior_mono subset_closure