# Operator norm for maps on normed spaces #

This file contains statements about operator norm for which it really matters that the underlying space has a norm (rather than just a seminorm).

theorem LinearMap.bound_of_shell {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [RingHomIsometric ฯโโ] (f : E โโโ[ฯโโ] F) {ฮต : โ} {C : โ} (ฮต_pos : 0 < ฮต) {c : ๐} (hc : 1 < ) (hf : โ (x : E), ฮต / โค โ < ฮต โ โf xโ โค C * ) (x : E) :
theorem LinearMap.bound_of_ball_bound {๐ : Type u_1} {E : Type u_4} {Fโ : Type u_7} [] [] [NormedSpace ๐ E] [NormedSpace ๐ Fโ] {r : โ} (r_pos : 0 < r) (c : โ) (f : E โโ[๐] Fโ) (h : โ z โ , โf zโ โค c) :
โ (C : โ), โ (z : E), โf zโ โค C *

LinearMap.bound_of_ball_bound' is a version of this lemma over a field satisfying RCLike that produces a concrete bound.

theorem LinearMap.antilipschitz_of_comap_nhds_le {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [h : RingHomIsometric ฯโโ] (f : E โโโ[ฯโโ] F) (hf : Filter.comap (โf) (nhds 0) โค nhds 0) :
โ (K : NNReal), AntilipschitzWith K โf
theorem ContinuousLinearMap.opNorm_zero_iff {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} (f : E โSL[ฯโโ] F) [RingHomIsometric ฯโโ] :
= 0 โ f = 0

An operator is zero iff its norm vanishes.

@[deprecated ContinuousLinearMap.opNorm_zero_iff]
theorem ContinuousLinearMap.op_norm_zero_iff {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} (f : E โSL[ฯโโ] F) [RingHomIsometric ฯโโ] :
= 0 โ f = 0

Alias of ContinuousLinearMap.opNorm_zero_iff.

An operator is zero iff its norm vanishes.

@[simp]
theorem ContinuousLinearMap.norm_id {๐ : Type u_1} {E : Type u_4} [] [NormedSpace ๐ E] [] :

If a normed space is non-trivial, then the norm of the identity equals 1.

@[simp]
theorem ContinuousLinearMap.nnnorm_id {๐ : Type u_1} {E : Type u_4} [] [NormedSpace ๐ E] [] :
= 1
noncomputable instance ContinuousLinearMap.normOneClass {๐ : Type u_1} {E : Type u_4} [] [NormedSpace ๐ E] [] :
NormOneClass (E โL[๐] E)
Equations
• โฏ = โฏ
noncomputable instance ContinuousLinearMap.toNormedAddCommGroup {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [RingHomIsometric ฯโโ] :
NormedAddCommGroup (E โSL[ฯโโ] F)

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

Equations
noncomputable instance ContinuousLinearMap.toNormedRing {๐ : Type u_1} {E : Type u_4} [] [NormedSpace ๐ E] :
NormedRing (E โL[๐] E)

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

Equations
• ContinuousLinearMap.toNormedRing = let __src := ContinuousLinearMap.toNormedAddCommGroup; let __src_1 := ContinuousLinearMap.toSemiNormedRing; NormedRing.mk โฏ โฏ
theorem ContinuousLinearMap.homothety_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) {a : โ} (hf : โ (x : E), โf xโ = a * ) :
= a
theorem ContinuousLinearMap.antilipschitz_of_embedding {๐ : Type u_1} {E : Type u_4} {Fโ : Type u_7} [] [] [NormedSpace ๐ E] [NormedSpace ๐ Fโ] (f : E โL[๐] Fโ) (hf : Embedding โf) :
โ (K : NNReal), AntilipschitzWith K โf

If a continuous linear map is a topology embedding, then it is expands the distances by a positive factor.

@[simp]
theorem LinearIsometry.norm_toContinuousLinearMap {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} [] [RingHomIsometric ฯโโ] (f : E โโโแตข[ฯโโ] F) :
theorem LinearIsometry.norm_toContinuousLinearMap_comp {๐ : 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 ฯโโ] (f : F โโโแตข[ฯโโ] G) {g : E โSL[ฯโโ] F} :

Postcomposition of a continuous linear map with a linear isometry preserves the operator norm.

theorem ContinuousLinearMap.opNorm_comp_linearIsometryEquiv {๐โ : Type u_2} {๐โ : Type u_3} {F : Type u_6} {G : Type u_8} [NontriviallyNormedField ๐โ] [NontriviallyNormedField ๐โ] [NormedSpace ๐โ F] [NormedSpace ๐โ G] {ฯโโ : ๐โ โ+* ๐โ} {๐โ' : Type u_11} [NontriviallyNormedField ๐โ'] {F' : Type u_12} [] [NormedSpace ๐โ' F'] {ฯโ' : ๐โ' โ+* ๐โ} {ฯโ'' : ๐โ โ+* ๐โ'} {ฯโโ' : ๐โ' โ+* ๐โ} [RingHomInvPair ฯโ' ฯโ''] [RingHomInvPair ฯโ'' ฯโ'] [RingHomCompTriple ฯโ' ฯโโ ฯโโ'] [RingHomCompTriple ฯโ'' ฯโโ' ฯโโ] [RingHomIsometric ฯโโ] [RingHomIsometric ฯโ'] [RingHomIsometric ฯโ''] [RingHomIsometric ฯโโ'] (f : F โSL[ฯโโ] G) (g : F' โโโแตข[ฯโ'] F) :

Precomposition with a linear isometry preserves the operator norm.

@[deprecated ContinuousLinearMap.opNorm_comp_linearIsometryEquiv]
theorem ContinuousLinearMap.op_norm_comp_linearIsometryEquiv {๐โ : Type u_2} {๐โ : Type u_3} {F : Type u_6} {G : Type u_8} [NontriviallyNormedField ๐โ] [NontriviallyNormedField ๐โ] [NormedSpace ๐โ F] [NormedSpace ๐โ G] {ฯโโ : ๐โ โ+* ๐โ} {๐โ' : Type u_11} [NontriviallyNormedField ๐โ'] {F' : Type u_12} [] [NormedSpace ๐โ' F'] {ฯโ' : ๐โ' โ+* ๐โ} {ฯโ'' : ๐โ โ+* ๐โ'} {ฯโโ' : ๐โ' โ+* ๐โ} [RingHomInvPair ฯโ' ฯโ''] [RingHomInvPair ฯโ'' ฯโ'] [RingHomCompTriple ฯโ' ฯโโ ฯโโ'] [RingHomCompTriple ฯโ'' ฯโโ' ฯโโ] [RingHomIsometric ฯโโ] [RingHomIsometric ฯโ'] [RingHomIsometric ฯโ''] [RingHomIsometric ฯโโ'] (f : F โSL[ฯโโ] G) (g : F' โโโแตข[ฯโ'] F) :

Alias of ContinuousLinearMap.opNorm_comp_linearIsometryEquiv.

Precomposition with a linear isometry preserves the operator norm.

@[simp]
theorem ContinuousLinearMap.norm_smulRight_apply {๐ : Type u_1} {E : Type u_4} {Fโ : Type u_7} [] [] [NormedSpace ๐ E] [NormedSpace ๐ Fโ] (c : E โL[๐] ๐) (f : Fโ) :

The norm of the tensor product of a scalar linear map and of an element of a normed space is the product of the norms.

@[simp]
theorem ContinuousLinearMap.nnnorm_smulRight_apply {๐ : Type u_1} {E : Type u_4} {Fโ : Type u_7} [] [] [NormedSpace ๐ E] [NormedSpace ๐ Fโ] (c : E โL[๐] ๐) (f : Fโ) :

The non-negative norm of the tensor product of a scalar linear map and of an element of a normed space is the product of the non-negative norms.

noncomputable def ContinuousLinearMap.smulRightL (๐ : Type u_1) (E : Type u_4) (Fโ : Type u_7) [] [] [NormedSpace ๐ E] [NormedSpace ๐ Fโ] :
(E โL[๐] ๐) โL[๐] Fโ โL[๐] E โL[๐] Fโ

ContinuousLinearMap.smulRight as a continuous trilinear map: smulRightL (c : E โL[๐] ๐) (f : F) (x : E) = c x โข f.

Equations
Instances For
@[simp]
theorem ContinuousLinearMap.norm_smulRightL_apply {๐ : Type u_1} {E : Type u_4} {Fโ : Type u_7} [] [] [NormedSpace ๐ E] [NormedSpace ๐ Fโ] (c : E โL[๐] ๐) (f : Fโ) :
โ((ContinuousLinearMap.smulRightL ๐ E Fโ) c) fโ =
@[simp]
theorem ContinuousLinearMap.norm_smulRightL {๐ : Type u_1} {E : Type u_4} {Fโ : Type u_7} [] [] [NormedSpace ๐ E] [NormedSpace ๐ Fโ] (c : E โL[๐] ๐) [Nontrivial Fโ] :
theorem Submodule.norm_subtypeL {๐ : Type u_1} {E : Type u_4} [] [NormedSpace ๐ E] (K : Submodule ๐ E) [Nontrivial โฅK] :
theorem ContinuousLinearEquiv.antilipschitz {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} {ฯโโ : ๐โ โ+* ๐} [RingHomInvPair ฯโโ ฯโโ] [RingHomInvPair ฯโโ ฯโโ] [RingHomIsometric ฯโโ] (e : E โSL[ฯโโ] F) :
theorem ContinuousLinearEquiv.one_le_norm_mul_norm_symm {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} {ฯโโ : ๐โ โ+* ๐} [RingHomInvPair ฯโโ ฯโโ] [RingHomInvPair ฯโโ ฯโโ] [RingHomIsometric ฯโโ] [RingHomIsometric ฯโโ] [] (e : E โSL[ฯโโ] F) :
theorem ContinuousLinearEquiv.norm_pos {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} {ฯโโ : ๐โ โ+* ๐} [RingHomInvPair ฯโโ ฯโโ] [RingHomInvPair ฯโโ ฯโโ] [RingHomIsometric ฯโโ] [RingHomIsometric ฯโโ] [] (e : E โSL[ฯโโ] F) :
0 < โโeโ
theorem ContinuousLinearEquiv.norm_symm_pos {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} {ฯโโ : ๐โ โ+* ๐} [RingHomInvPair ฯโโ ฯโโ] [RingHomInvPair ฯโโ ฯโโ] [RingHomIsometric ฯโโ] [RingHomIsometric ฯโโ] [] (e : E โSL[ฯโโ] F) :
theorem ContinuousLinearEquiv.nnnorm_symm_pos {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} {ฯโโ : ๐โ โ+* ๐} [RingHomInvPair ฯโโ ฯโโ] [RingHomInvPair ฯโโ ฯโโ] [RingHomIsometric ฯโโ] [RingHomIsometric ฯโโ] [] (e : E โSL[ฯโโ] F) :
theorem ContinuousLinearEquiv.subsingleton_or_norm_symm_pos {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} {ฯโโ : ๐โ โ+* ๐} [RingHomInvPair ฯโโ ฯโโ] [RingHomInvPair ฯโโ ฯโโ] [RingHomIsometric ฯโโ] [RingHomIsometric ฯโโ] (e : E โSL[ฯโโ] F) :
theorem ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} [] [NontriviallyNormedField ๐โ] [NormedSpace ๐ E] [NormedSpace ๐โ F] {ฯโโ : ๐ โ+* ๐โ} {ฯโโ : ๐โ โ+* ๐} [RingHomInvPair ฯโโ ฯโโ] [RingHomInvPair ฯโโ ฯโโ] [RingHomIsometric ฯโโ] [RingHomIsometric ฯโโ] (e : E โSL[ฯโโ] F) :
@[simp]
theorem ContinuousLinearEquiv.coord_norm (๐ : Type u_1) {E : Type u_4} [] [NormedSpace ๐ E] (x : E) (h : x โ  0) :
noncomputable def IsCoercive {E : Type u_4} [] (B : ) :

A bounded bilinear form B in a real normed space is coercive if there is some positive constant C such that C * โuโ * โuโ โค B u u.

Equations
Instances For
theorem NormedSpace.equicontinuous_TFAE {๐ : Type u_1} {๐โ : Type u_2} {E : Type u_4} {F : Type u_6} {ฮน : Type u_11} [] [NontriviallyNormedField ๐โ] {ฯโโ : ๐ โ+* ๐โ} [RingHomIsometric ฯโโ] [NormedSpace ๐ E] [NormedSpace ๐โ F] (f : ฮน โ E โSL[ฯโโ] F) :
List.TFAE [EquicontinuousAt (DFunLike.coe โ f) 0, Equicontinuous (DFunLike.coe โ f), UniformEquicontinuous (DFunLike.coe โ f), โ (C : โ), โ (i : ฮน) (x : E), โ(f i) xโ โค C * , โ C โฅ 0, โ (i : ฮน) (x : E), โ(f i) xโ โค C * , โ (C : โ), โ (i : ฮน), โf iโ โค C, โ C โฅ 0, โ (i : ฮน), โf iโ โค C, BddAbove (Set.range fun (x : ฮน) => โf xโ), โจ (i : ฮน), โโf iโโ < โค]

Equivalent characterizations for equicontinuity of a family of continuous linear maps between normed spaces. See also WithSeminorms.equicontinuous_TFAE for similar characterizations between spaces satisfying WithSeminorms.