Applications of the Hausdorff distance in normed spaces

Riesz's lemma, stated for a normed space over a normed field: for any closed proper subspace F of E, there is a nonzero x such that ‖x - F‖ is at least r * ‖x‖ for any r < 1. This is riesz_lemma.

In a nontrivially normed field (with an element c of norm > 1) and any R > ‖c‖, one can guarantee ‖x‖ ≤ R and ‖x - y‖ ≥ 1 for any y in F. This is riesz_lemma_of_norm_lt.

For a normed space over an RCLike field, one can find an element of norm exactly 1 with the same property. This is riesz_lemma_one.

A further lemma, Metric.closedBall_infDist_compl_subset_closure, finds a closed ball within the closure of a set s of optimal distance from a point in x to the frontier of s.

theorem riesz_lemma {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Subspace 𝕜 E} (hFc : IsClosed ↑F) (hF : ∃ (x : E), x ∉ F) {r : ℝ} (hr : r < 1) : ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖

Riesz's lemma, which usually states that it is possible to find a vector with norm 1 whose distance to a closed proper subspace is arbitrarily close to 1. The statement here is in terms of multiples of norms, since in general the existence of an element of norm exactly 1 is not guaranteed. For a variant giving an element with norm in [1, R], see riesz_lemma_of_norm_lt, and for a variant giving an element with norm exactly one assuming stronger assumptions on the underlying field, see riesz_lemma_of_lt_one.

theorem riesz_lemma_of_norm_lt {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : 𝕜} (hc : 1 < ‖c‖) {R : ℝ} (hR : ‖c‖ < R) {F : Subspace 𝕜 E} (hFc : IsClosed ↑F) (hF : ∃ (x : E), x ∉ F) : ∃ (x₀ : E), ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖

A version of Riesz lemma: given a strict closed subspace F, one may find an element of norm ≤ R which is at distance at least 1 of every element of F. Here, R is any given constant strictly larger than the norm of an element of norm > 1. For a version without an R, see riesz_lemma, and for a variant giving an element with norm exactly one assuming stronger assumptions on the underlying field, see riesz_lemma_of_lt_one.

Since we are considering a general nontrivially normed field, there may be a gap in possible norms (for instance no element of norm in (1,2)). Hence, we cannot allow R arbitrarily close to 1, and require R > ‖c‖ for some c : 𝕜 with norm > 1.

theorem Metric.closedBall_infDist_compl_subset_closure {F : Type u_3} [SeminormedAddCommGroup F] [NormedSpace ℝ F] {x : F} {s : Set F} (hx : x ∈ s) : closedBall x (infDist x sᶜ) ⊆ closure s

theorem riesz_lemma_of_lt_one {𝕜 : Type u_4} [RCLike 𝕜] {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Subspace 𝕜 E} (hFc : IsClosed ↑F) (hF : ∃ (x : E), x ∉ F) {r : ℝ} (hr : r < 1) : ∃ x₀ ∉ F, ‖x₀‖ = 1 ∧ ∀ y ∈ F, r ≤ ‖x₀ - y‖

A version of Riesz lemma: given a proper closed subspace F, one may find an element of norm 1 which is at distance at least r of every element of F, for any r < 1. For a version with weaker assumptions on the underlying field, see riesz_lemma or riesz_lemma_of_norm_lt.