Operator norm: bilinear maps

This file contains lemmas concerning operator norm as applied to bilinear maps E × F → G, interpreted as linear maps E → F → G as usual (and similarly for semilinear variants).

theorem ContinuousLinearMap.opNorm_ext {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_8} {G : Type u_12} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₁₃] (f : E →SL[σ₁₂] F) (g : E →SL[σ₁₃] G) (h : ∀ (x : E), ‖f x‖ = ‖g x‖) : ‖f‖ = ‖g‖

theorem ContinuousLinearMap.opNorm_le_bound₂ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_8} {G : Type u_12} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) {C : ℝ} (h0 : 0 ≤ C) (hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖) : ‖f‖ ≤ C

theorem ContinuousLinearMap.le_opNorm₂ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_8} {G : Type u_12} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (x : E) (y : F) : ‖(f x) y‖ ≤ ‖f‖ * ‖x‖ * ‖y‖

theorem ContinuousLinearMap.le_of_opNorm₂_le_of_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_8} {G : Type u_12} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) {x : E} {y : F} {a b c : ℝ} (hf : ‖f‖ ≤ a) (hx : ‖x‖ ≤ b) (hy : ‖y‖ ≤ c) : ‖(f x) y‖ ≤ a * b * c

theorem ContinuousLinearMap.opENorm_le_bound₂ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_8} {G : Type u_12} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) {C : ENNReal} (hC : ∀ (x : E) (y : F), ‖(f x) y‖ₑ ≤ C * ‖x‖ₑ * ‖y‖ₑ) : ‖f‖ₑ ≤ C

theorem ContinuousLinearMap.le_opENorm₂ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_8} {G : Type u_12} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (x : E) (y : F) : ‖(f x) y‖ₑ ≤ ‖f‖ₑ * ‖x‖ₑ * ‖y‖ₑ

theorem LinearMap.norm_mkContinuous₂_aux {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_8} {G : Type u_12} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) (C : ℝ) (h : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖) (x : E) : ‖(f x).mkContinuous (C * ‖x‖) ⋯‖ ≤ max C 0 * ‖x‖

noncomputable def LinearMap.mkContinuousOfExistsBound₂ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_8} {G : Type u_12} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) (h : ∃ (C : ℝ), ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖) : E →SL[σ₁₃] F →SL[σ₂₃] G

Create a bilinear map (represented as a map E →L[𝕜] F →L[𝕜] G) from the corresponding linear map and existence of a bound on the norm of the image. The linear map can be constructed using LinearMap.mk₂.

If you have an explicit bound, use LinearMap.mkContinuous₂ instead, as a norm estimate will follow automatically in LinearMap.mkContinuous₂_norm_le.

noncomputable def LinearMap.mkContinuous₂ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_8} {G : Type u_12} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) (C : ℝ) (hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖) : E →SL[σ₁₃] F →SL[σ₂₃] G

Create a bilinear map (represented as a map E →L[𝕜] F →L[𝕜] G) from the corresponding linear map and a bound on the norm of the image. The linear map can be constructed using LinearMap.mk₂. Lemmas LinearMap.mkContinuous₂_norm_le' and LinearMap.mkContinuous₂_norm_le provide estimates on the norm of an operator constructed using this function.

@[simp]

theorem LinearMap.mkContinuous₂_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_8} {G : Type u_12} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) {C : ℝ} (hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖) (x : E) (y : F) : ((f.mkContinuous₂ C hC) x) y = (f x) y

theorem LinearMap.mkContinuous₂_norm_le' {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_8} {G : Type u_12} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) {C : ℝ} (hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖) : ‖f.mkContinuous₂ C hC‖ ≤ max C 0

theorem LinearMap.mkContinuous₂_norm_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_8} {G : Type u_12} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) {C : ℝ} (h0 : 0 ≤ C) (hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖) : ‖f.mkContinuous₂ C hC‖ ≤ C

noncomputable def LinearMap.mkContinuous₂OfExists {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E' : Type u_6} {F' : Type u_10} {G' : Type u_14} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [AddCommGroup G'] [Module 𝕜₃ G'] [TopologicalSpace G'] [IsNormableSpace 𝕜₃ G'] [IsTopologicalAddGroup G'] (f : E' →ₛₗ[σ₁₃] F' →ₛₗ[σ₂₃] G') (hf : ∃ (g : E' →SL[σ₁₃] F' →SL[σ₂₃] G'), ∀ (a : E') (b : F'), (f a) b = (g a) b) : E' →SL[σ₁₃] F' →SL[σ₂₃] G'

Given a bilinear map, convert it to a continuous bilinear map if there exists a continuous bilinear map which coincides with it. This may seem silly: why not use the witness directly? The reason to use this is good definitional behavior: in use cases for normable spaces, the witness is constructed by putting a norm on the space, so it has a complicated definition which the kernel struggles with, while the output of the current definition is definitionally much nicer.

noncomputable def ContinuousLinearMap.flip {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E' : Type u_6} {F' : Type u_10} {G' : Type u_14} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [AddCommGroup G'] [Module 𝕜₃ G'] [TopologicalSpace G'] [IsNormableSpace 𝕜₃ G'] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup G'] (f : E' →SL[σ₁₃] F' →SL[σ₂₃] G') : F' →SL[σ₂₃] E' →SL[σ₁₃] G'

Flip the order of arguments of a continuous bilinear map. For a version bundled as LinearIsometryEquiv, see ContinuousLinearMap.flipL.

@[simp]

theorem ContinuousLinearMap.flip_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E' : Type u_6} {F' : Type u_10} {G' : Type u_14} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [AddCommGroup G'] [Module 𝕜₃ G'] [TopologicalSpace G'] [IsNormableSpace 𝕜₃ G'] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup G'] (f : E' →SL[σ₁₃] F' →SL[σ₂₃] G') (x : E') (y : F') : (f.flip y) x = (f x) y

@[simp]

theorem ContinuousLinearMap.flip_flip {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E' : Type u_6} {F' : Type u_10} {G' : Type u_14} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [AddCommGroup G'] [Module 𝕜₃ G'] [TopologicalSpace G'] [IsNormableSpace 𝕜₃ G'] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup G'] (f : E' →SL[σ₁₃] F' →SL[σ₂₃] G') : f.flip.flip = f

@[simp]

theorem ContinuousLinearMap.opNorm_flip {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_8} {G : Type u_12} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f.flip‖ = ‖f‖

@[simp]

theorem ContinuousLinearMap.opNNNorm_flip {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_8} {G : Type u_12} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f.flip‖₊ = ‖f‖₊

@[simp]

theorem ContinuousLinearMap.opENorm_flip {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_8} {G : Type u_12} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f.flip‖ₑ = ‖f‖ₑ

@[simp]

theorem ContinuousLinearMap.flip_zero {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E' : Type u_6} {F' : Type u_10} {G' : Type u_14} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [AddCommGroup G'] [Module 𝕜₃ G'] [TopologicalSpace G'] [IsNormableSpace 𝕜₃ G'] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup G'] : flip 0 = 0

@[simp]

theorem ContinuousLinearMap.flip_add {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E' : Type u_6} {F' : Type u_10} {G' : Type u_14} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [AddCommGroup G'] [Module 𝕜₃ G'] [TopologicalSpace G'] [IsNormableSpace 𝕜₃ G'] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup G'] (f g : E' →SL[σ₁₃] F' →SL[σ₂₃] G') : (f + g).flip = f.flip + g.flip

@[simp]

theorem ContinuousLinearMap.flip_smul {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E' : Type u_6} {F' : Type u_10} {G' : Type u_14} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [AddCommGroup G'] [Module 𝕜₃ G'] [TopologicalSpace G'] [IsNormableSpace 𝕜₃ G'] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup G'] (c : 𝕜₃) (f : E' →SL[σ₁₃] F' →SL[σ₂₃] G') : (c • f).flip = c • f.flip

noncomputable def ContinuousLinearMap.flipₗᵢ' {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} (E : Type u_4) (F : Type u_8) (G : Type u_12) [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] (σ₂₃ : 𝕜₂ →+* 𝕜₃) (σ₁₃ : 𝕜 →+* 𝕜₃) [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] : (E →SL[σ₁₃] F →SL[σ₂₃] G) ≃ₗᵢ[𝕜₃] F →SL[σ₂₃] E →SL[σ₁₃] G

Flip the order of arguments of a continuous bilinear map. This is a version bundled as a LinearIsometryEquiv. For an unbundled version see ContinuousLinearMap.flip.

@[simp]

theorem ContinuousLinearMap.flipₗᵢ'_symm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_8} {G : Type u_12} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] : (flipₗᵢ' E F G σ₂₃ σ₁₃).symm = flipₗᵢ' F E G σ₁₃ σ₂₃

@[simp]

theorem ContinuousLinearMap.coe_flipₗᵢ' {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_8} {G : Type u_12} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] : ⇑(flipₗᵢ' E F G σ₂₃ σ₁₃) = flip

noncomputable def ContinuousLinearMap.flipₗᵢ (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_9) (Gₗ : Type u_13) [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] : (E →L[𝕜] Fₗ →L[𝕜] Gₗ) ≃ₗᵢ[𝕜] Fₗ →L[𝕜] E →L[𝕜] Gₗ

Flip the order of arguments of a continuous bilinear map. This is a version bundled as a LinearIsometryEquiv. For an unbundled version see ContinuousLinearMap.flip.

@[simp]

theorem ContinuousLinearMap.flipₗᵢ_symm {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_9} {Gₗ : Type u_13} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] : (flipₗᵢ 𝕜 E Fₗ Gₗ).symm = flipₗᵢ 𝕜 Fₗ E Gₗ

@[simp]

theorem ContinuousLinearMap.coe_flipₗᵢ {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_9} {Gₗ : Type u_13} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] : ⇑(flipₗᵢ 𝕜 E Fₗ Gₗ) = flip

noncomputable def ContinuousLinearMap.apply' {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E' : Type u_6} (F' : Type u_10) [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] (σ₁₂ : 𝕜 →+* 𝕜₂) [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [IsNormableSpace 𝕜 E'] [RingHomIsometric σ₁₂] [IsTopologicalAddGroup F'] : E' →SL[σ₁₂] (E' →SL[σ₁₂] F') →L[𝕜₂] F'

The continuous semilinear map obtained by applying a continuous semilinear map at a given vector.

This is the continuous version of applyₗ (and the fully continuous version of LinearMap.applyₗ).

@[simp]

theorem ContinuousLinearMap.apply_apply' {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E' : Type u_6} {F' : Type u_10} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [IsNormableSpace 𝕜 E'] [RingHomIsometric σ₁₂] [IsTopologicalAddGroup F'] (v : E') (f : E' →SL[σ₁₂] F') : ((apply' F' σ₁₂) v) f = f v

@[simp]

theorem ContinuousLinearMap.toLinearMap_apply' {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E' : Type u_6} {F' : Type u_10} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [IsNormableSpace 𝕜 E'] [RingHomIsometric σ₁₂] [IsTopologicalAddGroup F'] : ↑(apply' F' σ₁₂) = applyₗ F' σ₁₂

noncomputable def ContinuousLinearMap.apply (𝕜 : Type u_1) {E' : Type u_6} (Fₗ' : Type u_11) [NontriviallyNormedField 𝕜] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ'] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup Fₗ'] : E' →L[𝕜] (E' →L[𝕜] Fₗ') →L[𝕜] Fₗ'

The continuous semilinear map obtained by applying a continuous semilinear map at a given vector.

This is the continuous version of applyₗ (and fully continuous version of LinearMap.applyₗ).

@[simp]

theorem ContinuousLinearMap.apply_apply {𝕜 : Type u_1} {E' : Type u_6} {Fₗ' : Type u_11} [NontriviallyNormedField 𝕜] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ'] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup Fₗ'] (v : E') (f : E' →L[𝕜] Fₗ') : ((apply 𝕜 Fₗ') v) f = f v

@[simp]

theorem ContinuousLinearMap.toLinearMap_apply {𝕜 : Type u_1} {E' : Type u_6} {Fₗ' : Type u_11} [NontriviallyNormedField 𝕜] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ'] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup Fₗ'] : ↑(apply 𝕜 Fₗ') = applyₗ Fₗ' (RingHom.id 𝕜)

noncomputable def ContinuousLinearMap.compSLₗ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} (E' : Type u_6) (F' : Type u_10) (G' : Type u_14) [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] (σ₁₂ : 𝕜 →+* 𝕜₂) (σ₂₃ : 𝕜₂ →+* 𝕜₃) {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [AddCommGroup G'] [Module 𝕜₃ G'] [TopologicalSpace G'] [IsNormableSpace 𝕜₃ G'] [IsTopologicalAddGroup G'] [IsTopologicalAddGroup F'] : (F' →SL[σ₂₃] G') →ₗ[𝕜₃] (E' →SL[σ₁₂] F') →ₛₗ[σ₂₃] E' →SL[σ₁₃] G'

Composition of continuous semilinear maps as a semibilinear map. Do not use: use instead the version compSL which outputs a continuous semibilinear map.

noncomputable def ContinuousLinearMap.compSL {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} (E' : Type u_6) (F' : Type u_10) (G' : Type u_14) [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] (σ₁₂ : 𝕜 →+* 𝕜₂) (σ₂₃ : 𝕜₂ →+* 𝕜₃) {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [AddCommGroup G'] [Module 𝕜₃ G'] [TopologicalSpace G'] [IsNormableSpace 𝕜₃ G'] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup G'] [RingHomIsometric σ₁₂] [IsTopologicalAddGroup F'] : (F' →SL[σ₂₃] G') →L[𝕜₃] (E' →SL[σ₁₂] F') →SL[σ₂₃] E' →SL[σ₁₃] G'

Composition of continuous semilinear maps as a continuous semibilinear map.

theorem ContinuousLinearMap.norm_compSL_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} (E : Type u_4) (F : Type u_8) (G : Type u_12) [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₃ G] (σ₁₂ : 𝕜 →+* 𝕜₂) (σ₂₃ : 𝕜₂ →+* 𝕜₃) {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] [RingHomIsometric σ₁₂] : ‖compSL E F G σ₁₂ σ₂₃‖ ≤ 1

@[simp]

theorem ContinuousLinearMap.compSL_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E' : Type u_6} {F' : Type u_10} {G' : Type u_14} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [AddCommGroup G'] [Module 𝕜₃ G'] [TopologicalSpace G'] [IsNormableSpace 𝕜₃ G'] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup G'] [RingHomIsometric σ₁₂] [IsTopologicalAddGroup F'] (f : F' →SL[σ₂₃] G') (g : E' →SL[σ₁₂] F') : ((compSL E' F' G' σ₁₂ σ₂₃) f) g = f ∘SL g

theorem Continuous.const_clm_comp {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E' : Type u_6} {F' : Type u_10} {G' : Type u_14} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [AddCommGroup G'] [Module 𝕜₃ G'] [TopologicalSpace G'] [IsNormableSpace 𝕜₃ G'] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup G'] [RingHomIsometric σ₁₂] [IsTopologicalAddGroup F'] {X : Type u_16} [TopologicalSpace X] {f : X → E' →SL[σ₁₂] F'} (hf : Continuous f) (g : F' →SL[σ₂₃] G') : Continuous fun (x : X) => g ∘SL f x

theorem Continuous.clm_comp_const {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E' : Type u_6} {F' : Type u_10} {G' : Type u_14} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [AddCommGroup G'] [Module 𝕜₃ G'] [TopologicalSpace G'] [IsNormableSpace 𝕜₃ G'] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup G'] [RingHomIsometric σ₁₂] [IsTopologicalAddGroup F'] {X : Type u_16} [TopologicalSpace X] {g : X → F' →SL[σ₂₃] G'} (hg : Continuous g) (f : E' →SL[σ₁₂] F') : Continuous fun (x : X) => g x ∘SL f

noncomputable def ContinuousLinearMap.compL (𝕜 : Type u_1) (E' : Type u_6) (Fₗ' : Type u_11) (Gₗ' : Type u_15) [NontriviallyNormedField 𝕜] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ'] [AddCommGroup Gₗ'] [Module 𝕜 Gₗ'] [TopologicalSpace Gₗ'] [IsNormableSpace 𝕜 Gₗ'] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup Gₗ'] [IsTopologicalAddGroup Fₗ'] : (Fₗ' →L[𝕜] Gₗ') →L[𝕜] (E' →L[𝕜] Fₗ') →L[𝕜] E' →L[𝕜] Gₗ'

Composition of continuous linear maps as a continuous bilinear map.

theorem ContinuousLinearMap.norm_compL_le (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_9) (Gₗ : Type u_13) [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] : ‖compL 𝕜 E Fₗ Gₗ‖ ≤ 1

@[simp]

theorem ContinuousLinearMap.compL_apply (𝕜 : Type u_1) (E' : Type u_6) (Fₗ' : Type u_11) (Gₗ' : Type u_15) [NontriviallyNormedField 𝕜] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ'] [AddCommGroup Gₗ'] [Module 𝕜 Gₗ'] [TopologicalSpace Gₗ'] [IsNormableSpace 𝕜 Gₗ'] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup Gₗ'] [IsTopologicalAddGroup Fₗ'] (f : Fₗ' →L[𝕜] Gₗ') (g : E' →L[𝕜] Fₗ') : ((compL 𝕜 E' Fₗ' Gₗ') f) g = f ∘SL g

noncomputable def ContinuousLinearMap.precompR {𝕜 : Type u_1} {E' : Type u_6} (Eₗ' : Type u_7) {Fₗ' : Type u_11} {Gₗ' : Type u_15} [NontriviallyNormedField 𝕜] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup Eₗ'] [Module 𝕜 Eₗ'] [TopologicalSpace Eₗ'] [IsNormableSpace 𝕜 Eₗ'] [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ'] [AddCommGroup Gₗ'] [Module 𝕜 Gₗ'] [TopologicalSpace Gₗ'] [IsNormableSpace 𝕜 Gₗ'] [IsTopologicalAddGroup Gₗ'] [IsTopologicalAddGroup Fₗ'] (L : E' →L[𝕜] Fₗ' →L[𝕜] Gₗ') : E' →L[𝕜] (Eₗ' →L[𝕜] Fₗ') →L[𝕜] Eₗ' →L[𝕜] Gₗ'

Apply L(x,-) pointwise to bilinear maps, as a continuous bilinear map

@[simp]

theorem ContinuousLinearMap.precompR_apply {𝕜 : Type u_1} {E' : Type u_6} (Eₗ' : Type u_7) {Fₗ' : Type u_11} {Gₗ' : Type u_15} [NontriviallyNormedField 𝕜] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup Eₗ'] [Module 𝕜 Eₗ'] [TopologicalSpace Eₗ'] [IsNormableSpace 𝕜 Eₗ'] [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ'] [AddCommGroup Gₗ'] [Module 𝕜 Gₗ'] [TopologicalSpace Gₗ'] [IsNormableSpace 𝕜 Gₗ'] [IsTopologicalAddGroup Gₗ'] [IsTopologicalAddGroup Fₗ'] (L : E' →L[𝕜] Fₗ' →L[𝕜] Gₗ') (x : E') : (precompR Eₗ' L) x = (compL 𝕜 Eₗ' Fₗ' Gₗ') (L x)

noncomputable def ContinuousLinearMap.precompL {𝕜 : Type u_1} {E' : Type u_6} (Eₗ' : Type u_7) {Fₗ' : Type u_11} {Gₗ' : Type u_15} [NontriviallyNormedField 𝕜] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup Eₗ'] [Module 𝕜 Eₗ'] [TopologicalSpace Eₗ'] [IsNormableSpace 𝕜 Eₗ'] [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ'] [AddCommGroup Gₗ'] [Module 𝕜 Gₗ'] [TopologicalSpace Gₗ'] [IsNormableSpace 𝕜 Gₗ'] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup Gₗ'] [IsTopologicalAddGroup E'] (L : E' →L[𝕜] Fₗ' →L[𝕜] Gₗ') : (Eₗ' →L[𝕜] E') →L[𝕜] Fₗ' →L[𝕜] Eₗ' →L[𝕜] Gₗ'

Apply L(-,y) pointwise to bilinear maps, as a continuous bilinear map

@[simp]

theorem ContinuousLinearMap.precompL_apply {𝕜 : Type u_1} {E' : Type u_6} (Eₗ' : Type u_7) {Fₗ' : Type u_11} {Gₗ' : Type u_15} [NontriviallyNormedField 𝕜] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup Eₗ'] [Module 𝕜 Eₗ'] [TopologicalSpace Eₗ'] [IsNormableSpace 𝕜 Eₗ'] [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ'] [AddCommGroup Gₗ'] [Module 𝕜 Gₗ'] [TopologicalSpace Gₗ'] [IsNormableSpace 𝕜 Gₗ'] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup Gₗ'] [IsTopologicalAddGroup E'] (L : E' →L[𝕜] Fₗ' →L[𝕜] Gₗ') (u : Eₗ' →L[𝕜] E') (f : Fₗ') (g : Eₗ') : (((precompL Eₗ' L) u) f) g = (L (u g)) f

theorem ContinuousLinearMap.norm_precompR_le {𝕜 : Type u_1} {E : Type u_4} (Eₗ : Type u_5) {Fₗ : Type u_9} {Gₗ : Type u_13} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Eₗ] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Eₗ] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) : ‖precompR Eₗ L‖ ≤ ‖L‖

theorem ContinuousLinearMap.norm_precompL_le {𝕜 : Type u_1} {E : Type u_4} (Eₗ : Type u_5) {Fₗ : Type u_9} {Gₗ : Type u_13} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Eₗ] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Eₗ] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) : ‖precompL Eₗ L‖ ≤ ‖L‖

noncomputable def ContinuousLinearMap.bilinearComp {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E' : Type u_6} {F' : Type u_10} {G' : Type u_14} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [AddCommGroup G'] [Module 𝕜₃ G'] [TopologicalSpace G'] [IsNormableSpace 𝕜₃ G'] {E'' : Type u_16} {F'' : Type u_17} [AddCommGroup E''] [AddCommGroup F''] [TopologicalSpace E''] [TopologicalSpace F''] [IsTopologicalAddGroup G'] {𝕜₁' : Type u_18} {𝕜₂' : Type u_19} [NontriviallyNormedField 𝕜₁'] [NontriviallyNormedField 𝕜₂'] [Module 𝕜₁' E''] [Module 𝕜₂' F''] [IsNormableSpace 𝕜₁' E''] [IsNormableSpace 𝕜₂' F''] {σ₁' : 𝕜₁' →+* 𝕜} {σ₁₃' : 𝕜₁' →+* 𝕜₃} {σ₂' : 𝕜₂' →+* 𝕜₂} {σ₂₃' : 𝕜₂' →+* 𝕜₃} [RingHomCompTriple σ₁' σ₁₃ σ₁₃'] [RingHomCompTriple σ₂' σ₂₃ σ₂₃'] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃'] [RingHomIsometric σ₂₃'] (f : E' →SL[σ₁₃] F' →SL[σ₂₃] G') (gE : E'' →SL[σ₁'] E') (gF : F'' →SL[σ₂'] F') : E'' →SL[σ₁₃'] F'' →SL[σ₂₃'] G'

Compose a bilinear map E' →SL[σ₁₃] F' →SL[σ₂₃] G' with two linear maps E'' →SL[σ₁'] E' and F'' →SL[σ₂'] F'.

@[simp]

theorem ContinuousLinearMap.bilinearComp_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E' : Type u_6} {F' : Type u_10} {G' : Type u_14} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [AddCommGroup G'] [Module 𝕜₃ G'] [TopologicalSpace G'] [IsNormableSpace 𝕜₃ G'] {E'' : Type u_16} {F'' : Type u_17} [AddCommGroup E''] [AddCommGroup F''] [TopologicalSpace E''] [TopologicalSpace F''] [IsTopologicalAddGroup G'] {𝕜₁' : Type u_18} {𝕜₂' : Type u_19} [NontriviallyNormedField 𝕜₁'] [NontriviallyNormedField 𝕜₂'] [Module 𝕜₁' E''] [Module 𝕜₂' F''] [IsNormableSpace 𝕜₁' E''] [IsNormableSpace 𝕜₂' F''] {σ₁' : 𝕜₁' →+* 𝕜} {σ₁₃' : 𝕜₁' →+* 𝕜₃} {σ₂' : 𝕜₂' →+* 𝕜₂} {σ₂₃' : 𝕜₂' →+* 𝕜₃} [RingHomCompTriple σ₁' σ₁₃ σ₁₃'] [RingHomCompTriple σ₂' σ₂₃ σ₂₃'] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃'] [RingHomIsometric σ₂₃'] (f : E' →SL[σ₁₃] F' →SL[σ₂₃] G') (gE : E'' →SL[σ₁'] E') (gF : F'' →SL[σ₂'] F') (x : E'') (y : F'') : ((f.bilinearComp gE gF) x) y = (f (gE x)) (gF y)

@[simp]

theorem ContinuousLinearMap.bilinearComp_zero {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E' : Type u_6} {F' : Type u_10} {G' : Type u_14} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [AddCommGroup G'] [Module 𝕜₃ G'] [TopologicalSpace G'] [IsNormableSpace 𝕜₃ G'] {E'' : Type u_16} {F'' : Type u_17} [AddCommGroup E''] [AddCommGroup F''] [TopologicalSpace E''] [TopologicalSpace F''] [IsTopologicalAddGroup G'] {𝕜₁' : Type u_18} {𝕜₂' : Type u_19} [NontriviallyNormedField 𝕜₁'] [NontriviallyNormedField 𝕜₂'] [Module 𝕜₁' E''] [Module 𝕜₂' F''] [IsNormableSpace 𝕜₁' E''] [IsNormableSpace 𝕜₂' F''] {σ₁' : 𝕜₁' →+* 𝕜} {σ₁₃' : 𝕜₁' →+* 𝕜₃} {σ₂' : 𝕜₂' →+* 𝕜₂} {σ₂₃' : 𝕜₂' →+* 𝕜₃} [RingHomCompTriple σ₁' σ₁₃ σ₁₃'] [RingHomCompTriple σ₂' σ₂₃ σ₂₃'] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃'] [RingHomIsometric σ₂₃'] {gE : E'' →SL[σ₁'] E'} {gF : F'' →SL[σ₂'] F'} : bilinearComp 0 gE gF = 0

@[simp]

theorem ContinuousLinearMap.bilinearComp_zero_left {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E' : Type u_6} {F' : Type u_10} {G' : Type u_14} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [AddCommGroup G'] [Module 𝕜₃ G'] [TopologicalSpace G'] [IsNormableSpace 𝕜₃ G'] {E'' : Type u_16} {F'' : Type u_17} [AddCommGroup E''] [AddCommGroup F''] [TopologicalSpace E''] [TopologicalSpace F''] [IsTopologicalAddGroup G'] {𝕜₁' : Type u_18} {𝕜₂' : Type u_19} [NontriviallyNormedField 𝕜₁'] [NontriviallyNormedField 𝕜₂'] [Module 𝕜₁' E''] [Module 𝕜₂' F''] [IsNormableSpace 𝕜₁' E''] [IsNormableSpace 𝕜₂' F''] {σ₁' : 𝕜₁' →+* 𝕜} {σ₁₃' : 𝕜₁' →+* 𝕜₃} {σ₂' : 𝕜₂' →+* 𝕜₂} {σ₂₃' : 𝕜₂' →+* 𝕜₃} [RingHomCompTriple σ₁' σ₁₃ σ₁₃'] [RingHomCompTriple σ₂' σ₂₃ σ₂₃'] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃'] [RingHomIsometric σ₂₃'] {f : E' →SL[σ₁₃] F' →SL[σ₂₃] G'} {gF : F'' →SL[σ₂'] F'} : f.bilinearComp 0 gF = 0

@[simp]

theorem ContinuousLinearMap.bilinearComp_zero_right {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E' : Type u_6} {F' : Type u_10} {G' : Type u_14} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup F'] [Module 𝕜₂ F'] [TopologicalSpace F'] [IsNormableSpace 𝕜₂ F'] [AddCommGroup G'] [Module 𝕜₃ G'] [TopologicalSpace G'] [IsNormableSpace 𝕜₃ G'] {E'' : Type u_16} {F'' : Type u_17} [AddCommGroup E''] [AddCommGroup F''] [TopologicalSpace E''] [TopologicalSpace F''] [IsTopologicalAddGroup G'] {𝕜₁' : Type u_18} {𝕜₂' : Type u_19} [NontriviallyNormedField 𝕜₁'] [NontriviallyNormedField 𝕜₂'] [Module 𝕜₁' E''] [Module 𝕜₂' F''] [IsNormableSpace 𝕜₁' E''] [IsNormableSpace 𝕜₂' F''] {σ₁' : 𝕜₁' →+* 𝕜} {σ₁₃' : 𝕜₁' →+* 𝕜₃} {σ₂' : 𝕜₂' →+* 𝕜₂} {σ₂₃' : 𝕜₂' →+* 𝕜₃} [RingHomCompTriple σ₁' σ₁₃ σ₁₃'] [RingHomCompTriple σ₂' σ₂₃ σ₂₃'] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃'] [RingHomIsometric σ₂₃'] {f : E' →SL[σ₁₃] F' →SL[σ₂₃] G'} {gE : E'' →SL[σ₁'] E'} : f.bilinearComp gE 0 = 0

noncomputable def ContinuousLinearMap.deriv₂ {𝕜 : Type u_1} {E' : Type u_6} {Fₗ' : Type u_11} {Gₗ' : Type u_15} [NontriviallyNormedField 𝕜] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ'] [AddCommGroup Gₗ'] [Module 𝕜 Gₗ'] [TopologicalSpace Gₗ'] [IsNormableSpace 𝕜 Gₗ'] [IsTopologicalAddGroup Gₗ'] [IsNormableSpace 𝕜 E'] (f : E' →L[𝕜] Fₗ' →L[𝕜] Gₗ') : E' × Fₗ' →L[𝕜] E' × Fₗ' →L[𝕜] Gₗ'

Derivative of a continuous bilinear map f : E →L[𝕜] F →L[𝕜] G interpreted as a map E × F → G at point p : E × F evaluated at q : E × F, as a continuous bilinear map.

@[simp]

theorem ContinuousLinearMap.coe_deriv₂ {𝕜 : Type u_1} {E' : Type u_6} {Fₗ' : Type u_11} {Gₗ' : Type u_15} [NontriviallyNormedField 𝕜] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ'] [AddCommGroup Gₗ'] [Module 𝕜 Gₗ'] [TopologicalSpace Gₗ'] [IsNormableSpace 𝕜 Gₗ'] [IsTopologicalAddGroup Gₗ'] [IsNormableSpace 𝕜 E'] (f : E' →L[𝕜] Fₗ' →L[𝕜] Gₗ') (p : E' × Fₗ') : ⇑(f.deriv₂ p) = fun (q : E' × Fₗ') => (f p.1) q.2 + (f q.1) p.2

theorem ContinuousLinearMap.map_add_add {𝕜 : Type u_1} {E' : Type u_6} {Fₗ' : Type u_11} {Gₗ' : Type u_15} [NontriviallyNormedField 𝕜] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ'] [AddCommGroup Gₗ'] [Module 𝕜 Gₗ'] [TopologicalSpace Gₗ'] [IsNormableSpace 𝕜 Gₗ'] [IsTopologicalAddGroup Gₗ'] [IsNormableSpace 𝕜 E'] (f : E' →L[𝕜] Fₗ' →L[𝕜] Gₗ') (x x' : E') (y y' : Fₗ') : (f (x + x')) (y + y') = (f x) y + (f.deriv₂ (x, y)) (x', y') + (f x') y'

@[simp]

theorem ContinuousLinearMap.norm_smulRight_apply {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_9} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (c : StrongDual 𝕜 E) (f : Fₗ) : ‖smulRight c f‖ = ‖c‖ * ‖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_9} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (c : StrongDual 𝕜 E) (f : Fₗ) : ‖smulRight c f‖₊ = ‖c‖₊ * ‖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.

@[simp]

theorem ContinuousLinearMap.norm_toSpanSingleton {𝕜 : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (x : E) : ‖toSpanSingleton 𝕜 x‖ = ‖x‖

@[simp]

theorem ContinuousLinearMap.nnnorm_toSpanSingleton {𝕜 : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] (x : E) : ‖toSpanSingleton 𝕜 x‖₊ = ‖x‖₊

noncomputable def ContinuousLinearMap.smulRightLₗ (𝕜 : Type u_1) (E' : Type u_6) (Fₗ' : Type u_11) [NontriviallyNormedField 𝕜] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ'] [IsTopologicalAddGroup Fₗ'] : StrongDual 𝕜 E' →ₗ[𝕜] Fₗ' →ₗ[𝕜] E' →L[𝕜] Fₗ'

ContinuousLinearMap.smulRight as a trilinear map: smulRightLₗ (c : StrongDual 𝕜 E) (f : F) (x : E) = c x • f. Do not use: use instead smulRightL which outputs a continuous trilinear map.

@[simp]

theorem ContinuousLinearMap.smulRightLₗ_apply_apply (𝕜 : Type u_1) (E' : Type u_6) (Fₗ' : Type u_11) [NontriviallyNormedField 𝕜] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ'] [IsTopologicalAddGroup Fₗ'] (c : E' →L[𝕜] 𝕜) (f : Fₗ') : ((smulRightLₗ 𝕜 E' Fₗ') c) f = c.smulRight f

noncomputable def ContinuousLinearMap.smulRightL (𝕜 : Type u_1) (E' : Type u_6) (Fₗ' : Type u_11) [NontriviallyNormedField 𝕜] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ'] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup Fₗ'] : StrongDual 𝕜 E' →L[𝕜] Fₗ' →L[𝕜] E' →L[𝕜] Fₗ'

ContinuousLinearMap.smulRight as a continuous trilinear map: smulRightL (c : StrongDual 𝕜 E) (f : F) (x : E) = c x • f.

This is also known as a rank-one operator. See also InnerProductSpace.rankOne for the rank-one operator on Hilbert spaces.

@[simp]

theorem ContinuousLinearMap.smulRightL_apply_apply (𝕜 : Type u_1) (E' : Type u_6) (Fₗ' : Type u_11) [NontriviallyNormedField 𝕜] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ'] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup Fₗ'] (a : StrongDual 𝕜 E') (b : Fₗ') : ((smulRightL 𝕜 E' Fₗ') a) b = smulRight a b

noncomputable def ContinuousLinearMap.bilinearRestrictScalars (𝕜 : Type u_1) {E : Type u_4} {F : Type u_8} {G : Type u_12} {𝕜' : Type u_16} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedSpace 𝕜' G] [IsScalarTower 𝕜 𝕜' G] (B : E →L[𝕜'] F →L[𝕜'] G) : E →L[𝕜] F →L[𝕜] G

Convenience function for restricting the linearity of a bilinear map.

theorem ContinuousLinearMap.bilinearRestrictScalars_eq_restrictScalarsL_comp_restrictScalars {𝕜 : Type u_1} {E : Type u_4} {F : Type u_8} {G : Type u_12} {𝕜' : Type u_16} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedSpace 𝕜' G] [IsScalarTower 𝕜 𝕜' G] (B : E →L[𝕜'] F →L[𝕜'] G) : bilinearRestrictScalars 𝕜 B = restrictScalarsL 𝕜' F G 𝕜 𝕜 ∘SL restrictScalars 𝕜 B

theorem ContinuousLinearMap.bilinearRestrictScalars_eq_restrictScalars_restrictScalarsL_comp {𝕜 : Type u_1} {E : Type u_4} {F : Type u_8} {G : Type u_12} {𝕜' : Type u_16} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedSpace 𝕜' G] [IsScalarTower 𝕜 𝕜' G] (B : E →L[𝕜'] F →L[𝕜'] G) : bilinearRestrictScalars 𝕜 B = restrictScalars 𝕜 (restrictScalarsL 𝕜' F G 𝕜 𝕜' ∘SL B)

@[simp]

theorem ContinuousLinearMap.bilinearRestrictScalars_apply_apply (𝕜 : Type u_1) {E : Type u_4} {F : Type u_8} {G : Type u_12} {𝕜' : Type u_16} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedSpace 𝕜' G] [IsScalarTower 𝕜 𝕜' G] (B : E →L[𝕜'] F →L[𝕜'] G) (x : E) (y : F) : ((bilinearRestrictScalars 𝕜 B) x) y = (B x) y

@[simp]

theorem ContinuousLinearMap.norm_bilinearRestrictScalars {𝕜 : Type u_1} {E : Type u_4} {F : Type u_8} {G : Type u_12} {𝕜' : Type u_16} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedSpace 𝕜' G] [IsScalarTower 𝕜 𝕜' G] (B : E →L[𝕜'] F →L[𝕜'] G) : ‖bilinearRestrictScalars 𝕜 B‖ = ‖B‖