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_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‖)
:
@[deprecated ContinuousLinearMap.opNorm_ext]
theorem
ContinuousLinearMap.op_norm_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‖)
:
Alias of ContinuousLinearMap.opNorm_ext.
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‖)
:
@[deprecated ContinuousLinearMap.opNorm_le_bound₂]
theorem
ContinuousLinearMap.op_norm_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‖)
:
Alias of ContinuousLinearMap.opNorm_le_bound₂.
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)
:
@[deprecated ContinuousLinearMap.le_opNorm₂]
theorem
ContinuousLinearMap.le_op_norm₂
{𝕜 : 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)
:
Alias of ContinuousLinearMap.le_opNorm₂.
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)
:
@[deprecated ContinuousLinearMap.le_of_opNorm₂_le_of_le]
theorem
ContinuousLinearMap.le_of_op_norm₂_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)
:
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)
:
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‖)
:
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
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‖)
:
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
@[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
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‖)
:
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‖)
:
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)
:
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
@[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
@[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
@[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)
:
@[deprecated ContinuousLinearMap.opNorm_flip]
theorem
ContinuousLinearMap.op_norm_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)
:
Alias of ContinuousLinearMap.opNorm_flip.
@[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)
:
@[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)
:
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 σ₁₃]
:
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
@[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 σ₁₃]
:
(ContinuousLinearMap.flipₗᵢ' E F G σ₂₃ σ₁₃).symm = ContinuousLinearMap.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_6}
{G : Type u_8}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
{σ₁₃ : 𝕜 →+* 𝕜₃}
[RingHomIsometric σ₂₃]
[RingHomIsometric σ₁₃]
:
⇑(ContinuousLinearMap.flipₗᵢ' E F G σ₂₃ σ₁₃) = ContinuousLinearMap.flip
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ₗ]
:
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
@[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ₗ]
:
(ContinuousLinearMap.flipₗᵢ 𝕜 E Fₗ Gₗ).symm = ContinuousLinearMap.flipₗᵢ 𝕜 Fₗ E Gₗ
@[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ₗ]
:
⇑(ContinuousLinearMap.flipₗᵢ 𝕜 E Fₗ Gₗ) = ContinuousLinearMap.flip
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 σ₁₂]
:
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
@[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)
:
((ContinuousLinearMap.apply' F σ₁₂) v) f = f v
noncomputable def
ContinuousLinearMap.apply
(𝕜 : Type u_1)
{E : Type u_4}
(Fₗ : Type u_7)
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Fₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 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
@[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ₗ)
:
((ContinuousLinearMap.apply 𝕜 Fₗ) v) f = f v
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 σ₁₂]
:
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
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 σ₁₂]
:
‖ContinuousLinearMap.compSL E F G σ₁₂ σ₂₃‖ ≤ 1
@[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)
:
((ContinuousLinearMap.compSL E F G σ₁₂ σ₂₃) f) g = f.comp g
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)
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
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ₗ]
:
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
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ₗ]
:
‖ContinuousLinearMap.compL 𝕜 E Fₗ Gₗ‖ ≤ 1
@[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ₗ)
:
((ContinuousLinearMap.compL 𝕜 E Fₗ Gₗ) f) g = f.comp g
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ₗ)
:
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
@[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)
:
(ContinuousLinearMap.precompR Eₗ L) a✝ = (ContinuousLinearMap.compL 𝕜 Eₗ Fₗ Gₗ) (L a✝)
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ₗ)
:
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
@[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ₗ)
:
(((ContinuousLinearMap.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_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ₗ)
:
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ₗ)
:
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)
:
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
@[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)
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ₗ)
:
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
@[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ₗ)
:
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ₗ)
:
@[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 : E →L[𝕜] 𝕜)
(f : Fₗ)
:
The norm of the tensor product of a scalar linear map and of an element of a normed space is the product of the norms.
@[simp]
theorem
ContinuousLinearMap.nnnorm_smulRight_apply
{𝕜 : Type u_1}
{E : Type u_4}
{Fₗ : Type u_7}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Fₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Fₗ]
(c : E →L[𝕜] 𝕜)
(f : Fₗ)
:
The non-negative norm of the tensor product of a scalar linear map and of an element of a normed space is the product of the non-negative norms.
noncomputable def
ContinuousLinearMap.smulRightL
(𝕜 : Type u_1)
(E : Type u_4)
(Fₗ : Type u_7)
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup Fₗ]
[NontriviallyNormedField 𝕜]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜 Fₗ]
:
ContinuousLinearMap.smulRight as a continuous trilinear map:
smulRightL (c : E →L[𝕜] 𝕜) (f : F) (x : E) = c x • f.
Equations
- ContinuousLinearMap.smulRightL 𝕜 E Fₗ = { toFun := ContinuousLinearMap.smulRightₗ, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous₂ 1 ⋯
Instances For
@[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 : E →L[𝕜] 𝕜)
(f : Fₗ)
:
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)
:
Convenience function for restricting the linearity of a bilinear map.
Equations
- ContinuousLinearMap.bilinearRestrictScalars 𝕜 B = (ContinuousLinearMap.restrictScalarsL 𝕜' F G 𝕜 𝕜).comp (ContinuousLinearMap.restrictScalars 𝕜 B)
Instances For
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)
:
ContinuousLinearMap.bilinearRestrictScalars 𝕜 B = (ContinuousLinearMap.restrictScalarsL 𝕜' F G 𝕜 𝕜).comp (ContinuousLinearMap.restrictScalars 𝕜 B)
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)
:
ContinuousLinearMap.bilinearRestrictScalars 𝕜 B = ContinuousLinearMap.restrictScalars 𝕜 ((ContinuousLinearMap.restrictScalarsL 𝕜' F G 𝕜 𝕜').comp B)
@[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)
:
((ContinuousLinearMap.bilinearRestrictScalars 𝕜 B) x) y = (B x) y
@[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)
: