mathlib3 documentation

analysis.normed_space.is_R_or_C

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 #

Notes #

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

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} :
@[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) :

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

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) :

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

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) :
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) :

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.

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
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) :