Normed spaces over R or C #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

None.

Main theorems #

continuous_linear_map.op_norm_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 is_R_or_C in the main normed space theory files.

source

theorem is_R_or_C.norm_coe_norm {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [normed_add_comm_group E] {z : E} :

‖↑‖z‖‖ = ‖z‖

source

@[simp]

theorem norm_smul_inv_norm {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 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.

source

theorem norm_smul_inv_norm' {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 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.

source

theorem linear_map.bound_of_sphere_bound {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] 𝕜) (h : ∀ (z : E), z ∈ metric.sphere 0 r → ‖⇑f z‖ ≤ c) (z : E) :

‖⇑f z‖ ≤ c / r * ‖z‖

source

theorem linear_map.bound_of_ball_bound' {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] 𝕜) (h : ∀ (z : E), z ∈ metric.closed_ball 0 r → ‖⇑f z‖ ≤ c) (z : E) :

‖⇑f z‖ ≤ c / r * ‖z‖

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

source

theorem continuous_linear_map.op_norm_bound_of_ball_bound {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →L[𝕜] 𝕜) (h : ∀ (z : E), z ∈ metric.closed_ball 0 r → ‖⇑f z‖ ≤ c) :

‖f‖ ≤ c / r

source

theorem normed_space.sphere_nonempty_is_R_or_C (𝕜 : Type u_1) [is_R_or_C 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] [nontrivial E] {r : ℝ} (hr : 0 ≤ r) :

nonempty ↥(metric.sphere 0 r)