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_5} [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‖

theorem LinearMap.bound_of_ball_bound {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_6} [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.

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

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

@[deprecated ContinuousLinearMap.opNorm_zero_iff]

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

@[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.

@[simp]

theorem ContinuousLinearMap.nnnorm_id {𝕜 : Type u_1} {E : Type u_4} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [Nontrivial E] : ‖ContinuousLinearMap.id 𝕜 E‖₊ = 1

noncomputable instance ContinuousLinearMap.normOneClass {𝕜 : Type u_1} {E : Type u_4} [NormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [Nontrivial E] : NormOneClass (E →L[𝕜] E)

Equations

• ⋯ = ⋯

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

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 = NormedRing.mk ⋯ ⋯

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

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

@[simp]

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

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

noncomputable def LinearIsometry.postcomp {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₁₂] [RingHomIsometric σ₁₃] (a : F →ₛₗᵢ[σ₂₃] G) : (E →SL[σ₁₂] F) →ₛₗᵢ[σ₂₃] E →SL[σ₁₃] G

Composing on the left with a linear isometry gives a linear isometry between spaces of continuous linear maps.

Equations

• a.postcomp = { toFun := fun (f : E →SL[σ₁₂] F) => a.toContinuousLinearMap.comp f, map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }

theorem ContinuousLinearMap.opNorm_comp_linearIsometryEquiv {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {F : Type u_5} {G : Type u_7} [NormedAddCommGroup F] [NormedAddCommGroup G] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {𝕜₂' : Type u_8} [NontriviallyNormedField 𝕜₂'] {F' : Type u_9} [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.

@[deprecated ContinuousLinearMap.opNorm_comp_linearIsometryEquiv]

theorem ContinuousLinearMap.op_norm_comp_linearIsometryEquiv {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {F : Type u_5} {G : Type u_7} [NormedAddCommGroup F] [NormedAddCommGroup G] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {𝕜₂' : Type u_8} [NontriviallyNormedField 𝕜₂'] {F' : Type u_9} [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.

@[simp]

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

theorem ContinuousLinearMap.norm_smulRightL_le {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] : ‖ContinuousLinearMap.smulRightL 𝕜 E Fₗ‖ ≤ 1

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

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

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

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

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

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

theorem ContinuousLinearEquiv.subsingleton_or_norm_symm_pos {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] (e : E ≃SL[σ₁₂] F) : Subsingleton E ∨ 0 < ‖↑e.symm‖

theorem ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂] (e : E ≃SL[σ₁₂] F) : Subsingleton E ∨ 0 < ‖↑e.symm‖₊

@[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‖⁻¹

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

theorem NormedSpace.equicontinuous_TFAE {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} {ι : Type u_8} [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.