English
The map liftIsometry preserves norms up to the operator norm of f; in particular, norm_map' ensures bound.
Русский
ЛифтИзометрия сохраняет нормы в пределах операционной нормы f; нормирование ограничено.
LaTeX
$$norm_map' := (for all f, ‖lift f.toMultilinearMap‖ ≤ ‖f‖)$$
Lean4
/-- For a normed space `F`, we have constructed in `PiTensorProduct.liftEquiv` the canonical
linear equivalence between `ContinuousMultilinearMap 𝕜 E F` and `(⨂[𝕜] i, Eᵢ) →L[𝕜] F`
(induced by `PiTensorProduct.lift`). Here we give the upgrade of this equivalence to
an isometric linear equivalence; in particular, it is a continuous linear equivalence.
-/
noncomputable def liftIsometry : ContinuousMultilinearMap 𝕜 E F ≃ₗᵢ[𝕜] (⨂[𝕜] i, E i) →L[𝕜] F :=
{ liftEquiv 𝕜 E F with
norm_map' := by
intro f
refine le_antisymm ?_ ?_
· simp only [liftEquiv_apply]
exact LinearMap.mkContinuous_norm_le _ (norm_nonneg f) _
· conv_lhs => rw [← (liftEquiv 𝕜 E F).symm_apply_apply f]
rw [liftEquiv_symm_apply]
exact MultilinearMap.mkContinuous_norm_le _ (norm_nonneg _) _ }
