English
Let E be a normed space over a nontrivial normed field 𝕜, and F ⊆ E a closed subspace. If there exists a scalar c ∈ 𝕜 with 1 < ‖c‖ and a real R with ‖c‖ < R, then there exists x0 ∈ E with ‖x0‖ ≤ R such that x0 stays at distance at least 1 from every point of F; i.e., ∀ y ∈ F, ‖x0 − y‖ ≥ 1.
Русский
Пусть E — нормированное пространство над ненулевым полем 𝕜, F ⊆ E — замкнутое подпространство. Если существует c ∈ 𝕜 такая, что 1 < ‖c‖ и R ∈ ℝ с ‖c‖ < R, то существует x0 ∈ E с ‖x0‖ ≤ R и для любого y ∈ F выполняется ‖x0 − y‖ ≥ 1; то есть x0 лежит на расстоянии не менее 1 от F.
LaTeX
$$$\text{Let } E \text{ be a normed space over a nontrivial normed field } \mathfrak k,\ F \subset E \text{ a closed subspace. If } 1 < \|c\| \text{ for some } c \in \mathfrak k \text{ and } \|c\| < R \text{ for some } R \in \mathbb R,\text{ then }\exists x_0\in E: \|x_0\| \le R\ \&\ \forall y\in F:\ 1 \le \|x_0 - y\|.$$
Lean4
/-- 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 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 riesz_lemma_of_norm_lt {c : 𝕜} (hc : 1 < ‖c‖) {R : ℝ} (hR : ‖c‖ < R) {F : Subspace 𝕜 E}
(hFc : IsClosed (F : Set E)) (hF : ∃ x : E, x ∉ F) : ∃ x₀ : E, ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖ :=
by
have Rpos : 0 < R := (norm_nonneg _).trans_lt hR
have : ‖c‖ / R < 1 := by
rw [div_lt_iff₀ Rpos]
simpa using hR
rcases riesz_lemma hFc hF this with ⟨x, xF, hx⟩
have x0 : x ≠ 0 := fun H => by simp [H] at xF
obtain ⟨d, d0, dxlt, ledx, -⟩ : ∃ d : 𝕜, d ≠ 0 ∧ ‖d • x‖ < R ∧ R / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ R⁻¹ * ‖c‖ * ‖x‖ :=
rescale_to_shell hc Rpos x0
refine ⟨d • x, dxlt.le, fun y hy => ?_⟩
set y' := d⁻¹ • y
have yy' : y = d • y' := by simp [y', smul_smul, mul_inv_cancel₀ d0]
calc
1 = ‖c‖ / R * (R / ‖c‖) := by field_simp
_ ≤ ‖c‖ / R * ‖d • x‖ := by gcongr
_ = ‖d‖ * (‖c‖ / R * ‖x‖) := by
simp only [norm_smul]
ring
_ ≤ ‖d‖ * ‖x - y'‖ := by gcongr; exact hx y' (by simp [y', Submodule.smul_mem _ _ hy])
_ = ‖d • x - y‖ := by rw [yy', ← smul_sub, norm_smul]
