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).
Alias of ContinuousLinearMap.opNorm_ext
.
Alias of ContinuousLinearMap.opNorm_le_bound₂
.
Alias of ContinuousLinearMap.le_opNorm₂
.
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
- One or more equations did not get rendered due to their size.
Instances For
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
Instances For
Flip the order of arguments of a continuous bilinear map.
For a version bundled as LinearIsometryEquiv
, see
ContinuousLinearMap.flipL
.
Equations
- ContinuousLinearMap.flip f = LinearMap.mkContinuous₂ (LinearMap.mk₂'ₛₗ σ₂₃ σ₁₃ (fun (y : F) (x : E) => (f x) y) ⋯ ⋯ ⋯ ⋯) ‖f‖ ⋯
Instances For
Alias of ContinuousLinearMap.opNorm_flip
.
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
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
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.flip (ContinuousLinearMap.id 𝕜₂ (E →SL[σ₁₂] F))
Instances For
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.flip (ContinuousLinearMap.id 𝕜 (E →L[𝕜] Fₗ))
Instances For
Composition of continuous semilinear maps as a continuous semibilinear map.
Equations
- ContinuousLinearMap.compSL E F G σ₁₂ σ₂₃ = LinearMap.mkContinuous₂ (LinearMap.mk₂'ₛₗ (RingHom.id 𝕜₃) σ₂₃ ContinuousLinearMap.comp ⋯ ⋯ ⋯ ⋯) 1 ⋯
Instances For
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
Apply L(x,-)
pointwise to bilinear maps, as a continuous bilinear map
Equations
- ContinuousLinearMap.precompR Eₗ L = ContinuousLinearMap.comp (ContinuousLinearMap.compL 𝕜 Eₗ Fₗ Gₗ) L
Instances For
Apply L(-,y)
pointwise to bilinear maps, as a continuous bilinear map
Equations
Instances For
Compose a bilinear map E →SL[σ₁₃] F →SL[σ₂₃] G
with two linear maps
E' →SL[σ₁'] E
and F' →SL[σ₂'] F
.
Equations
Instances For
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
- One or more equations did not get rendered due to their size.