English
The operator norm of mapLMultilinear is at most 1: ||mapLMultilinear|| ≤ 1.
Русский
Операторная норма mapLMultilinear не превышает единицу: ||mapLMultilinear|| ≤ 1.
LaTeX
$$$ \\|\\mathrm{mapLMultilinear} \\| \\le 1 $$$
Lean4
theorem mapL_opNorm : ‖mapL f‖ ≤ ∏ i, ‖f i‖ :=
by
rw [ContinuousLinearMap.opNorm_le_iff (by positivity)]
intro x
rw [mapL, liftIsometry]
simp only [LinearIsometryEquiv.coe_mk, liftEquiv_apply, LinearMap.mkContinuous_apply]
refine le_trans (norm_eval_le_injectiveSeminorm _ _) (mul_le_mul_of_nonneg_right ?_ (norm_nonneg x))
rw [ContinuousMultilinearMap.opNorm_le_iff (Finset.prod_nonneg (fun _ _ ↦ norm_nonneg _))]
intro m
simp only [ContinuousMultilinearMap.compContinuousLinearMap_apply]
refine le_trans (injectiveSeminorm_tprod_le (fun i ↦ (f i) (m i))) ?_
rw [← Finset.prod_mul_distrib]
exact Finset.prod_le_prod (fun _ _ ↦ norm_nonneg _) (fun _ _ ↦ ContinuousLinearMap.le_opNorm _ _)
