feat(analysis/convex/topology): add lemma `convex.subset_interior_ima…

…ge_homothety_of_one_lt` (#9044)





Co-authored-by: YaelDillies <yael.dillies@gmail.com>

src/analysis/convex/topology.lean

@@ -6,6 +6,7 @@ Authors: Alexander Bentkamp, Yury Kudriashov
 import analysis.convex.function
 import analysis.normed_space.finite_dimension
 import topology.path_connected
+import topology.algebra.affine
 
 /-!
 # Topological and metric properties of convex sets
@@ -138,6 +139,40 @@ lemma convex.add_smul_mem_interior {s : set E} (hs : convex ℝ s)
   x + t • y ∈ interior s :=
 by { convert hs.add_smul_sub_mem_interior hx hy ht, abel }
 
+open affine_map
+
+/-- If we dilate a convex set about a point in its interior by a scale `t > 1`, the interior of
+the result contains the original set.
+
+TODO Generalise this from convex sets to sets that are balanced / star-shaped about `x`. -/
+lemma convex.subset_interior_image_homothety_of_one_lt
+  {s : set E} (hs : convex ℝ s) {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) :
+  s ⊆ interior (image (homothety x t) s) :=
+begin
+  intros y hy,
+  let I := { z | ∃ (u : ℝ), u ∈ Ioc (0 : ℝ) 1 ∧ z = y + u • (x - y) },
+  have hI : I ⊆ interior s,
+  { rintros z ⟨u, hu, rfl⟩, exact hs.add_smul_sub_mem_interior hy hx hu, },
+  let z := homothety x t⁻¹ y,
+  have hz₁ : z ∈ interior s,
+  { suffices : z ∈ I, { exact hI this, },
+    use 1 - t⁻¹,
+    split,
+    { simp only [mem_Ioc, sub_le_self_iff, inv_nonneg, sub_pos, inv_lt_one ht, true_and],
+      linarith, },
+    { simp only [z, homothety_apply, sub_smul, smul_sub, vsub_eq_sub, vadd_eq_add, one_smul],
+      abel, }, },
+  have ht' : t ≠ 0, { linarith, },
+  have hz₂ : y = homothety x t z, { simp [z, ht', homothety_apply, smul_smul], },
+  rw hz₂,
+  rw mem_interior at hz₁ ⊢,
+  obtain ⟨U, hU₁, hU₂, hU₃⟩ := hz₁,
+  exact ⟨image (homothety x t) U,
+         image_subset ⇑(homothety x t) hU₁,
+         homothety_is_open_map x t ht' U hU₂,
+         mem_image_of_mem ⇑(homothety x t) hU₃⟩,
+end
+
 end has_continuous_smul
 
 /-! ### Normed vector space -/

src/topology/algebra/affine.lean

@@ -11,18 +11,19 @@ import linear_algebra.affine_space.affine_map
 
 For now, this contains only a few facts regarding the continuity of affine maps in the special
 case when the point space and vector space are the same.
+
+TODO: Deal with the case where the point spaces are different from the vector spaces.
 -/
 
+namespace affine_map
+
 variables {R E F : Type*}
-  [ring R]
-  [add_comm_group E] [module R E] [topological_space E]
-  [add_comm_group F] [module R F] [topological_space F] [topological_add_group F]
+variables [add_comm_group E] [topological_space E]
+variables [add_comm_group F] [topological_space F] [topological_add_group F]
 
-namespace affine_map
+section ring
 
-/-
-TODO: Deal with the case where the point spaces are different from the vector spaces.
--/
+variables [ring R] [module R E] [module R F]
 
 /-- An affine map is continuous iff its underlying linear map is continuous. -/
 lemma continuous_iff {f : E →ᵃ[R] F} :
@@ -46,4 +47,33 @@ lemma line_map_continuous [topological_space R] [has_continuous_smul R F] {p v :
 continuous_iff.mpr $ (continuous_id.smul continuous_const).add $
   @continuous_const _ _ _ _ (0 : F)
 
+end ring
+
+section comm_ring
+
+variables [comm_ring R] [module R F] [topological_space R] [has_continuous_smul R F]
+
+@[continuity]
+lemma homothety_continuous (x : F) (t : R) : continuous $ homothety x t :=
+begin
+  suffices : ⇑(homothety x t) = λ y, t • (y - x) + x, { rw this, continuity, },
+  ext y,
+  simp [homothety_apply],
+end
+
+end comm_ring
+
+section field
+
+variables [field R] [module R F] [topological_space R] [has_continuous_smul R F]
+
+lemma homothety_is_open_map (x : F) (t : R) (ht : t ≠ 0) : is_open_map $ homothety x t :=
+begin
+  apply is_open_map.of_inverse (homothety_continuous x t⁻¹);
+  intros e;
+  simp [← affine_map.comp_apply, ← homothety_mul, ht],
+end
+
+end field
+
 end affine_map