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 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 : E →L[𝕜] 𝕜) (h : ∀ z ∈ Metric.closedBall 0 r, ‖f z‖ ≤ c) : ‖f‖ ≤ c / r

@[deprecated ContinuousLinearMap.opNorm_bound_of_ball_bound]

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

Alias of ContinuousLinearMap.opNorm_bound_of_ball_bound.

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)