riesz_lemma_of_norm_lt
theorem riesz_lemma_of_norm_lt :
∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
{c : 𝕜},
1 < ‖c‖ →
∀ {R : ℝ},
‖c‖ < R → ∀ {F : Subspace 𝕜 E}, IsClosed ↑F → (∃ x, x ∉ F) → ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖
The theorem `riesz_lemma_of_norm_lt` is a variant of the Riesz lemma in the field of functional analysis. It states that given a strictly closed subspace `F` of a normed space `E` over a non-trivially normed field `𝕜`, and a constant `R` that is strictly larger than the norm of an element `c` of `𝕜` with norm greater than `1`, one can find an element `x₀` in `E` with norm less than or equal to `R` such that the distance between `x₀` and any element `y` in `F` is at least `1`. This theorem is particularly useful when considering a non-trivially normed field where there might be a gap in possible norms. In such cases, `R` cannot be arbitrarily close to `1` and therefore, the condition `R > ‖c‖` is required.
More concisely: Given a strictly closed subspace of a normed space over a non-trivially normed field and a constant strictly larger than the norm of an element with norm greater than 1, there exists an element with norm less than or equal to the constant and distance greater than 1 to any element in the subspace.
|
riesz_lemma
theorem riesz_lemma :
∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
{F : Subspace 𝕜 E}, IsClosed ↑F → (∃ x, x ∉ F) → ∀ {r : ℝ}, r < 1 → ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
The theorem is a formalization of Riesz's lemma in the field of functional analysis. In simpler terms, Riesz's Lemma states that given a closed proper subspace (F) of a normed space over a field (E), and given a real number (r) less than 1, we can always find a vector (x₀) that is not in the subspace (F), such that the distance of this vector (x₀) to the subspace (F) is at least r times the norm of the vector (x₀). In other words, the vector is almost orthogonal to the subspace, where the degree of 'orthogonality' is controlled by the real number r. This theorem is often used in functional analysis to prove that infinite dimensional normed spaces aren't locally compact.
More concisely: Given a closed proper subspace of a normed space and a real number less than 1, there exists a vector outside the subspace with distance to it being norm greater than the vector's norm multiplied by the real number.
|