English
For any x and any continuous multilinear f, we have that the norm of lift f at x is bounded by projectiveSeminorm x times the operator norm of f.
Русский
Для всякого x и непрерывного мультилейного отображения f имеет место неравенство: ||lift f (x)|| ≤ projectiveSeminorm x · ||f||.
LaTeX
$$$ \\|\\mathrm{lift} f^{\\mathrm{toMultilinearMap}}(x)\\| \\leq \\mathrm{projectiveSeminorm}(x) \\cdot \\|f\\| $$$
Lean4
theorem norm_eval_le_projectiveSeminorm (x : ⨂[𝕜] i, E i) (G : Type*) [SeminormedAddCommGroup G] [NormedSpace 𝕜 G]
(f : ContinuousMultilinearMap 𝕜 E G) : ‖lift f.toMultilinearMap x‖ ≤ projectiveSeminorm x * ‖f‖ :=
by
letI := nonempty_subtype.mpr (nonempty_lifts x)
rw [projectiveSeminorm_apply, Real.iInf_mul_of_nonneg (norm_nonneg _)]
unfold projectiveSeminormAux
refine le_ciInf ?_
intro ⟨p, hp⟩
rw [mem_lifts_iff] at hp
conv_lhs => rw [← hp, ← List.sum_map_hom, ← Multiset.sum_coe]
refine le_trans (norm_multiset_sum_le _) ?_
simp only [Multiset.map_coe, List.map_map, Multiset.sum_coe]
rw [mul_comm, ← smul_eq_mul, List.smul_sum]
refine List.Forall₂.sum_le_sum ?_
simp only [smul_eq_mul, List.map_map, List.forall₂_map_right_iff, Function.comp_apply, List.forall₂_map_left_iff,
map_smul, lift.tprod, ContinuousMultilinearMap.coe_coe, List.forall₂_same, Prod.forall]
intro a m _
rw [norm_smul, ← mul_assoc, mul_comm ‖f‖ _, mul_assoc]
exact mul_le_mul_of_nonneg_left (f.le_opNorm _) (norm_nonneg _)
