feat(topology/algebra/affine): a sufficiently small dilation of a point in the interior of a set lands in the interior (#13766)

Formalized as part of the Sphere Eversion project.

Author: ocfnash

src/algebra/add_torsor.lean

@@ -114,6 +114,9 @@ equal. -/
 @[simp] lemma vsub_eq_zero_iff_eq {p1 p2 : P} : p1 -ᵥ p2 = (0 : G) ↔ p1 = p2 :=
 iff.intro eq_of_vsub_eq_zero (λ h, h ▸ vsub_self _)
 
+lemma vsub_ne_zero {p q : P} : p -ᵥ q ≠ (0 : G) ↔ p ≠ q :=
+not_congr vsub_eq_zero_iff_eq
+
 /-- Cancellation adding the results of two subtractions. -/
 @[simp] lemma vsub_add_vsub_cancel (p1 p2 p3 : P) : p1 -ᵥ p2 + (p2 -ᵥ p3) = (p1 -ᵥ p3) :=
 begin
@@ -129,6 +132,9 @@ begin
   rw [vsub_add_vsub_cancel, vsub_self],
 end
 
+lemma vadd_vsub_eq_sub_vsub (g : G) (p q : P) : g +ᵥ p -ᵥ q = g - (q -ᵥ p) :=
+by rw [vadd_vsub_assoc, sub_eq_add_neg, neg_vsub_eq_vsub_rev]
+
 /-- Subtracting the result of adding a group element produces the same result
 as subtracting the points and subtracting that group element. -/
 lemma vsub_vadd_eq_vsub_sub (p1 p2 : P) (g : G) : p1 -ᵥ (g +ᵥ p2) = (p1 -ᵥ p2) - g :=

src/analysis/normed/group/basic.lean

@@ -256,6 +256,9 @@ lemma norm_le_add_norm_add (u v : E) :
 calc ∥u∥ = ∥u + v - v∥ : by rw add_sub_cancel
 ... ≤ ∥u + v∥ + ∥v∥ : norm_sub_le _ _
 
+lemma ball_eq (y : E) (ε : ℝ) : metric.ball y ε = { x | ∥x - y∥ < ε} :=
+by { ext, simp [dist_eq_norm], }
+
 lemma ball_zero_eq (ε : ℝ) : ball (0 : E) ε = {x | ∥x∥ < ε} :=
 set.ext $ assume a, by simp
 
@@ -425,6 +428,20 @@ lemma normed_group.cauchy_seq_iff [nonempty α] [semilattice_sup α] {u : α →
   cauchy_seq u ↔ ∀ ε > 0, ∃ N, ∀ m, N ≤ m → ∀ n, N ≤ n → ∥u m - u n∥ < ε :=
 by simp [metric.cauchy_seq_iff, dist_eq_norm]
 
+lemma normed_group.nhds_basis_norm_lt (x : E) :
+  (𝓝 x).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), { y | ∥y - x∥ < ε }) :=
+begin
+  simp_rw ← ball_eq,
+  exact metric.nhds_basis_ball,
+end
+
+lemma normed_group.nhds_zero_basis_norm_lt :
+  (𝓝 (0 : E)).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), { y | ∥y∥ < ε }) :=
+begin
+  convert normed_group.nhds_basis_norm_lt (0 : E),
+  simp,
+end
+
 lemma normed_group.uniformity_basis_dist :
   (𝓤 E).has_basis (λ (ε : ℝ), 0 < ε) (λ ε, {p : E × E | ∥p.fst - p.snd∥ < ε}) :=
 begin

src/analysis/normed_space/add_torsor.lean

@@ -24,11 +24,11 @@ variables {W Q : Type*} [normed_group W] [metric_space Q] [normed_add_torsor W Q
 
 section normed_space
 
-variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 V]
+variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 V] [normed_space 𝕜 W]
 
 open affine_map
 
-lemma affine_subspace.is_closed_direction_iff [normed_space 𝕜 W] (s : affine_subspace 𝕜 Q) :
+lemma affine_subspace.is_closed_direction_iff (s : affine_subspace 𝕜 Q) :
   is_closed (s.direction : set W) ↔ is_closed (s : set Q) :=
 begin
   rcases s.eq_bot_or_nonempty with rfl|⟨x, hx⟩, { simp [is_closed_singleton] },
@@ -60,15 +60,6 @@ lemma lipschitz_with_line_map (p₁ p₂ : P) :
 lipschitz_with.of_dist_le_mul $ λ c₁ c₂,
   ((dist_line_map_line_map p₁ p₂ c₁ c₂).trans (mul_comm _ _)).le
 
-omit V
-
-lemma antilipschitz_with_line_map [normed_space 𝕜 W] {p₁ p₂ : Q} (h : p₁ ≠ p₂) :
-  antilipschitz_with (nndist p₁ p₂)⁻¹ (line_map p₁ p₂ : 𝕜 → Q) :=
-antilipschitz_with.of_le_mul_dist $ λ c₁ c₂, by rw [dist_line_map_line_map, nnreal.coe_inv,
-  ← dist_nndist, mul_left_comm, inv_mul_cancel (dist_ne_zero.2 h), mul_one]
-
-include V
-
 @[simp] lemma dist_line_map_left (p₁ p₂ : P) (c : 𝕜) :
   dist (line_map p₁ p₂ c) p₁ = ∥c∥ * dist p₁ p₂ :=
 by simpa only [line_map_apply_zero, dist_zero_right] using dist_line_map_line_map p₁ p₂ c 0
@@ -93,6 +84,8 @@ by rw [homothety_eq_line_map, dist_line_map_right]
   dist p₂ (homothety p₁ c p₂) = ∥1 - c∥ * dist p₁ p₂ :=
 by rw [dist_comm, dist_homothety_self]
 
+section invertible_two
+
 variables [invertible (2:𝕜)]
 
 @[simp] lemma dist_left_midpoint (p₁ p₂ : P) :
@@ -120,6 +113,40 @@ begin
   exact div_le_div_of_le_of_nonneg (norm_add_le _ _) (norm_nonneg _),
 end
 
+end invertible_two
+
+omit V
+include W
+
+lemma antilipschitz_with_line_map {p₁ p₂ : Q} (h : p₁ ≠ p₂) :
+  antilipschitz_with (nndist p₁ p₂)⁻¹ (line_map p₁ p₂ : 𝕜 → Q) :=
+antilipschitz_with.of_le_mul_dist $ λ c₁ c₂, by rw [dist_line_map_line_map, nnreal.coe_inv,
+  ← dist_nndist, mul_left_comm, inv_mul_cancel (dist_ne_zero.2 h), mul_one]
+
+lemma eventually_homothety_mem_of_mem_interior (x : Q) {s : set Q} {y : Q} (hy : y ∈ interior s) :
+  ∀ᶠ δ in 𝓝 (1 : 𝕜), homothety x δ y ∈ s :=
+begin
+  rw (normed_group.nhds_basis_norm_lt (1 : 𝕜)).eventually_iff,
+  cases eq_or_ne y x with h h, { use 1, simp [h.symm, interior_subset hy], },
+  have hxy : 0 < ∥y -ᵥ x∥, { rwa [norm_pos_iff, vsub_ne_zero], },
+  obtain ⟨u, hu₁, hu₂, hu₃⟩ := mem_interior.mp hy,
+  obtain ⟨ε, hε, hyε⟩ := metric.is_open_iff.mp hu₂ y hu₃,
+  refine ⟨ε / ∥y -ᵥ x∥, div_pos hε hxy, λ δ (hδ : ∥δ - 1∥ < ε / ∥y -ᵥ x∥), hu₁ (hyε _)⟩,
+  rw [lt_div_iff hxy, ← norm_smul, sub_smul, one_smul] at hδ,
+  rwa [homothety_apply, metric.mem_ball, dist_eq_norm_vsub W, vadd_vsub_eq_sub_vsub],
+end
+
+lemma eventually_homothety_image_subset_of_finite_subset_interior
+  (x : Q) {s : set Q} {t : set Q} (ht : t.finite) (h : t ⊆ interior s) :
+  ∀ᶠ δ in 𝓝 (1 : 𝕜), homothety x δ '' t ⊆ s :=
+begin
+  suffices : ∀ y ∈ t, ∀ᶠ δ in 𝓝 (1 : 𝕜), homothety x δ y ∈ s,
+  { simp_rw set.image_subset_iff,
+    exact (filter.eventually_all_finite ht).mpr this, },
+  intros y hy,
+  exact eventually_homothety_mem_of_mem_interior x (h hy),
+end
+
 end normed_space
 
 variables [normed_space ℝ V] [normed_space ℝ W]