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

source

theorem LinearMap.bound_of_shell {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →ₛₗ[σ₁₂] F) {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) {c : 𝕜} (hc : 1 < ‖c‖) (hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) (x : E) :

‖f x‖ ≤ C * ‖x‖

source

theorem LinearMap.bound_of_ball_bound {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] Fₗ) (h : ∀ z ∈ Metric.ball 0 r, ‖f z‖ ≤ c) :

∃ (C : ℝ), ∀ (z : E), ‖f z‖ ≤ C * ‖z‖

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

source

theorem LinearMap.antilipschitz_of_comap_nhds_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [h : RingHomIsometric σ₁₂] (f : E →ₛₗ[σ₁₂] F) (hf : Filter.comap (⇑f) (nhds 0) ≤ nhds 0) :

∃ (K : NNReal), AntilipschitzWith K ⇑f

source

theorem ContinuousLinearMap.opNorm_zero_iff {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [RingHomIsometric σ₁₂] :

‖f‖ = 0 ↔ f = 0

An operator is zero iff its norm vanishes.

source

@[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} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [RingHomIsometric σ₁₂] :

‖f‖ = 0 ↔ f = 0

Alias of ContinuousLinearMap.opNorm_zero_iff.

An operator is zero iff its norm vanishes.

source

@[simp]

theorem ContinuousLinearMap.norm_id {𝕜 : Type u_1} {E : Type u_4} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [Nontrivial E] :

‖ContinuousLinearMap.id 𝕜 E‖ = 1

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

source

@[simp]

theorem ContinuousLinearMap.nnnorm_id {𝕜 : Type u_1} {E : Type u_4} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [Nontrivial E] :

‖ContinuousLinearMap.id 𝕜 E‖₊ = 1

source

noncomputable instance ContinuousLinearMap.normOneClass {𝕜 : Type u_1} {E : Type u_4} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [Nontrivial E] :

NormOneClass (E →L[𝕜] E)

Equations

⋯ = ⋯

source

noncomputable instance ContinuousLinearMap.toNormedAddCommGroup {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [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

ContinuousLinearMap.toNormedAddCommGroup = NormedAddCommGroup.ofSeparation ⋯

source

noncomputable instance ContinuousLinearMap.toNormedRing {𝕜 : Type u_1} {E : Type u_4} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [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 ⋯ ⋯

source

theorem ContinuousLinearMap.homothety_norm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [Nontrivial E] (f : E →SL[σ₁₂] F) {a : ℝ} (hf : ∀ (x : E), ‖f x‖ = a * ‖x‖) :

‖f‖ = a

source

theorem ContinuousLinearMap.antilipschitz_of_embedding {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [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.

source

@[simp]

theorem LinearIsometry.norm_toContinuousLinearMap {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [Nontrivial E] [RingHomIsometric σ₁₂] (f : E →ₛₗᵢ[σ₁₂] F) :

‖f.toContinuousLinearMap‖ = 1

source

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} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₁₂] (f : F →ₛₗᵢ[σ₂₃] G) {g : E →SL[σ₁₂] F} :

‖f.toContinuousLinearMap.comp g‖ = ‖g‖

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

source

theorem ContinuousLinearMap.opNorm_comp_linearIsometryEquiv {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {F : Type u_6} {G : Type u_8} [NormedAddCommGroup F] [NormedAddCommGroup G] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {𝕜₂' : Type u_11} [NontriviallyNormedField 𝕜₂'] {F' : Type u_12} [NormedAddCommGroup F'] [NormedSpace 𝕜₂' F'] {σ₂' : 𝕜₂' →+* 𝕜₂} {σ₂'' : 𝕜₂ →+* 𝕜₂'} {σ₂₃' : 𝕜₂' →+* 𝕜₃} [RingHomInvPair σ₂' σ₂''] [RingHomInvPair σ₂'' σ₂'] [RingHomCompTriple σ₂' σ₂₃ σ₂₃'] [RingHomCompTriple σ₂'' σ₂₃' σ₂₃] [RingHomIsometric σ₂₃] [RingHomIsometric σ₂'] [RingHomIsometric σ₂''] [RingHomIsometric σ₂₃'] (f : F →SL[σ₂₃] G) (g : F' ≃ₛₗᵢ[σ₂'] F) :

‖f.comp g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖

Precomposition with a linear isometry preserves the operator norm.

source

@[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} [NormedAddCommGroup F] [NormedAddCommGroup G] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {𝕜₂' : Type u_11} [NontriviallyNormedField 𝕜₂'] {F' : Type u_12} [NormedAddCommGroup F'] [NormedSpace 𝕜₂' F'] {σ₂' : 𝕜₂' →+* 𝕜₂} {σ₂'' : 𝕜₂ →+* 𝕜₂'} {σ₂₃' : 𝕜₂' →+* 𝕜₃} [RingHomInvPair σ₂' σ₂''] [RingHomInvPair σ₂'' σ₂'] [RingHomCompTriple σ₂' σ₂₃ σ₂₃'] [RingHomCompTriple σ₂'' σ₂₃' σ₂₃] [RingHomIsometric σ₂₃] [RingHomIsometric σ₂'] [RingHomIsometric σ₂''] [RingHomIsometric σ₂₃'] (f : F →SL[σ₂₃] G) (g : F' ≃ₛₗᵢ[σ₂'] F) :

‖f.comp g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖

Alias of ContinuousLinearMap.opNorm_comp_linearIsometryEquiv.

Precomposition with a linear isometry preserves the operator norm.

source

@[simp]

theorem ContinuousLinearMap.norm_smulRight_apply {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (c : E →L[𝕜] 𝕜) (f : Fₗ) :

‖c.smulRight f‖ = ‖c‖ * ‖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.

source

@[simp]

theorem ContinuousLinearMap.nnnorm_smulRight_apply {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (c : E →L[𝕜] 𝕜) (f : Fₗ) :

‖c.smulRight f‖₊ = ‖c‖₊ * ‖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.

source

noncomputable def ContinuousLinearMap.smulRightL (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [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

ContinuousLinearMap.smulRightL 𝕜 E Fₗ = { toFun := ContinuousLinearMap.smulRightₗ, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous₂ 1 ⋯

Instances For

source

@[simp]

theorem ContinuousLinearMap.norm_smulRightL_apply {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (c : E →L[𝕜] 𝕜) (f : Fₗ) :

‖((ContinuousLinearMap.smulRightL 𝕜 E Fₗ) c) f‖ = ‖c‖ * ‖f‖

source

@[simp]

theorem ContinuousLinearMap.norm_smulRightL {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (c : E →L[𝕜] 𝕜) [Nontrivial Fₗ] :

‖(ContinuousLinearMap.smulRightL 𝕜 E Fₗ) c‖ = ‖c‖

source

theorem ContinuousLinearMap.norm_smulRightL_le {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] :

‖ContinuousLinearMap.smulRightL 𝕜 E Fₗ‖ ≤ 1

source

theorem Submodule.norm_subtypeL {𝕜 : Type u_1} {E : Type u_4} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (K : Submodule 𝕜 E) [Nontrivial ↥K] :

‖K.subtypeL‖ = 1

source

theorem ContinuousLinearEquiv.antilipschitz {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] (e : E ≃SL[σ₁₂] F) :

AntilipschitzWith ‖↑e.symm‖₊ ⇑e

source

theorem ContinuousLinearEquiv.one_le_norm_mul_norm_symm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) :

1 ≤ ‖↑e‖ * ‖↑e.symm‖

source

theorem ContinuousLinearEquiv.norm_pos {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) :

0 < ‖↑e‖

source

theorem ContinuousLinearEquiv.norm_symm_pos {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) :

0 < ‖↑e.symm‖

source

theorem ContinuousLinearEquiv.nnnorm_symm_pos {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) :

0 < ‖↑e.symm‖₊

source

theorem ContinuousLinearEquiv.subsingleton_or_norm_symm_pos {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] (e : E ≃SL[σ₁₂] F) :

Subsingleton E ∨ 0 < ‖↑e.symm‖

source

theorem ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] (e : E ≃SL[σ₁₂] F) :

Subsingleton E ∨ 0 < ‖↑e.symm‖₊

source

@[simp]

theorem ContinuousLinearEquiv.coord_norm (𝕜 : Type u_1) {E : Type u_4} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (x : E) (h : x ≠ 0) :

‖ContinuousLinearEquiv.coord 𝕜 x h‖ = ‖x‖⁻¹

source

noncomputable def IsCoercive {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ ] E →L[ℝ ] ℝ) :

Prop

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

IsCoercive B = ∃ (C : ℝ), 0 < C ∧ ∀ (u : E), C * ‖u‖ * ‖u‖ ≤ (B u) u

Instances For

source

theorem NormedSpace.equicontinuous_TFAE {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {ι : Type u_11} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] (f : ι → E →SL[σ₁₂] F) :

[EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f), ∃ (C : ℝ), ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖, ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖, ∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C, ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C, BddAbove (Set.range fun (x : ι) => ‖f x‖), ⨆ (i : ι), ↑‖f i‖₊ < ⊤].TFAE

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.

Documentation

Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace

Operator norm for maps on normed spaces #