Normed spaces over R or C

This file is about results on normed spaces over the fields ℝ and ℂ.

Main definitions

None.

Main theorems

• ContinuousLinearMap.opNorm_bound_of_ball_bound: A bound on the norms of values of a linear map in a ball yields a bound on the operator norm.

Notes

This file exists mainly to avoid importing RCLike in the main normed space theory files.

theorem RCLike.norm_coe_norm {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] {z : E} : ‖↑‖z‖‖ = ‖z‖

@[simp]

theorem norm_smul_inv_norm {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} (hx : x ≠ 0) : ‖(↑‖x‖)⁻¹ • x‖ = 1

Lemma to normalize a vector in a normed space E over either ℂ or ℝ to unit length.

theorem norm_smul_inv_norm' {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} (r_nonneg : 0 ≤ r) {x : E} (hx : x ≠ 0) : ‖(↑r * (↑‖x‖)⁻¹) • x‖ = r

Lemma to normalize a vector in a normed space E over either ℂ or ℝ to length r.

theorem ContinuousLinearEquiv.coord_norm' {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} (h : x ≠ 0) : ‖↑‖x‖ • coord 𝕜 x h‖ = 1

@[deprecated ContinuousLinearEquiv.coord_norm' (since := "2026-02-01")]

theorem coord_norm' {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} (h : x ≠ 0) : ‖↑‖x‖ • ContinuousLinearEquiv.coord 𝕜 x h‖ = 1

Alias of ContinuousLinearEquiv.coord_norm'.

theorem LinearMap.bound_of_sphere_bound {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] 𝕜) (h : ∀ z ∈ Metric.sphere 0 r, ‖f z‖ ≤ c) (z : E) : ‖f z‖ ≤ c / r * ‖z‖

theorem LinearMap.bound_of_ball_bound' {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] 𝕜) (h : ∀ z ∈ Metric.closedBall 0 r, ‖f z‖ ≤ c) (z : E) : ‖f z‖ ≤ c / r * ‖z‖

LinearMap.bound_of_ball_bound is a version of this over arbitrary nontrivially normed fields. It produces a less precise bound so we keep both versions.

theorem ContinuousLinearMap.opNorm_bound_of_ball_bound {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : StrongDual 𝕜 E) (h : ∀ z ∈ Metric.closedBall 0 r, ‖f z‖ ≤ c) : ‖f‖ ≤ c / r

theorem antilipschitz_of_bound_of_norm_one {𝕜 : Type u_1} [RCLike 𝕜] {𝓕 : Type u_3} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] [MulActionHomClass 𝓕 𝕜 E F] (f : 𝓕) {K : NNReal} (h : ∀ (x : E), ‖x‖ = 1 → 1 ≤ ↑K * ‖f x‖) : AntilipschitzWith K ⇑f

If a map f over an RCLike space satisfies ‖x‖ = 1 → 1 ≤ K * ‖f x‖, then f is antilipschitz with constant K. We require that the map is an additive monoid homomorphism, and acts as a multiplicative action: in practice this means f is a linear map, but we allow the flexibility so it is convenient to apply for eg continuous linear maps also, without a coercion in the goal.

theorem NormedSpace.sphere_nonempty_rclike (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [Nontrivial E] {r : ℝ} (hr : 0 ≤ r) : Nonempty ↑(Metric.sphere 0 r)