Documentation

Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace

Operator norm for maps on normed spaces #

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

theorem LinearMap.bound_of_shell {π•œ : Type u_1} {π•œβ‚‚ : Type u_2} {E : Type u_4} {F : Type u_6} [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) :
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.

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
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 σ₁₂] :

An operator is zero iff its norm vanishes.

@[deprecated ContinuousLinearMap.opNorm_zero_iff]
theorem ContinuousLinearMap.op_norm_zero_iff {π•œ : Type u_1} {π•œβ‚‚ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œβ‚‚] [NormedSpace π•œ E] [NormedSpace π•œβ‚‚ F] {σ₁₂ : π•œ β†’+* π•œβ‚‚} (f : E β†’SL[σ₁₂] F) [RingHomIsometric σ₁₂] :

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] :

If a normed space is non-trivial, then the norm of the identity equals 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_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
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 β‹― β‹―
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β€–) :
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.

@[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) :
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} :

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

theorem ContinuousLinearMap.opNorm_comp_linearIsometryEquiv {π•œβ‚‚ : Type u_2} {π•œβ‚ƒ : Type u_3} {F : Type u_6} {G : Type u_8} [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) :

Precomposition with a linear isometry preserves the operator norm.

@[deprecated ContinuousLinearMap.opNorm_comp_linearIsometryEquiv]
theorem ContinuousLinearMap.op_norm_comp_linearIsometryEquiv {π•œβ‚‚ : Type u_2} {π•œβ‚ƒ : Type u_3} {F : Type u_6} {G : Type u_8} [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) :

Alias of ContinuousLinearMap.opNorm_comp_linearIsometryEquiv.


Precomposition with a linear isometry preserves the operator norm.

@[simp]
theorem ContinuousLinearMap.norm_smulRight_apply {π•œ : Type u_1} {E : Type u_4} {Fβ‚— : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fβ‚—] [NontriviallyNormedField π•œ] [NormedSpace π•œ E] [NormedSpace π•œ Fβ‚—] (c : E β†’L[π•œ] π•œ) (f : Fβ‚—) :

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

@[simp]
theorem ContinuousLinearMap.nnnorm_smulRight_apply {π•œ : Type u_1} {E : Type u_4} {Fβ‚— : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup Fβ‚—] [NontriviallyNormedField π•œ] [NormedSpace π•œ E] [NormedSpace π•œ Fβ‚—] (c : E β†’L[π•œ] π•œ) (f : Fβ‚—) :

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

noncomputable def ContinuousLinearMap.smulRightL (π•œ : Type u_1) (E : Type u_4) (Fβ‚— : Type u_7) [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
Instances For
    @[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β‚—) :
    @[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β‚—] :
    theorem Submodule.norm_subtypeL {π•œ : Type u_1} {E : Type u_4} [NormedAddCommGroup E] [NontriviallyNormedField π•œ] [NormedSpace π•œ E] (K : Submodule π•œ E) [Nontrivial β†₯K] :
    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) :
    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) :
    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β€–
    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) :
    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) :
    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) :
    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) :
    @[simp]

    A bounded bilinear form B in a real normed space is coercive if there is some positive constant C such that C * β€–uβ€– * β€–uβ€– ≀ B u u.

    Equations
    Instances For
      theorem NormedSpace.equicontinuous_TFAE {π•œ : Type u_1} {π•œβ‚‚ : Type u_2} {E : Type u_4} {F : Type u_6} {ΞΉ : Type u_11} [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œβ‚‚] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [RingHomIsometric σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace π•œ E] [NormedSpace π•œβ‚‚ F] (f : ΞΉ β†’ E β†’SL[σ₁₂] F) :
      List.TFAE [EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f), βˆƒ (C : ℝ), βˆ€ (i : ΞΉ) (x : E), β€–(f i) xβ€– ≀ C * β€–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β€–β‚Š < ⊀]

      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.