# 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).

source
theorem ContinuousLinearMap.opNorm_ext {𝕜 : 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] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₁₃] (f : E →SL[σ₁₂] F) (g : E →SL[σ₁₃] G) (h : ∀ (x : E), ‖f x‖ = ‖g x‖) :
‖f‖ = ‖g‖
source
theorem ContinuousLinearMap.opNorm_le_bound₂ {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) {C : ℝ} (h0 : 0 ≤ C) (hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖) :
‖f‖ ≤ C
source
theorem ContinuousLinearMap.le_opNorm₂ {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (x : E) (y : F) :
‖(f x) y‖ ≤ ‖f‖ * ‖x‖ * ‖y‖
source
theorem ContinuousLinearMap.le_of_opNorm₂_le_of_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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [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
source
theorem LinearMap.norm_mkContinuous₂_aux {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} (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‖
source
noncomputable def LinearMap.mkContinuousOfExistsBound₂ {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [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`.

Equations

- f.mkContinuousOfExistsBound₂ h = { toFun := fun (x : E) => (f x).mkContinuousOfExistsBound ⋯, map_add' := ⋯, map_smul' := ⋯ }.mkContinuousOfExistsBound ⋯

Instances For

source
noncomputable def LinearMap.mkContinuous₂ {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [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.

Equations

- f.mkContinuous₂ C hC = f.mkContinuousOfExistsBound₂ ⋯

Instances For

source
@[simp]
theorem LinearMap.mkContinuous₂_apply {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [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
source
theorem LinearMap.mkContinuous₂_norm_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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) {C : ℝ} (hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖) :
‖f.mkContinuous₂ C hC‖ ≤ max C 0
source
theorem LinearMap.mkContinuous₂_norm_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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [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
source
noncomputable def ContinuousLinearMap.flip {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] (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`.

Equations

- f.flip = (LinearMap.mk₂'ₛₗ σ₂₃ σ₁₃ (fun (y : F) (x : E) => (f x) y) ⋯ ⋯ ⋯ ⋯).mkContinuous₂ ‖f‖ ⋯

Instances For

source
@[simp]
theorem ContinuousLinearMap.flip_apply {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (x : E) (y : F) :
(f.flip y) x = (f x) y
source
@[simp]
theorem ContinuousLinearMap.flip_flip {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) :
f.flip.flip = f
source
@[simp]
theorem ContinuousLinearMap.opNorm_flip {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) :
‖f.flip‖ = ‖f‖
source
@[simp]
theorem ContinuousLinearMap.flip_zero {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] :
flip 0 = 0
source
@[simp]
theorem ContinuousLinearMap.flip_add {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] (f g : E →SL[σ₁₃] F →SL[σ₂₃] G) :
(f + g).flip = f.flip + g.flip
source
@[simp]
theorem ContinuousLinearMap.flip_smul {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] (c : 𝕜₃) (f : E →SL[σ₁₃] F →SL[σ₂₃] G) :
(c • f).flip = c • f.flip
source
noncomputable def ContinuousLinearMap.flipₗᵢ' {𝕜 : 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] (σ₂₃ : 𝕜₂ →+* 𝕜₃) (σ₁₃ : 𝕜 →+* 𝕜₃) [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`.

Equations

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

Instances For

source
@[simp]
theorem ContinuousLinearMap.flipₗᵢ'_symm {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] :
(flipₗᵢ' E F G σ₂₃ σ₁₃).symm = flipₗᵢ' F E G σ₁₃ σ₂₃
source
@[simp]
theorem ContinuousLinearMap.coe_flipₗᵢ' {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃] :
⇑(flipₗᵢ' E F G σ₂₃ σ₁₃) = flip
source
noncomputable def ContinuousLinearMap.flipₗᵢ (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) (Gₗ : Type u_9) [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`.

Equations

- ContinuousLinearMap.flipₗᵢ 𝕜 E Fₗ Gₗ = { toFun := ContinuousLinearMap.flip, map_add' := ⋯, map_smul' := ⋯, invFun := ContinuousLinearMap.flip, left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }

Instances For

source
@[simp]
theorem ContinuousLinearMap.flipₗᵢ_symm {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} {Gₗ : Type u_9} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] :
(flipₗᵢ 𝕜 E Fₗ Gₗ).symm = flipₗᵢ 𝕜 Fₗ E Gₗ
source
@[simp]
theorem ContinuousLinearMap.coe_flipₗᵢ {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} {Gₗ : Type u_9} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] :
⇑(flipₗᵢ 𝕜 E Fₗ Gₗ) = flip
source
noncomputable def ContinuousLinearMap.apply' {𝕜 : 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 σ₁₂] :
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 `LinearMap.applyₗ`.

Equations

- ContinuousLinearMap.apply' F σ₁₂ = (ContinuousLinearMap.id 𝕜₂ (E →SL[σ₁₂] F)).flip

Instances For

source
@[simp]
theorem ContinuousLinearMap.apply_apply' {𝕜 : 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 σ₁₂] (v : E) (f : E →SL[σ₁₂] F) :
((apply' F σ₁₂) v) f = f v
source
noncomputable def ContinuousLinearMap.apply (𝕜 : Type u_1) {E : Type u_4} (Fₗ : Type u_7) [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 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 `LinearMap.applyₗ`.

Equations

- ContinuousLinearMap.apply 𝕜 Fₗ = (ContinuousLinearMap.id 𝕜 (E →L[𝕜] Fₗ)).flip

Instances For

source
@[simp]
theorem ContinuousLinearMap.apply_apply {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (v : E) (f : E →L[𝕜] Fₗ) :
((apply 𝕜 Fₗ) v) f = f v
source
noncomputable def ContinuousLinearMap.compSL {𝕜 : 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 σ₁₃] [RingHomIsometric σ₁₂] :
(F →SL[σ₂₃] G) →L[𝕜₃] (E →SL[σ₁₂] F) →SL[σ₂₃] E →SL[σ₁₃] G

Composition of continuous semilinear maps as a continuous semibilinear map.

Equations

- ContinuousLinearMap.compSL E F G σ₁₂ σ₂₃ = (LinearMap.mk₂'ₛₗ (RingHom.id 𝕜₃) σ₂₃ ContinuousLinearMap.comp ⋯ ⋯ ⋯ ⋯).mkContinuous₂ 1 ⋯

Instances For

source
theorem ContinuousLinearMap.norm_compSL_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 σ₁₃] [RingHomIsometric σ₁₂] :
‖compSL E F G σ₁₂ σ₂₃‖ ≤ 1
source
@[simp]
theorem ContinuousLinearMap.compSL_apply {𝕜 : 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 σ₁₃] [RingHomIsometric σ₁₂] (f : F →SL[σ₂₃] G) (g : E →SL[σ₁₂] F) :
((compSL E F G σ₁₂ σ₂₃) f) g = f.comp g
source
theorem Continuous.const_clm_comp {𝕜 : 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 σ₁₃] [RingHomIsometric σ₁₂] {X : Type u_11} [TopologicalSpace X] {f : X → E →SL[σ₁₂] F} (hf : Continuous f) (g : F →SL[σ₂₃] G) :
Continuous fun (x : X) => g.comp (f x)
source
theorem Continuous.clm_comp_const {𝕜 : 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 σ₁₃] [RingHomIsometric σ₁₂] {X : Type u_11} [TopologicalSpace X] {g : X → F →SL[σ₂₃] G} (hg : Continuous g) (f : E →SL[σ₁₂] F) :
Continuous fun (x : X) => (g x).comp f
source
noncomputable def ContinuousLinearMap.compL (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) (Gₗ : Type u_9) [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] :
(Fₗ →L[𝕜] Gₗ) →L[𝕜] (E →L[𝕜] Fₗ) →L[𝕜] E →L[𝕜] Gₗ

Composition of continuous linear maps as a continuous bilinear map.

Equations

- ContinuousLinearMap.compL 𝕜 E Fₗ Gₗ = ContinuousLinearMap.compSL E Fₗ Gₗ (RingHom.id 𝕜) (RingHom.id 𝕜)

Instances For

source
theorem ContinuousLinearMap.norm_compL_le (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) (Gₗ : Type u_9) [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] :
‖compL 𝕜 E Fₗ Gₗ‖ ≤ 1
source
@[simp]
theorem ContinuousLinearMap.compL_apply (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) (Gₗ : Type u_9) [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] (f : Fₗ →L[𝕜] Gₗ) (g : E →L[𝕜] Fₗ) :
((compL 𝕜 E Fₗ Gₗ) f) g = f.comp g
source
noncomputable def ContinuousLinearMap.precompR {𝕜 : Type u_1} {E : Type u_4} (Eₗ : Type u_5) {Fₗ : Type u_7} {Gₗ : Type u_9} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Eₗ] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Eₗ] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] (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

Equations

- ContinuousLinearMap.precompR Eₗ L = (ContinuousLinearMap.compL 𝕜 Eₗ Fₗ Gₗ).comp L

Instances For

source
@[simp]
theorem ContinuousLinearMap.precompR_apply {𝕜 : Type u_1} {E : Type u_4} (Eₗ : Type u_5) {Fₗ : Type u_7} {Gₗ : Type u_9} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Eₗ] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Eₗ] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) (a✝ : E) :
(precompR Eₗ L) a✝ = (compL 𝕜 Eₗ Fₗ Gₗ) (L a✝)
source
noncomputable def ContinuousLinearMap.precompL {𝕜 : Type u_1} {E : Type u_4} (Eₗ : Type u_5) {Fₗ : Type u_7} {Gₗ : Type u_9} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Eₗ] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Eₗ] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] (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

Equations

- ContinuousLinearMap.precompL Eₗ L = (ContinuousLinearMap.precompR Eₗ L.flip).flip

Instances For

source
@[simp]
theorem ContinuousLinearMap.precompL_apply {𝕜 : Type u_1} {E : Type u_4} (Eₗ : Type u_5) {Fₗ : Type u_7} {Gₗ : Type u_9} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Eₗ] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Eₗ] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) (u : Eₗ →L[𝕜] E) (f : Fₗ) (g : Eₗ) :
(((precompL Eₗ L) u) f) g = (L (u g)) f
source
theorem ContinuousLinearMap.norm_precompR_le {𝕜 : Type u_1} {E : Type u_4} (Eₗ : Type u_5) {Fₗ : Type u_7} {Gₗ : Type u_9} [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‖
source
theorem ContinuousLinearMap.norm_precompL_le {𝕜 : Type u_1} {E : Type u_4} (Eₗ : Type u_5) {Fₗ : Type u_7} {Gₗ : Type u_9} [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‖
source
noncomputable def ContinuousLinearMap.bilinearComp {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {E' : Type u_11} {F' : Type u_12} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {𝕜₁' : Type u_13} {𝕜₂' : Type u_14} [NontriviallyNormedField 𝕜₁'] [NontriviallyNormedField 𝕜₂'] [NormedSpace 𝕜₁' E'] [NormedSpace 𝕜₂' 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`.

Equations

- f.bilinearComp gE gF = ((f.comp gE).flip.comp gF).flip

Instances For

source
@[simp]
theorem ContinuousLinearMap.bilinearComp_apply {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {E' : Type u_11} {F' : Type u_12} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {𝕜₁' : Type u_13} {𝕜₂' : Type u_14} [NontriviallyNormedField 𝕜₁'] [NontriviallyNormedField 𝕜₂'] [NormedSpace 𝕜₁' E'] [NormedSpace 𝕜₂' 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)
source
@[simp]
theorem ContinuousLinearMap.bilinearComp_zero {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {E' : Type u_11} {F' : Type u_12} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {𝕜₁' : Type u_13} {𝕜₂' : Type u_14} [NontriviallyNormedField 𝕜₁'] [NontriviallyNormedField 𝕜₂'] [NormedSpace 𝕜₁' E'] [NormedSpace 𝕜₂' F'] {σ₁' : 𝕜₁' →+* 𝕜} {σ₁₃' : 𝕜₁' →+* 𝕜₃} {σ₂' : 𝕜₂' →+* 𝕜₂} {σ₂₃' : 𝕜₂' →+* 𝕜₃} [RingHomCompTriple σ₁' σ₁₃ σ₁₃'] [RingHomCompTriple σ₂' σ₂₃ σ₂₃'] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃'] [RingHomIsometric σ₂₃'] {gE : E' →SL[σ₁'] E} {gF : F' →SL[σ₂'] F} :
bilinearComp 0 gE gF = 0
source
@[simp]
theorem ContinuousLinearMap.bilinearComp_zero_left {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {E' : Type u_11} {F' : Type u_12} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {𝕜₁' : Type u_13} {𝕜₂' : Type u_14} [NontriviallyNormedField 𝕜₁'] [NontriviallyNormedField 𝕜₂'] [NormedSpace 𝕜₁' E'] [NormedSpace 𝕜₂' F'] {σ₁' : 𝕜₁' →+* 𝕜} {σ₁₃' : 𝕜₁' →+* 𝕜₃} {σ₂' : 𝕜₂' →+* 𝕜₂} {σ₂₃' : 𝕜₂' →+* 𝕜₃} [RingHomCompTriple σ₁' σ₁₃ σ₁₃'] [RingHomCompTriple σ₂' σ₂₃ σ₂₃'] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃'] [RingHomIsometric σ₂₃'] {f : E →SL[σ₁₃] F →SL[σ₂₃] G} {gF : F' →SL[σ₂'] F} :
f.bilinearComp 0 gF = 0
source
@[simp]
theorem ContinuousLinearMap.bilinearComp_zero_right {𝕜 : 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] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {E' : Type u_11} {F' : Type u_12} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {𝕜₁' : Type u_13} {𝕜₂' : Type u_14} [NontriviallyNormedField 𝕜₁'] [NontriviallyNormedField 𝕜₂'] [NormedSpace 𝕜₁' E'] [NormedSpace 𝕜₂' F'] {σ₁' : 𝕜₁' →+* 𝕜} {σ₁₃' : 𝕜₁' →+* 𝕜₃} {σ₂' : 𝕜₂' →+* 𝕜₂} {σ₂₃' : 𝕜₂' →+* 𝕜₃} [RingHomCompTriple σ₁' σ₁₃ σ₁₃'] [RingHomCompTriple σ₂' σ₂₃ σ₂₃'] [RingHomIsometric σ₂₃] [RingHomIsometric σ₁₃'] [RingHomIsometric σ₂₃'] {f : E →SL[σ₁₃] F →SL[σ₂₃] G} {gE : E' →SL[σ₁'] E} :
f.bilinearComp gE 0 = 0
source
noncomputable def ContinuousLinearMap.deriv₂ {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} {Gₗ : Type u_9} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] (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.

Equations

- f.deriv₂ = f.bilinearComp (ContinuousLinearMap.fst 𝕜 E Fₗ) (ContinuousLinearMap.snd 𝕜 E Fₗ) + f.flip.bilinearComp (ContinuousLinearMap.snd 𝕜 E Fₗ) (ContinuousLinearMap.fst 𝕜 E Fₗ)

Instances For

source
@[simp]
theorem ContinuousLinearMap.coe_deriv₂ {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} {Gₗ : Type u_9} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] (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
source
theorem ContinuousLinearMap.map_add_add {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} {Gₗ : Type u_9} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [SeminormedAddCommGroup Gₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] (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'
source
@[simp]
theorem ContinuousLinearMap.norm_smulRight_apply {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [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.

source
@[simp]
theorem ContinuousLinearMap.nnnorm_smulRight_apply {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [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.

source
noncomputable def ContinuousLinearMap.smulRightL (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 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`.

Equations

- ContinuousLinearMap.smulRightL 𝕜 E Fₗ = { toFun := ContinuousLinearMap.smulRightₗ, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous₂ 1 ⋯

Instances For

source
@[simp]
theorem ContinuousLinearMap.norm_smulRightL_apply {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] (c : StrongDual 𝕜 E) (f : Fₗ) :
‖((smulRightL 𝕜 E Fₗ) c) f‖ = ‖c‖ * ‖f‖
source
noncomputable def ContinuousLinearMap.bilinearRestrictScalars (𝕜 : Type u_1) {E : Type u_4} {F : Type u_6} {G : Type u_8} {𝕜' : Type u_11} [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.

Equations

- ContinuousLinearMap.bilinearRestrictScalars 𝕜 B = (ContinuousLinearMap.restrictScalarsL 𝕜' F G 𝕜 𝕜).comp (ContinuousLinearMap.restrictScalars 𝕜 B)

Instances For

source
theorem ContinuousLinearMap.bilinearRestrictScalars_eq_restrictScalarsL_comp_restrictScalars {𝕜 : Type u_1} {E : Type u_4} {F : Type u_6} {G : Type u_8} {𝕜' : Type u_11} [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 𝕜 𝕜).comp (restrictScalars 𝕜 B)
source
theorem ContinuousLinearMap.bilinearRestrictScalars_eq_restrictScalars_restrictScalarsL_comp {𝕜 : Type u_1} {E : Type u_4} {F : Type u_6} {G : Type u_8} {𝕜' : Type u_11} [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 𝕜 𝕜').comp B)
source
@[simp]
theorem ContinuousLinearMap.bilinearRestrictScalars_apply_apply (𝕜 : Type u_1) {E : Type u_4} {F : Type u_6} {G : Type u_8} {𝕜' : Type u_11} [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
source
@[simp]
theorem ContinuousLinearMap.norm_bilinearRestrictScalars {𝕜 : Type u_1} {E : Type u_4} {F : Type u_6} {G : Type u_8} {𝕜' : Type u_11} [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‖