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
- f.mkContinuousOfExistsBound₂ h = { toFun := fun (x : E) => (f x).mkContinuousOfExistsBound ⋯, map_add' := ⋯, map_smul' := ⋯ }.mkContinuousOfExistsBound ⋯
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
- f.mkContinuous₂ C hC = f.mkContinuousOfExistsBound₂ ⋯
Instances For
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
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
- ContinuousLinearMap.flipₗᵢ 𝕜 E Fₗ Gₗ = { toFun := ContinuousLinearMap.flip, map_add' := ⋯, map_smul' := ⋯, invFun := ContinuousLinearMap.flip, left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }
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.id 𝕜₂ (E →SL[σ₁₂] F)).flip
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.id 𝕜 (E →L[𝕜] Fₗ)).flip
Instances For
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
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.compL 𝕜 Eₗ Fₗ Gₗ).comp L
Instances For
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
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
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
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.
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.
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 ⋯