Documentation

Mathlib.Analysis.NormedSpace.OperatorNorm.Basic

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

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) :
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
Instances For
    @[simp]
    theorem LinearIsometry.toSpanSingleton_apply {π•œ : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField π•œ] [NormedSpace π•œ E] {v : E} (hv : β€–vβ€– = 1) (a : π•œ) :
    @[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
    Instances For
      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) :
      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) :
      @[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) :

      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β€–) :

      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β€–) :

      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β€–) :

      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β€–) :

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

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

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

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

      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] {σ₁₂ : π•œ β†’+* π•œβ‚‚} :

      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] {σ₁₂ : π•œ β†’+* π•œβ‚‚} :

      Alias of ContinuousLinearMap.opNorm_zero.


      The norm of the 0 operator is 0.

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

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

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

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

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

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

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

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

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

      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β€–) :
      @[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β€–) :

      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β€–) :
      @[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β€–) :

      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β€–) :
      @[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β€–) :

      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β€–) :
      @[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β€–) :

      Alias of ContinuousLinearMap.opNorm_le_of_shell'.

      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]

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

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

      Alias of ContinuousLinearMap.opNorm_add_le.


      The operator norm satisfies the triangle inequality.

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

      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
      Instances For
        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
        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
        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) :

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

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

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

        Equations
        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
        @[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] :
        @[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] :

        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β‚—) :
        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
        Instances For
          @[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β‚— π•œ' π•œ''
          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) :
          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