# Operator norm on the space of continuous linear maps #

Define the operator (semi)-norm on the space of continuous (semi)linear maps between (semi)-normed spaces, and prove its basic properties. In particular, show that this space is itself a semi-normed space.

Since a lot of elementary properties don't require βxβ = 0 β x = 0 we start setting up the theory for SeminormedAddCommGroup. Later we will specialize to NormedAddCommGroup in the file NormedSpace.lean.

Note that most of statements that apply to semilinear maps only hold when the ring homomorphism is isometric, as expressed by the typeclass [RingHomIsometric Ο].

theorem norm_image_of_norm_zero {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} {π : Type u_10} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [FunLike π E F] [SemilinearMapClass π Οββ E F] (f : π) (hf : Continuous βf) {x : E} (hx : = 0) :

If βxβ = 0 and f is continuous then βf xβ = 0.

theorem SemilinearMapClass.bound_of_shell_semi_normed {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} {π : Type u_10} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [FunLike π E F] [RingHomIsometric Οββ] [SemilinearMapClass π Οββ E F] (f : π) {Ξ΅ : β} {C : β} (Ξ΅_pos : 0 < Ξ΅) {c : π} (hc : 1 < ) (hf : β (x : E), Ξ΅ / β€ β < Ξ΅ β βf xβ β€ C * ) {x : E} (hx : β  0) :
theorem SemilinearMapClass.bound_of_continuous {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} {π : Type u_10} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [FunLike π E F] [RingHomIsometric Οββ] [SemilinearMapClass π Οββ E F] (f : π) (hf : Continuous βf) :
β (C : β), 0 < C β§ β (x : E), βf xβ β€ C *

A continuous linear map between seminormed spaces is bounded when the field is nontrivially normed. The continuity ensures boundedness on a ball of some radius Ξ΅. The nontriviality of the norm is then used to rescale any element into an element of norm in [Ξ΅/C, Ξ΅], whose image has a controlled norm. The norm control for the original element follows by rescaling.

theorem ContinuousLinearMap.bound {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) :
β (C : β), 0 < C β§ β (x : E), βf xβ β€ C *
noncomputable def LinearIsometry.toSpanSingleton (π : Type u_1) (E : Type u_4) [] [NormedSpace π E] {v : E} (hv : = 1) :
π ββα΅’[π] E

Given a unit-length element x of a normed space E over a field π, the natural linear isometry map from π to E by taking multiples of x.

Equations
• = let __src := ; { toLinearMap := __src, norm_map' := β― }
Instances For
@[simp]
theorem LinearIsometry.toSpanSingleton_apply {π : Type u_1} {E : Type u_4} [] [NormedSpace π E] {v : E} (hv : = 1) (a : π) :
() a = a β’ v
@[simp]
theorem LinearIsometry.coe_toSpanSingleton {π : Type u_1} {E : Type u_4} [] [NormedSpace π E] {v : E} (hv : = 1) :
().toLinearMap =
noncomputable def ContinuousLinearMap.opNorm {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} (f : E βSL[Οββ] F) :

The operator norm of a continuous linear map is the inf of all its bounds.

Equations
Instances For
noncomputable instance ContinuousLinearMap.hasOpNorm {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} :
Norm (E βSL[Οββ] F)
Equations
• ContinuousLinearMap.hasOpNorm = { norm := ContinuousLinearMap.opNorm }
theorem ContinuousLinearMap.norm_def {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} (f : E βSL[Οββ] F) :
= sInf {c : β | 0 β€ c β§ β (x : E), βf xβ β€ c * }
theorem ContinuousLinearMap.bounds_nonempty {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] {f : E βSL[Οββ] F} :
β (c : β), c β {c : β | 0 β€ c β§ β (x : E), βf xβ β€ c * }
theorem ContinuousLinearMap.bounds_bddBelow {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} {f : E βSL[Οββ] F} :
BddBelow {c : β | 0 β€ c β§ β (x : E), βf xβ β€ c * }
theorem ContinuousLinearMap.isLeast_opNorm {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) :
IsLeast {c : β | 0 β€ c β§ β (x : E), βf xβ β€ c * }
@[deprecated ContinuousLinearMap.isLeast_opNorm]
theorem ContinuousLinearMap.isLeast_op_norm {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) :
IsLeast {c : β | 0 β€ c β§ β (x : E), βf xβ β€ c * }

Alias of ContinuousLinearMap.isLeast_opNorm.

theorem ContinuousLinearMap.opNorm_le_bound {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} (f : E βSL[Οββ] F) {M : β} (hMp : 0 β€ M) (hM : β (x : E), βf xβ β€ M * ) :

If one controls the norm of every A x, then one controls the norm of A.

@[deprecated ContinuousLinearMap.opNorm_le_bound]
theorem ContinuousLinearMap.op_norm_le_bound {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} (f : E βSL[Οββ] F) {M : β} (hMp : 0 β€ M) (hM : β (x : E), βf xβ β€ M * ) :

Alias of ContinuousLinearMap.opNorm_le_bound.

If one controls the norm of every A x, then one controls the norm of A.

theorem ContinuousLinearMap.opNorm_le_bound' {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} (f : E βSL[Οββ] F) {M : β} (hMp : 0 β€ M) (hM : β (x : E), β  0 β βf xβ β€ M * ) :

If one controls the norm of every A x, βxβ β  0, then one controls the norm of A.

@[deprecated ContinuousLinearMap.opNorm_le_bound']
theorem ContinuousLinearMap.op_norm_le_bound' {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} (f : E βSL[Οββ] F) {M : β} (hMp : 0 β€ M) (hM : β (x : E), β  0 β βf xβ β€ M * ) :

Alias of ContinuousLinearMap.opNorm_le_bound'.

If one controls the norm of every A x, βxβ β  0, then one controls the norm of A.

theorem ContinuousLinearMap.opNorm_le_of_lipschitz {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} {f : E βSL[Οββ] F} {K : NNReal} (hf : LipschitzWith K βf) :
β€ βK
@[deprecated ContinuousLinearMap.opNorm_le_of_lipschitz]
theorem ContinuousLinearMap.op_norm_le_of_lipschitz {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} {f : E βSL[Οββ] F} {K : NNReal} (hf : LipschitzWith K βf) :
β€ βK

Alias of ContinuousLinearMap.opNorm_le_of_lipschitz.

theorem ContinuousLinearMap.opNorm_eq_of_bounds {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} {Ο : E βSL[Οββ] F} {M : β} (M_nonneg : 0 β€ M) (h_above : β (x : E), βΟ xβ β€ M * ) (h_below : β N β₯ 0, (β (x : E), βΟ xβ β€ N * ) β M β€ N) :
@[deprecated ContinuousLinearMap.opNorm_eq_of_bounds]
theorem ContinuousLinearMap.op_norm_eq_of_bounds {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} {Ο : E βSL[Οββ] F} {M : β} (M_nonneg : 0 β€ M) (h_above : β (x : E), βΟ xβ β€ M * ) (h_below : β N β₯ 0, (β (x : E), βΟ xβ β€ N * ) β M β€ N) :

Alias of ContinuousLinearMap.opNorm_eq_of_bounds.

theorem ContinuousLinearMap.opNorm_neg {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} (f : E βSL[Οββ] F) :
@[deprecated ContinuousLinearMap.opNorm_neg]
theorem ContinuousLinearMap.op_norm_neg {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} (f : E βSL[Οββ] F) :

Alias of ContinuousLinearMap.opNorm_neg.

theorem ContinuousLinearMap.opNorm_nonneg {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} (f : E βSL[Οββ] F) :
@[deprecated ContinuousLinearMap.opNorm_nonneg]
theorem ContinuousLinearMap.op_norm_nonneg {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} (f : E βSL[Οββ] F) :

Alias of ContinuousLinearMap.opNorm_nonneg.

theorem ContinuousLinearMap.opNorm_zero {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} :
= 0

The norm of the 0 operator is 0.

@[deprecated ContinuousLinearMap.opNorm_zero]
theorem ContinuousLinearMap.op_norm_zero {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} :
= 0

Alias of ContinuousLinearMap.opNorm_zero.

The norm of the 0 operator is 0.

theorem ContinuousLinearMap.norm_id_le {π : Type u_1} {E : Type u_4} [] [NormedSpace π E] :

The norm of the identity is at most 1. It is in fact 1, except when the space is trivial where it is 0. It means that one can not do better than an inequality in general.

theorem ContinuousLinearMap.le_opNorm {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) (x : E) :

The fundamental property of the operator norm: βf xβ β€ βfβ * βxβ.

@[deprecated ContinuousLinearMap.le_opNorm]
theorem ContinuousLinearMap.le_op_norm {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) (x : E) :

Alias of ContinuousLinearMap.le_opNorm.

The fundamental property of the operator norm: βf xβ β€ βfβ * βxβ.

theorem ContinuousLinearMap.dist_le_opNorm {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) (x : E) (y : E) :
dist (f x) (f y) β€ * dist x y
@[deprecated ContinuousLinearMap.dist_le_opNorm]
theorem ContinuousLinearMap.dist_le_op_norm {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) (x : E) (y : E) :
dist (f x) (f y) β€ * dist x y

Alias of ContinuousLinearMap.dist_le_opNorm.

theorem ContinuousLinearMap.le_of_opNorm_le_of_le {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) {x : E} {a : β} {b : β} (hf : ) (hx : ) :
@[deprecated ContinuousLinearMap.le_of_opNorm_le_of_le]
theorem ContinuousLinearMap.le_of_op_norm_le_of_le {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) {x : E} {a : β} {b : β} (hf : ) (hx : ) :

Alias of ContinuousLinearMap.le_of_opNorm_le_of_le.

theorem ContinuousLinearMap.le_opNorm_of_le {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) {c : β} {x : E} (h : ) :
@[deprecated ContinuousLinearMap.le_opNorm_of_le]
theorem ContinuousLinearMap.le_op_norm_of_le {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) {c : β} {x : E} (h : ) :

Alias of ContinuousLinearMap.le_opNorm_of_le.

theorem ContinuousLinearMap.le_of_opNorm_le {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) {c : β} (h : ) (x : E) :
@[deprecated ContinuousLinearMap.le_of_opNorm_le]
theorem ContinuousLinearMap.le_of_op_norm_le {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) {c : β} (h : ) (x : E) :

Alias of ContinuousLinearMap.le_of_opNorm_le.

theorem ContinuousLinearMap.opNorm_le_iff {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] {f : E βSL[Οββ] F} {M : β} (hMp : 0 β€ M) :
β β (x : E), βf xβ β€ M *
@[deprecated ContinuousLinearMap.opNorm_le_iff]
theorem ContinuousLinearMap.op_norm_le_iff {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] {f : E βSL[Οββ] F} {M : β} (hMp : 0 β€ M) :
β β (x : E), βf xβ β€ M *

Alias of ContinuousLinearMap.opNorm_le_iff.

theorem ContinuousLinearMap.ratio_le_opNorm {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) (x : E) :
@[deprecated ContinuousLinearMap.ratio_le_opNorm]
theorem ContinuousLinearMap.ratio_le_op_norm {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) (x : E) :

Alias of ContinuousLinearMap.ratio_le_opNorm.

theorem ContinuousLinearMap.unit_le_opNorm {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) (x : E) :
β βf xβ β€

The image of the unit ball under a continuous linear map is bounded.

@[deprecated ContinuousLinearMap.unit_le_opNorm]
theorem ContinuousLinearMap.unit_le_op_norm {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) (x : E) :
β βf xβ β€

Alias of ContinuousLinearMap.unit_le_opNorm.

The image of the unit ball under a continuous linear map is bounded.

theorem ContinuousLinearMap.opNorm_le_of_shell {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] {f : E βSL[Οββ] F} {Ξ΅ : β} {C : β} (Ξ΅_pos : 0 < Ξ΅) (hC : 0 β€ C) {c : π} (hc : 1 < ) (hf : β (x : E), Ξ΅ / β€ β < Ξ΅ β βf xβ β€ C * ) :
@[deprecated ContinuousLinearMap.opNorm_le_of_shell]
theorem ContinuousLinearMap.op_norm_le_of_shell {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] {f : E βSL[Οββ] F} {Ξ΅ : β} {C : β} (Ξ΅_pos : 0 < Ξ΅) (hC : 0 β€ C) {c : π} (hc : 1 < ) (hf : β (x : E), Ξ΅ / β€ β < Ξ΅ β βf xβ β€ C * ) :

Alias of ContinuousLinearMap.opNorm_le_of_shell.

theorem ContinuousLinearMap.opNorm_le_of_ball {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] {f : E βSL[Οββ] F} {Ξ΅ : β} {C : β} (Ξ΅_pos : 0 < Ξ΅) (hC : 0 β€ C) (hf : β x β Metric.ball 0 Ξ΅, βf xβ β€ C * ) :
@[deprecated ContinuousLinearMap.opNorm_le_of_ball]
theorem ContinuousLinearMap.op_norm_le_of_ball {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] {f : E βSL[Οββ] F} {Ξ΅ : β} {C : β} (Ξ΅_pos : 0 < Ξ΅) (hC : 0 β€ C) (hf : β x β Metric.ball 0 Ξ΅, βf xβ β€ C * ) :

Alias of ContinuousLinearMap.opNorm_le_of_ball.

theorem ContinuousLinearMap.opNorm_le_of_nhds_zero {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] {f : E βSL[Οββ] F} {C : β} (hC : 0 β€ C) (hf : βαΆ  (x : E) in nhds 0, βf xβ β€ C * ) :
@[deprecated ContinuousLinearMap.opNorm_le_of_nhds_zero]
theorem ContinuousLinearMap.op_norm_le_of_nhds_zero {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] {f : E βSL[Οββ] F} {C : β} (hC : 0 β€ C) (hf : βαΆ  (x : E) in nhds 0, βf xβ β€ C * ) :

Alias of ContinuousLinearMap.opNorm_le_of_nhds_zero.

theorem ContinuousLinearMap.opNorm_le_of_shell' {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] {f : E βSL[Οββ] F} {Ξ΅ : β} {C : β} (Ξ΅_pos : 0 < Ξ΅) (hC : 0 β€ C) {c : π} (hc : < 1) (hf : β (x : E), Ξ΅ * β€ β < Ξ΅ β βf xβ β€ C * ) :
@[deprecated ContinuousLinearMap.opNorm_le_of_shell']
theorem ContinuousLinearMap.op_norm_le_of_shell' {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] {f : E βSL[Οββ] F} {Ξ΅ : β} {C : β} (Ξ΅_pos : 0 < Ξ΅) (hC : 0 β€ C) {c : π} (hc : < 1) (hf : β (x : E), Ξ΅ * β€ β < Ξ΅ β βf xβ β€ C * ) :

Alias of ContinuousLinearMap.opNorm_le_of_shell'.

theorem ContinuousLinearMap.opNorm_le_of_unit_norm {E : Type u_4} {F : Type u_6} [] [] {f : } {C : β} (hC : 0 β€ C) (hf : β (x : E), = 1 β βf xβ β€ C) :

For a continuous real linear map f, if one controls the norm of every f x, βxβ = 1, then one controls the norm of f.

@[deprecated ContinuousLinearMap.opNorm_le_of_unit_norm]
theorem ContinuousLinearMap.op_norm_le_of_unit_norm {E : Type u_4} {F : Type u_6} [] [] {f : } {C : β} (hC : 0 β€ C) (hf : β (x : E), = 1 β βf xβ β€ C) :

Alias of ContinuousLinearMap.opNorm_le_of_unit_norm.

For a continuous real linear map f, if one controls the norm of every f x, βxβ = 1, then one controls the norm of f.

theorem ContinuousLinearMap.opNorm_add_le {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) (g : E βSL[Οββ] F) :

The operator norm satisfies the triangle inequality.

theorem ContinuousLinearMap.op_norm_add_le {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) (g : E βSL[Οββ] F) :

Alias of ContinuousLinearMap.opNorm_add_le.

The operator norm satisfies the triangle inequality.

theorem ContinuousLinearMap.norm_id_of_nontrivial_seminorm {π : Type u_1} {E : Type u_4} [] [NormedSpace π E] (h : β (x : E), β  0) :

If there is an element with norm different from 0, then the norm of the identity equals 1. (Since we are working with seminorms supposing that the space is non-trivial is not enough.)

theorem ContinuousLinearMap.opNorm_smul_le {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] {π' : Type u_11} [NormedField π'] [NormedSpace π' F] [SMulCommClass πβ π' F] (c : π') (f : E βSL[Οββ] F) :
@[deprecated ContinuousLinearMap.opNorm_smul_le]
theorem ContinuousLinearMap.op_norm_smul_le {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] {π' : Type u_11} [NormedField π'] [NormedSpace π' F] [SMulCommClass πβ π' F] (c : π') (f : E βSL[Οββ] F) :

Alias of ContinuousLinearMap.opNorm_smul_le.

noncomputable def ContinuousLinearMap.seminorm {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] :
Seminorm πβ (E βSL[Οββ] F)

Operator seminorm on the space of continuous (semi)linear maps, as Seminorm.

We use this seminorm to define a SeminormedGroup structure on E βSL[Ο] F, but we have to override the projection UniformSpace so that it is definitionally equal to the one coming from the topologies on E and F.

Equations
Instances For
noncomputable instance ContinuousLinearMap.toPseudoMetricSpace {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] :
PseudoMetricSpace (E βSL[Οββ] F)
Equations
noncomputable instance ContinuousLinearMap.toSeminormedAddCommGroup {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] :

Continuous linear maps themselves form a seminormed space with respect to the operator norm.

Equations
noncomputable instance ContinuousLinearMap.toNormedSpace {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] {π' : Type u_11} [NormedField π'] [NormedSpace π' F] [SMulCommClass πβ π' F] :
NormedSpace π' (E βSL[Οββ] F)
Equations
• ContinuousLinearMap.toNormedSpace =
theorem ContinuousLinearMap.opNorm_comp_le {π : Type u_1} {πβ : Type u_2} {πβ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8} [] [NontriviallyNormedField πβ] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] [NormedSpace πβ G] {Οββ : π β+* πβ} {Οββ : πβ β+* πβ} {Οββ : π β+* πβ} [RingHomCompTriple Οββ Οββ Οββ] [RingHomIsometric Οββ] [RingHomIsometric Οββ] (h : F βSL[Οββ] G) (f : E βSL[Οββ] F) :

The operator norm is submultiplicative.

@[deprecated ContinuousLinearMap.opNorm_comp_le]
theorem ContinuousLinearMap.op_norm_comp_le {π : Type u_1} {πβ : Type u_2} {πβ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8} [] [NontriviallyNormedField πβ] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] [NormedSpace πβ G] {Οββ : π β+* πβ} {Οββ : πβ β+* πβ} {Οββ : π β+* πβ} [RingHomCompTriple Οββ Οββ Οββ] [RingHomIsometric Οββ] [RingHomIsometric Οββ] (h : F βSL[Οββ] G) (f : E βSL[Οββ] F) :

Alias of ContinuousLinearMap.opNorm_comp_le.

The operator norm is submultiplicative.

noncomputable instance ContinuousLinearMap.toSemiNormedRing {π : Type u_1} {E : Type u_4} [] [NormedSpace π E] :

Continuous linear maps form a seminormed ring with respect to the operator norm.

Equations
• ContinuousLinearMap.toSemiNormedRing = let __src := ContinuousLinearMap.toSeminormedAddCommGroup; let __src_1 := ContinuousLinearMap.ring; SeminormedRing.mk β― β―
noncomputable instance ContinuousLinearMap.toNormedAlgebra {π : Type u_1} {E : Type u_4} [] [NormedSpace π E] :
NormedAlgebra π (E βL[π] E)

For a normed space E, continuous linear endomorphisms form a normed algebra with respect to the operator norm.

Equations
• ContinuousLinearMap.toNormedAlgebra = let __src := ContinuousLinearMap.algebra;
@[simp]
theorem ContinuousLinearMap.opNorm_subsingleton {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) [] :
= 0
@[deprecated ContinuousLinearMap.opNorm_subsingleton]
theorem ContinuousLinearMap.op_norm_subsingleton {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} [RingHomIsometric Οββ] (f : E βSL[Οββ] F) [] :
= 0

Alias of ContinuousLinearMap.opNorm_subsingleton.

@[simp]
theorem ContinuousLinearMap.norm_restrictScalars {π : Type u_1} {E : Type u_4} {Fβ : Type u_7} [] [] [NormedSpace π E] [NormedSpace π Fβ] {π' : Type u_11} [] [NormedAlgebra π' π] [NormedSpace π' E] [IsScalarTower π' π E] [NormedSpace π' Fβ] [IsScalarTower π' π Fβ] (f : E βL[π] Fβ) :
noncomputable def ContinuousLinearMap.restrictScalarsIsometry (π : Type u_1) (E : Type u_4) (Fβ : Type u_7) [] [] [NormedSpace π E] [NormedSpace π Fβ] (π' : Type u_11) [] [NormedAlgebra π' π] [NormedSpace π' E] [IsScalarTower π' π E] [NormedSpace π' Fβ] [IsScalarTower π' π Fβ] (π'' : Type u_12) [Ring π''] [Module π'' Fβ] [ContinuousConstSMul π'' Fβ] [SMulCommClass π π'' Fβ] [SMulCommClass π' π'' Fβ] :
(E βL[π] Fβ) ββα΅’[π''] E βL[π'] Fβ

ContinuousLinearMap.restrictScalars as a LinearIsometry.

Equations
Instances For
@[simp]
theorem ContinuousLinearMap.coe_restrictScalarsIsometry (π : Type u_1) (E : Type u_4) (Fβ : Type u_7) [] [] [NormedSpace π E] [NormedSpace π Fβ] (π' : Type u_11) [] [NormedAlgebra π' π] [NormedSpace π' E] [IsScalarTower π' π E] [NormedSpace π' Fβ] [IsScalarTower π' π Fβ] {π'' : Type u_12} [Ring π''] [Module π'' Fβ] [ContinuousConstSMul π'' Fβ] [SMulCommClass π π'' Fβ] [SMulCommClass π' π'' Fβ] :
β(ContinuousLinearMap.restrictScalarsIsometry π E Fβ π' π'') =
@[simp]
theorem ContinuousLinearMap.restrictScalarsIsometry_toLinearMap (π : Type u_1) (E : Type u_4) (Fβ : Type u_7) [] [] [NormedSpace π E] [NormedSpace π Fβ] (π' : Type u_11) [] [NormedAlgebra π' π] [NormedSpace π' E] [IsScalarTower π' π E] [NormedSpace π' Fβ] [IsScalarTower π' π Fβ] {π'' : Type u_12} [Ring π''] [Module π'' Fβ] [ContinuousConstSMul π'' Fβ] [SMulCommClass π π'' Fβ] [SMulCommClass π' π'' Fβ] :
(ContinuousLinearMap.restrictScalarsIsometry π E Fβ π' π'').toLinearMap = ContinuousLinearMap.restrictScalarsβ π E Fβ π' π''
noncomputable def ContinuousLinearMap.restrictScalarsL (π : Type u_1) (E : Type u_4) (Fβ : Type u_7) [] [] [NormedSpace π E] [NormedSpace π Fβ] (π' : Type u_11) [] [NormedAlgebra π' π] [NormedSpace π' E] [IsScalarTower π' π E] [NormedSpace π' Fβ] [IsScalarTower π' π Fβ] (π'' : Type u_12) [Ring π''] [Module π'' Fβ] [ContinuousConstSMul π'' Fβ] [SMulCommClass π π'' Fβ] [SMulCommClass π' π'' Fβ] :
(E βL[π] Fβ) βL[π''] E βL[π'] Fβ

ContinuousLinearMap.restrictScalars as a ContinuousLinearMap.

Equations
Instances For
@[simp]
theorem ContinuousLinearMap.coe_restrictScalarsL {π : Type u_1} {E : Type u_4} {Fβ : Type u_7} [] [] [NormedSpace π E] [NormedSpace π Fβ] {π' : Type u_11} [] [NormedAlgebra π' π] [NormedSpace π' E] [IsScalarTower π' π E] [NormedSpace π' Fβ] [IsScalarTower π' π Fβ] {π'' : Type u_12} [Ring π''] [Module π'' Fβ] [ContinuousConstSMul π'' Fβ] [SMulCommClass π π'' Fβ] [SMulCommClass π' π'' Fβ] :
β(ContinuousLinearMap.restrictScalarsL π E Fβ π' π'') = ContinuousLinearMap.restrictScalarsβ π E Fβ π' π''
@[simp]
theorem ContinuousLinearMap.coe_restrict_scalarsL' {π : Type u_1} {E : Type u_4} {Fβ : Type u_7} [] [] [NormedSpace π E] [NormedSpace π Fβ] {π' : Type u_11} [] [NormedAlgebra π' π] [NormedSpace π' E] [IsScalarTower π' π E] [NormedSpace π' Fβ] [IsScalarTower π' π Fβ] {π'' : Type u_12} [Ring π''] [Module π'' Fβ] [ContinuousConstSMul π'' Fβ] [SMulCommClass π π'' Fβ] [SMulCommClass π' π'' Fβ] :
β(ContinuousLinearMap.restrictScalarsL π E Fβ π' π'') =
theorem ContinuousLinearMap.norm_pi_le_of_le {π : Type u_1} {E : Type u_4} [] [NormedSpace π E] {ΞΉ : Type u_11} [Fintype ΞΉ] {M : ΞΉ β Type u_12} [(i : ΞΉ) β ] [(i : ΞΉ) β NormedSpace π (M i)] {C : β} {L : (i : ΞΉ) β E βL[π] M i} (hL : β (i : ΞΉ), βL iβ β€ C) (hC : 0 β€ C) :
theorem LinearMap.mkContinuous_norm_le {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} (f : E βββ[Οββ] F) {C : β} (hC : 0 β€ C) (h : β (x : E), βf xβ β€ C * ) :
βf.mkContinuous C hβ β€ C

If a continuous linear map is constructed from a linear map via the constructor mkContinuous, then its norm is bounded by the bound given to the constructor if it is nonnegative.

theorem LinearMap.mkContinuous_norm_le' {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} (f : E βββ[Οββ] F) {C : β} (h : β (x : E), βf xβ β€ C * ) :
βf.mkContinuous C hβ β€ max C 0

If a continuous linear map is constructed from a linear map via the constructor mkContinuous, then its norm is bounded by the bound or zero if bound is negative.

theorem LinearIsometry.norm_toContinuousLinearMap_le {π : Type u_1} {πβ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField πβ] [NormedSpace π E] [NormedSpace πβ F] {Οββ : π β+* πβ} (f : E βββα΅’[Οββ] F) :
βf.toContinuousLinearMapβ β€ 1
theorem Submodule.norm_subtypeL_le {π : Type u_1} {E : Type u_4} [] [NormedSpace π E] (K : Submodule π E) :
βK.subtypeLβ β€ 1