English
For any f and x, the action of liftIsometry on f and x equals the action of lift on the underlying multilinear map.
Русский
Для любого f и x применение liftIsometry к f и x равно применению lift к соответствующей многообразной карте.
LaTeX
$$liftIsometry 𝕜 E F f x = lift f.toMultilinearMap x$$
Lean4
/-- The linear equivalence between `ContinuousMultilinearMap 𝕜 E F` and `(⨂[𝕜] i, Eᵢ) →L[𝕜] F`
induced by `PiTensorProduct.lift`, for every normed space `F`.
-/
@[simps]
noncomputable def liftEquiv : ContinuousMultilinearMap 𝕜 E F ≃ₗ[𝕜] (⨂[𝕜] i, E i) →L[𝕜] F
where
toFun f := LinearMap.mkContinuous (lift f.toMultilinearMap) ‖f‖ fun x ↦ norm_eval_le_injectiveSeminorm f x
map_add' f
g := by ext _;
simp only [ContinuousMultilinearMap.toMultilinearMap_add, map_add, LinearMap.mkContinuous_apply,
LinearMap.add_apply, ContinuousLinearMap.add_apply]
map_smul' a
f := by ext _;
simp only [ContinuousMultilinearMap.toMultilinearMap_smul, map_smul, LinearMap.mkContinuous_apply,
LinearMap.smul_apply, RingHom.id_apply, ContinuousLinearMap.coe_smul', Pi.smul_apply]
invFun
l :=
MultilinearMap.mkContinuous (lift.symm l.toLinearMap) ‖l‖ fun x ↦
by
simp only [lift_symm, LinearMap.compMultilinearMap_apply, ContinuousLinearMap.coe_coe]
exact ContinuousLinearMap.le_opNorm_of_le _ (injectiveSeminorm_tprod_le x)
left_inv
f := by ext x;
simp only [LinearMap.mkContinuous_coe, LinearEquiv.symm_apply_apply, MultilinearMap.coe_mkContinuous,
ContinuousMultilinearMap.coe_coe]
right_inv
l := by
rw [← ContinuousLinearMap.coe_inj]
apply PiTensorProduct.ext; ext m
simp only [lift_symm, LinearMap.mkContinuous_coe, LinearMap.compMultilinearMap_apply, lift.tprod,
ContinuousMultilinearMap.coe_coe, MultilinearMap.coe_mkContinuous, ContinuousLinearMap.coe_coe]
