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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [FunLike 𝓕 E F] [SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕) (hf : Continuous ⇑f) {x : E} (hx : ‖x‖ = 0) : ‖f x‖ = 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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [FunLike 𝓕 E F] [RingHomIsometric σ₁₂] [SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕) {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) {c : 𝕜} (hc : 1 < ‖c‖) (hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) {x : E} (hx : ‖x‖ ≠ 0) : ‖f x‖ ≤ C * ‖x‖

theorem SemilinearMapClass.bound_of_continuous {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {𝓕 : Type u_10} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [FunLike 𝓕 E F] [RingHomIsometric σ₁₂] [SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕) (hf : Continuous ⇑f) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : E), ‖f x‖ ≤ C * ‖x‖

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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : E), ‖f x‖ ≤ C * ‖x‖

noncomputable def LinearIsometry.toSpanSingleton (𝕜 : Type u_1) (E : Type u_4) [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] {v : E} (hv : ‖v‖ = 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

• LinearIsometry.toSpanSingleton 𝕜 E hv = let __src := LinearMap.toSpanSingleton 𝕜 E v; { toLinearMap := __src, norm_map' := ⋯ }

@[simp]

theorem LinearIsometry.toSpanSingleton_apply {𝕜 : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] {v : E} (hv : ‖v‖ = 1) (a : 𝕜) : (LinearIsometry.toSpanSingleton 𝕜 E hv) a = a • v

@[simp]

theorem LinearIsometry.coe_toSpanSingleton {𝕜 : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] {v : E} (hv : ‖v‖ = 1) : (LinearIsometry.toSpanSingleton 𝕜 E hv).toLinearMap = LinearMap.toSpanSingleton 𝕜 E v

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

• f.opNorm = sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖}

noncomputable instance ContinuousLinearMap.hasOpNorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) : ‖f‖ = sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖}

theorem ContinuousLinearMap.bounds_nonempty {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} : ∃ (c : ℝ), c ∈ {c : ℝ | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖}

theorem ContinuousLinearMap.bounds_bddBelow {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {f : E →SL[σ₁₂] F} : BddBelow {c : ℝ | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖}

theorem ContinuousLinearMap.isLeast_opNorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) : IsLeast {c : ℝ | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖} ‖f‖

@[deprecated ContinuousLinearMap.isLeast_opNorm]

theorem ContinuousLinearMap.isLeast_op_norm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) : IsLeast {c : ℝ | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖} ‖f‖

Alias of ContinuousLinearMap.isLeast_opNorm.

theorem ContinuousLinearMap.opNorm_le_bound {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖) : ‖f‖ ≤ 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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (x : E), ‖f x‖ ≤ M * ‖x‖) : ‖f‖ ≤ 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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (x : E), ‖x‖ ≠ 0 → ‖f x‖ ≤ M * ‖x‖) : ‖f‖ ≤ 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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (x : E), ‖x‖ ≠ 0 → ‖f x‖ ≤ M * ‖x‖) : ‖f‖ ≤ 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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {f : E →SL[σ₁₂] F} {K : NNReal} (hf : LipschitzWith K ⇑f) : ‖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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {f : E →SL[σ₁₂] F} {K : NNReal} (hf : LipschitzWith K ⇑f) : ‖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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {φ : E →SL[σ₁₂] F} {M : ℝ} (M_nonneg : 0 ≤ M) (h_above : ∀ (x : E), ‖φ x‖ ≤ M * ‖x‖) (h_below : ∀ N ≥ 0, (∀ (x : E), ‖φ x‖ ≤ N * ‖x‖) → M ≤ N) : ‖φ‖ = M

@[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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {φ : E →SL[σ₁₂] F} {M : ℝ} (M_nonneg : 0 ≤ M) (h_above : ∀ (x : E), ‖φ x‖ ≤ M * ‖x‖) (h_below : ∀ N ≥ 0, (∀ (x : E), ‖φ x‖ ≤ N * ‖x‖) → M ≤ N) : ‖φ‖ = M

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

@[deprecated ContinuousLinearMap.opNorm_neg]

theorem ContinuousLinearMap.op_norm_neg {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) : ‖-f‖ = ‖f‖

Alias of ContinuousLinearMap.opNorm_neg.

theorem ContinuousLinearMap.opNorm_nonneg {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) : 0 ≤ ‖f‖

@[deprecated ContinuousLinearMap.opNorm_nonneg]

theorem ContinuousLinearMap.op_norm_nonneg {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) : 0 ≤ ‖f‖

Alias of ContinuousLinearMap.opNorm_nonneg.

theorem ContinuousLinearMap.opNorm_zero {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} : ‖0‖ = 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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} : ‖0‖ = 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} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] : ‖ContinuousLinearMap.id 𝕜 E‖ ≤ 1

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

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

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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) (x : E) (y : E) : dist (f x) (f y) ≤ ‖f‖ * 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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) (x : E) (y : E) : dist (f x) (f y) ≤ ‖f‖ * 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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) {x : E} {a : ℝ} {b : ℝ} (hf : ‖f‖ ≤ a) (hx : ‖x‖ ≤ b) : ‖f x‖ ≤ a * b

@[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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) {x : E} {a : ℝ} {b : ℝ} (hf : ‖f‖ ≤ a) (hx : ‖x‖ ≤ b) : ‖f x‖ ≤ a * b

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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) {c : ℝ} {x : E} (h : ‖x‖ ≤ c) : ‖f x‖ ≤ ‖f‖ * c

@[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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) {c : ℝ} {x : E} (h : ‖x‖ ≤ c) : ‖f x‖ ≤ ‖f‖ * c

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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) {c : ℝ} (h : ‖f‖ ≤ c) (x : E) : ‖f x‖ ≤ c * ‖x‖

@[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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) {c : ℝ} (h : ‖f‖ ≤ c) (x : E) : ‖f x‖ ≤ c * ‖x‖

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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} {M : ℝ} (hMp : 0 ≤ M) : ‖f‖ ≤ M ↔ ∀ (x : E), ‖f x‖ ≤ M * ‖x‖

@[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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} {M : ℝ} (hMp : 0 ≤ M) : ‖f‖ ≤ M ↔ ∀ (x : E), ‖f x‖ ≤ M * ‖x‖

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

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

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

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

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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C) {c : 𝕜} (hc : 1 < ‖c‖) (hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ 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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C) {c : 𝕜} (hc : 1 < ‖c‖) (hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ 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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C) (hf : ∀ x ∈ Metric.ball 0 ε, ‖f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ 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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C) (hf : ∀ x ∈ Metric.ball 0 ε, ‖f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ 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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} {C : ℝ} (hC : 0 ≤ C) (hf : ∀ᶠ (x : E) in nhds 0, ‖f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ 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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} {C : ℝ} (hC : 0 ≤ C) (hf : ∀ᶠ (x : E) in nhds 0, ‖f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ 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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C) {c : 𝕜} (hc : ‖c‖ < 1) (hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ 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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C) {c : 𝕜} (hc : ‖c‖ < 1) (hf : ∀ (x : E), ε * ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ C

Alias of ContinuousLinearMap.opNorm_le_of_shell'.

theorem ContinuousLinearMap.opNorm_le_of_unit_norm {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] {f : E →L[ℝ] F} {C : ℝ} (hC : 0 ≤ C) (hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C) : ‖f‖ ≤ 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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] {f : E →L[ℝ] F} {C : ℝ} (hC : 0 ≤ C) (hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C) : ‖f‖ ≤ 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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) (g : E →SL[σ₁₂] F) : ‖f + g‖ ≤ ‖f‖ + ‖g‖

The operator norm satisfies the triangle inequality.

@[deprecated ContinuousLinearMap.opNorm_add_le]

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

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} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (h : ∃ (x : E), ‖x‖ ≠ 0) : ‖ContinuousLinearMap.id 𝕜 E‖ = 1

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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {𝕜' : Type u_11} [NormedField 𝕜'] [NormedSpace 𝕜' F] [SMulCommClass 𝕜₂ 𝕜' F] (c : 𝕜') (f : E →SL[σ₁₂] F) : ‖c • f‖ ≤ ‖c‖ * ‖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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {𝕜' : Type u_11} [NormedField 𝕜'] [NormedSpace 𝕜' F] [SMulCommClass 𝕜₂ 𝕜' F] (c : 𝕜') (f : E →SL[σ₁₂] F) : ‖c • f‖ ≤ ‖c‖ * ‖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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [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

• ContinuousLinearMap.seminorm = Seminorm.ofSMulLE norm ⋯ ⋯ ⋯

noncomputable instance ContinuousLinearMap.toPseudoMetricSpace {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] : PseudoMetricSpace (E →SL[σ₁₂] F)

Equations

• ContinuousLinearMap.toPseudoMetricSpace = SeminormedAddCommGroup.toPseudoMetricSpace.replaceUniformity ⋯

noncomputable instance ContinuousLinearMap.toSeminormedAddCommGroup {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] : SeminormedAddCommGroup (E →SL[σ₁₂] F)

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

Equations

• ContinuousLinearMap.toSeminormedAddCommGroup = SeminormedAddCommGroup.mk ⋯

noncomputable instance ContinuousLinearMap.toNormedSpace {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {𝕜' : Type u_11} [NormedField 𝕜'] [NormedSpace 𝕜' F] [SMulCommClass 𝕜₂ 𝕜' F] : NormedSpace 𝕜' (E →SL[σ₁₂] F)

Equations

• ContinuousLinearMap.toNormedSpace = NormedSpace.mk ⋯

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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₁₂] [RingHomIsometric σ₂₃] (h : F →SL[σ₂₃] G) (f : E →SL[σ₁₂] F) : ‖h.comp f‖ ≤ ‖h‖ * ‖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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₁₂] [RingHomIsometric σ₂₃] (h : F →SL[σ₂₃] G) (f : E →SL[σ₁₂] F) : ‖h.comp f‖ ≤ ‖h‖ * ‖f‖

Alias of ContinuousLinearMap.opNorm_comp_le.

---

The operator norm is submultiplicative.

noncomputable instance ContinuousLinearMap.toSemiNormedRing {𝕜 : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] : SeminormedRing (E →L[𝕜] 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} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [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; NormedAlgebra.mk ⋯

@[simp]

theorem ContinuousLinearMap.opNorm_subsingleton {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) [Subsingleton E] : ‖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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) [Subsingleton E] : ‖f‖ = 0

Alias of ContinuousLinearMap.opNorm_subsingleton.

@[simp]

theorem ContinuousLinearMap.norm_restrictScalars {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] {𝕜' : Type u_11} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [NormedSpace 𝕜' Fₗ] [IsScalarTower 𝕜' 𝕜 Fₗ] (f : E →L[𝕜] Fₗ) : ‖ContinuousLinearMap.restrictScalars 𝕜' f‖ = ‖f‖

noncomputable def ContinuousLinearMap.restrictScalarsIsometry (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (𝕜' : Type u_11) [NontriviallyNormedField 𝕜'] [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

• ContinuousLinearMap.restrictScalarsIsometry 𝕜 E Fₗ 𝕜' 𝕜'' = { toLinearMap := ContinuousLinearMap.restrictScalarsₗ 𝕜 E Fₗ 𝕜' 𝕜'', norm_map' := ⋯ }

@[simp]

theorem ContinuousLinearMap.coe_restrictScalarsIsometry (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (𝕜' : Type u_11) [NontriviallyNormedField 𝕜'] [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ₗ 𝕜' 𝕜'') = ContinuousLinearMap.restrictScalars 𝕜'

@[simp]

theorem ContinuousLinearMap.restrictScalarsIsometry_toLinearMap (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (𝕜' : Type u_11) [NontriviallyNormedField 𝕜'] [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) [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (𝕜' : Type u_11) [NontriviallyNormedField 𝕜'] [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

• ContinuousLinearMap.restrictScalarsL 𝕜 E Fₗ 𝕜' 𝕜'' = (ContinuousLinearMap.restrictScalarsIsometry 𝕜 E Fₗ 𝕜' 𝕜'').toContinuousLinearMap

@[simp]

theorem ContinuousLinearMap.coe_restrictScalarsL {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] {𝕜' : Type u_11} [NontriviallyNormedField 𝕜'] [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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] {𝕜' : Type u_11} [NontriviallyNormedField 𝕜'] [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 𝕜'

theorem ContinuousLinearMap.norm_pi_le_of_le {𝕜 : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] {ι : Type u_11} [Fintype ι] {M : ι → Type u_12} [(i : ι) → SeminormedAddCommGroup (M i)] [(i : ι) → NormedSpace 𝕜 (M i)] {C : ℝ} {L : (i : ι) → E →L[𝕜] M i} (hL : ∀ (i : ι), ‖L i‖ ≤ C) (hC : 0 ≤ C) : ‖ContinuousLinearMap.pi L‖ ≤ C

theorem LinearMap.mkContinuous_norm_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ₁₂] F) {C : ℝ} (hC : 0 ≤ C) (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) : ‖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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ₁₂] F) {C : ℝ} (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) : ‖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} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →ₛₗᵢ[σ₁₂] F) : ‖f.toContinuousLinearMap‖ ≤ 1

theorem Submodule.norm_subtypeL_le {𝕜 : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (K : Submodule 𝕜 E) : ‖K.subtypeL‖ ≤ 1