mathlib documentation

analysis.normed_space.is_R_or_C

Normed spaces over R or C #

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.

@[simp]
theorem is_R_or_C.norm_coe_norm {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [normed_group E] {z : E} :
@[simp]
theorem norm_smul_inv_norm {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [normed_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_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_group E] [normed_space 𝕜 E] {r : } (r_pos : 0 < r) (c : ) (f : E →ₗ[𝕜] 𝕜) (h : ∀ (z : E), z metric.sphere 0 rf z c) (z : E) :
f z (c / r) * z
theorem linear_map.bound_of_ball_bound {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {r : } (r_pos : 0 < r) (c : ) (f : E →ₗ[𝕜] 𝕜) (h : ∀ (z : E), z metric.closed_ball 0 rf z c) (z : E) :
f z (c / r) * z
theorem continuous_linear_map.op_norm_bound_of_ball_bound {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {r : } (r_pos : 0 < r) (c : ) (f : E →L[𝕜] 𝕜) (h : ∀ (z : E), z metric.closed_ball 0 rf z c) :
f c / r