feat(analysis/normed_space/finite_dimension): add a lemma about `inf_…

…dist` (#12282)

Add a version of `exists_mem_frontier_inf_dist_compl_eq_dist` for a
compact set in a real normed space. This version does not assume that
the ambient space is finite dimensional.

src/analysis/normed_space/finite_dimension.lean

@@ -621,9 +621,10 @@ begin
 end
 
 variable (𝕜)
-/-- Riesz's theorem: if the unit ball is compact in a vector space, then the space is
-finite-dimensional. -/
-theorem finite_dimensional_of_is_compact_closed_ball {r : ℝ} (rpos : 0 < r)
+
+/-- **Riesz's theorem**: if a closed ball with center zero of positive radius is compact in a vector
+space, then the space is finite-dimensional. -/
+theorem finite_dimensional_of_is_compact_closed_ball₀ {r : ℝ} (rpos : 0 < r)
   (h : is_compact (metric.closed_ball (0 : E) r)) : finite_dimensional 𝕜 E :=
 begin
   by_contra hfin,
@@ -653,6 +654,16 @@ begin
   ... < ∥c∥ : hN (N+1) (nat.le_succ N)
 end
 
+/-- **Riesz's theorem**: if a closed ball of positive radius is compact in a vector space, then the
+space is finite-dimensional. -/
+theorem finite_dimensional_of_is_compact_closed_ball {r : ℝ} (rpos : 0 < r) {c : E}
+  (h : is_compact (metric.closed_ball c r)) : finite_dimensional 𝕜 E :=
+begin
+  apply finite_dimensional_of_is_compact_closed_ball₀ 𝕜 rpos,
+  have : continuous (λ x, -c + x), from continuous_const.add continuous_id,
+  simpa using h.image this,
+end
+
 end riesz
 
 /-- An injective linear map with finite-dimensional domain is a closed embedding. -/
@@ -710,7 +721,8 @@ finite_dimensional.proper ℝ E
 
 /-- If `E` is a finite dimensional normed real vector space, `x : E`, and `s` is a neighborhood of
 `x` that is not equal to the whole space, then there exists a point `y ∈ frontier s` at distance
-`metric.inf_dist x sᶜ` from `x`. -/
+`metric.inf_dist x sᶜ` from `x`. See also
+`is_compact.exists_mem_frontier_inf_dist_compl_eq_dist`. -/
 lemma exists_mem_frontier_inf_dist_compl_eq_dist {E : Type*} [normed_group E]
   [normed_space ℝ E] [finite_dimensional ℝ E] {x : E} {s : set E} (hx : x ∈ s) (hs : s ≠ univ) :
   ∃ y ∈ frontier s, metric.inf_dist x sᶜ = dist x y :=
@@ -722,6 +734,26 @@ begin
   rwa dist_comm
 end
 
+/-- If `K` is a compact set in a nontrivial real normed space and `x ∈ K`, then there exists a point
+`y` of the boundary of `K` at distance `metric.inf_dist x Kᶜ` from `x`. See also
+`exists_mem_frontier_inf_dist_compl_eq_dist`. -/
+lemma is_compact.exists_mem_frontier_inf_dist_compl_eq_dist {E : Type*} [normed_group E]
+  [normed_space ℝ E] [nontrivial E] {x : E} {K : set E} (hK : is_compact K) (hx : x ∈ K) :
+  ∃ y ∈ frontier K, metric.inf_dist x Kᶜ = dist x y :=
+begin
+  obtain (hx'|hx') : x ∈ interior K ∪ frontier K,
+  { rw ← closure_eq_interior_union_frontier, exact subset_closure hx },
+  { rw [mem_interior_iff_mem_nhds, metric.nhds_basis_closed_ball.mem_iff] at hx',
+    rcases hx' with ⟨r, hr₀, hrK⟩,
+    haveI : finite_dimensional ℝ E,
+      from finite_dimensional_of_is_compact_closed_ball ℝ hr₀
+        (compact_of_is_closed_subset hK metric.is_closed_ball hrK),
+    exact exists_mem_frontier_inf_dist_compl_eq_dist hx hK.ne_univ },
+  { refine ⟨x, hx', _⟩,
+    rw frontier_eq_closure_inter_closure at hx',
+    rw [metric.inf_dist_zero_of_mem_closure hx'.2, dist_self] },
+end
+
 /-- In a finite dimensional vector space over `ℝ`, the series `∑ x, ∥f x∥` is unconditionally
 summable if and only if the series `∑ x, f x` is unconditionally summable. One implication holds in
 any complete normed space, while the other holds only in finite dimensional spaces. -/

src/topology/metric_space/hausdorff_distance.lean

@@ -475,6 +475,11 @@ variable {s}
 lemma inf_dist_eq_closure : inf_dist x (closure s) = inf_dist x s :=
 by simp [inf_dist, inf_edist_closure]
 
+/-- If a point belongs to the closure of `s`, then its infimum distance to `s` equals zero.
+The converse is true provided that `s` is nonempty, see `mem_closure_iff_inf_dist_zero`. -/
+lemma inf_dist_zero_of_mem_closure (hx : x ∈ closure s) : inf_dist x s = 0 :=
+by { rw ← inf_dist_eq_closure, exact inf_dist_zero_of_mem hx }
+
 /-- A point belongs to the closure of `s` iff its infimum distance to this set vanishes -/
 lemma mem_closure_iff_inf_dist_zero (h : s.nonempty) : x ∈ closure s ↔ inf_dist x s = 0 :=
 by simp [mem_closure_iff_inf_edist_zero, inf_dist, ennreal.to_real_eq_zero_iff, inf_edist_ne_top h]