mathlib documentation

analysis.normed_space.riesz_lemma

Riesz's lemma #

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 nondiscrete 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.

theorem riesz_lemma {𝕜 : Type u_1} [normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : subspace 𝕜 E} (hFc : is_closed F) (hF : ∃ (x : E), x F) {r : } (hr : r < 1) :
∃ (x₀ : E), x₀ F ∀ (y : E), y Fr * 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.

theorem riesz_lemma_of_norm_lt {𝕜 : Type u_1} [normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {c : 𝕜} (hc : 1 < c) {R : } (hR : c < R) {F : subspace 𝕜 E} (hFc : is_closed F) (hF : ∃ (x : E), x F) :
∃ (x₀ : E), x₀ R ∀ (y : E), y F1 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.

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