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_5} {𝓕 : Type u_8} [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_5} {𝓕 : Type u_8} [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_5} {𝓕 : Type u_8} [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 SemilinearMapClass.nnbound_of_continuous {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} {𝓕 : Type u_8} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [FunLike 𝓕 E F] [RingHomIsometric σ₁₂] [SemilinearMapClass 𝓕 σ₁₂ E F] (f : 𝓕) (hf : Continuous ⇑f) : ∃ (C : NNReal), 0 < C ∧ ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊

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

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

theorem ContinuousLinearMap.nnbound {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) : ∃ (C : NNReal), 0 < C ∧ ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊

theorem ContinuousLinearMap.ebound {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) : ∃ (C : NNReal), 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 = { toLinearMap := LinearMap.toSpanSingleton 𝕜 E v, 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 : 𝕜) : (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) : (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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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‖

theorem ContinuousLinearMap.opNorm_le_bound {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [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.

theorem ContinuousLinearMap.opNorm_le_bound' {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [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.

theorem ContinuousLinearMap.opNorm_eq_of_bounds {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [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

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

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

theorem ContinuousLinearMap.opNorm_zero {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} : ‖0‖ = 0

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 cannot do better than an inequality in general.

theorem ContinuousLinearMap.le_opNorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [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‖.

theorem ContinuousLinearMap.dist_le_opNorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) (x y : E) : dist (f x) (f y) ≤ ‖f‖ * dist x y

theorem ContinuousLinearMap.le_of_opNorm_le_of_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [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

theorem ContinuousLinearMap.le_opNorm_of_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [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

theorem ContinuousLinearMap.le_of_opNorm_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [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‖

theorem ContinuousLinearMap.opNorm_le_iff {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [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‖

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

theorem ContinuousLinearMap.unit_le_opNorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [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.

theorem ContinuousLinearMap.opNorm_le_of_shell {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [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

theorem ContinuousLinearMap.opNorm_le_of_ball {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [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

theorem ContinuousLinearMap.opNorm_le_of_nhds_zero {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [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

theorem ContinuousLinearMap.opNorm_le_of_shell' {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [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

theorem ContinuousLinearMap.opNorm_le_of_unit_norm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [NormedAlgebra ℝ 𝕜] {f : E →SL[σ₁₂] 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.

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

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

theorem ContinuousLinearMap.opNorm_le_iff_lipschitz {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} {K : NNReal} : ‖f‖ ≤ ↑K ↔ LipschitzWith K ⇑f

theorem ContinuousLinearMap.opNorm_le_of_lipschitz {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} {K : NNReal} : LipschitzWith K ⇑f → ‖f‖ ≤ ↑K

Alias of the reverse direction of ContinuousLinearMap.opNorm_le_iff_lipschitz.

theorem ContinuousLinearMap.lipschitzWith_of_opNorm_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} {K : NNReal} : ‖f‖ ≤ ↑K → LipschitzWith K ⇑f

Alias of the forward direction of ContinuousLinearMap.opNorm_le_iff_lipschitz.

noncomputable def ContinuousLinearMap.seminorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [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_5} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] : PseudoMetricSpace (E →SL[σ₁₂] F)

Equations

• ContinuousLinearMap.toPseudoMetricSpace = ContinuousLinearMap.seminorm.toSeminormedAddCommGroup.replaceUniformity ⋯

noncomputable instance ContinuousLinearMap.toSeminormedAddCommGroup {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [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

• One or more equations did not get rendered due to their size.

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

Equations

• ContinuousLinearMap.toNormedSpace = { toModule := ContinuousLinearMap.module, norm_smul_le := ⋯ }

theorem ContinuousLinearMap.opNorm_comp_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_7} [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.

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

• One or more equations did not get rendered due to their size.

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 = { toSMul := ContinuousLinearMap.toNormedSpace.toSMul, algebraMap := Algebra.algebraMap, commutes' := ⋯, smul_def' := ⋯, norm_smul_le := ⋯ }

@[simp]

theorem ContinuousLinearMap.opNorm_subsingleton {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) [Subsingleton E] : ‖f‖ = 0

theorem ContinuousLinearMap.le_opNorm_enorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [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, expressed with extended norms: ‖f x‖ₑ ≤ ‖f‖ₑ * ‖x‖ₑ.

@[simp]

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

noncomputable def ContinuousLinearMap.restrictScalarsIsometry (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_6) [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (𝕜' : Type u_9) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [NormedSpace 𝕜' Fₗ] [IsScalarTower 𝕜' 𝕜 Fₗ] (𝕜'' : Type u_10) [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_6) [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (𝕜' : Type u_9) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [NormedSpace 𝕜' Fₗ] [IsScalarTower 𝕜' 𝕜 Fₗ] {𝕜'' : Type u_10} [Ring 𝕜''] [Module 𝕜'' Fₗ] [ContinuousConstSMul 𝕜'' Fₗ] [SMulCommClass 𝕜 𝕜'' Fₗ] [SMulCommClass 𝕜' 𝕜'' Fₗ] : ⇑(restrictScalarsIsometry 𝕜 E Fₗ 𝕜' 𝕜'') = restrictScalars 𝕜'

@[simp]

theorem ContinuousLinearMap.restrictScalarsIsometry_toLinearMap (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_6) [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (𝕜' : Type u_9) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [NormedSpace 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [NormedSpace 𝕜' Fₗ] [IsScalarTower 𝕜' 𝕜 Fₗ] {𝕜'' : Type u_10} [Ring 𝕜''] [Module 𝕜'' Fₗ] [ContinuousConstSMul 𝕜'' Fₗ] [SMulCommClass 𝕜 𝕜'' Fₗ] [SMulCommClass 𝕜' 𝕜'' Fₗ] : (restrictScalarsIsometry 𝕜 E Fₗ 𝕜' 𝕜'').toLinearMap = restrictScalarsₗ 𝕜 E Fₗ 𝕜' 𝕜''

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

theorem LinearMap.mkContinuous_norm_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [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_5} [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_5} [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