# Documentation

Mathlib.Analysis.NormedSpace.IsROrC

# Normed spaces over R or C #

This file is about results on normed spaces over the fields โ and โ.

None.

## Main theorems #

• ContinuousLinearMap.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 IsROrC in the main normed space theory files.

theorem IsROrC.norm_coe_norm {๐ : Type u_1} [IsROrC ๐] {E : Type u_2} {z : E} :
@[simp]
theorem norm_smul_inv_norm {๐ : Type u_1} [IsROrC ๐] {E : Type u_2} [NormedSpace ๐ 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} [IsROrC ๐] {E : Type u_2} [NormedSpace ๐ E] {r : โ} (r_nonneg : 0 โค r) {x : E} (hx : x โ  0) :
โ(โr * (โ)โปยน) โข 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} [IsROrC ๐] {E : Type u_2} [NormedSpace ๐ E] {r : โ} (r_pos : 0 < r) (c : โ) (f : E โโ[๐] ๐) (h : โ (z : E), z โ โ โโf zโ โค c) (z : E) :
โโf zโ โค c / r *
theorem LinearMap.bound_of_ball_bound' {๐ : Type u_1} [IsROrC ๐] {E : Type u_2} [NormedSpace ๐ E] {r : โ} (r_pos : 0 < r) (c : โ) (f : E โโ[๐] ๐) (h : โ (z : E), z โ โ โโf zโ โค c) (z : E) :
โโf zโ โค c / r *

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.op_norm_bound_of_ball_bound {๐ : Type u_1} [IsROrC ๐] {E : Type u_2} [NormedSpace ๐ E] {r : โ} (r_pos : 0 < r) (c : โ) (f : E โL[๐] ๐) (h : โ (z : E), z โ โ โโf zโ โค c) :
โค c / r
theorem NormedSpace.sphere_nonempty_isROrC (๐ : Type u_1) [IsROrC ๐] {E : Type u_2} [NormedSpace ๐ E] [] {r : โ} (hr : 0 โค r) :
Nonempty โ()