English
The injective seminorm is bounded above by the projective seminorm on the same tensor product.
Русский
Инъективная полунормированность ограничена сверху проективной полунормой на том же тензорном произведении.
LaTeX
$$injectiveSeminorm ≤ projectiveSeminorm$$
Lean4
theorem norm_eval_le_injectiveSeminorm (f : ContinuousMultilinearMap 𝕜 E F) (x : ⨂[𝕜] i, E i) :
‖lift f.toMultilinearMap x‖ ≤ ‖f‖ * injectiveSeminorm x := by
/- If `F` were in `Type (max uι u𝕜 uE)` (which is the type of `⨂[𝕜] i, E i`), then the
property that we want to prove would hold by definition of `injectiveSeminorm`. This is
not necessarily true, but we will show that there exists a normed vector space `G` in
`Type (max uι u𝕜 uE)` and an injective isometry from `G` to `F` such that `f` factors
through a continuous multilinear map `f'` from `E = Π i, E i` to `G`, to which we can apply
the definition of `injectiveSeminorm`. The desired inequality for `f` then follows
immediately.
The idea is very simple: the multilinear map `f` corresponds by `PiTensorProduct.lift`
to a linear map from `⨂[𝕜] i, E i` to `F`, say `l`. We want to take `G` to be the image of
`l`, with the norm induced from that of `F`; to make sure that we are in the correct universe,
it is actually more convenient to take `G` equal to the coimage of `l` (i.e. the quotient
of `⨂[𝕜] i, E i` by the kernel of `l`), which is canonically isomorphic to its image by
`LinearMap.quotKerEquivRange`. -/
set G := (⨂[𝕜] i, E i) ⧸ LinearMap.ker (lift f.toMultilinearMap)
set G' := LinearMap.range (lift f.toMultilinearMap)
set e := LinearMap.quotKerEquivRange (lift f.toMultilinearMap)
letI := SeminormedAddCommGroup.induced G G' e
letI := NormedSpace.induced 𝕜 G G' e
set f'₀ := lift.symm (e.symm.toLinearMap ∘ₗ LinearMap.rangeRestrict (lift f.toMultilinearMap))
have hf'₀ : ∀ (x : Π (i : ι), E i), ‖f'₀ x‖ ≤ ‖f‖ * ∏ i, ‖x i‖ := fun x ↦
by
change ‖e (f'₀ x)‖ ≤ _
simp only [lift_symm, LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, LinearEquiv.coe_coe,
Function.comp_apply, LinearEquiv.apply_symm_apply, Submodule.coe_norm, LinearMap.codRestrict_apply, lift.tprod,
ContinuousMultilinearMap.coe_coe, e, f'₀]
exact f.le_opNorm x
set f' := MultilinearMap.mkContinuous f'₀ ‖f‖ hf'₀
have hnorm : ‖f'‖ ≤ ‖f‖ := (f'.opNorm_le_iff (norm_nonneg f)).mpr hf'₀
have heq : e (lift f'.toMultilinearMap x) = lift f.toMultilinearMap x := by
induction x using PiTensorProduct.induction_on with
| smul_tprod =>
simp only [lift_symm, map_smul, lift.tprod, ContinuousMultilinearMap.coe_coe, MultilinearMap.coe_mkContinuous,
LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
LinearEquiv.apply_symm_apply, SetLike.val_smul, LinearMap.codRestrict_apply, f', f'₀]
| add _ _ hx hy => simp only [map_add, Submodule.coe_add, hx, hy]
suffices h : ‖lift f'.toMultilinearMap x‖ ≤ ‖f'‖ * injectiveSeminorm x
by
change ‖(e (lift f'.toMultilinearMap x)).1‖ ≤ _ at h
rw [heq] at h
exact le_trans h (mul_le_mul_of_nonneg_right hnorm (apply_nonneg _ _))
have hle :
Seminorm.comp (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
(toDualContinuousMultilinearMap G (𝕜 := 𝕜) (E := E)) ≤
injectiveSeminorm :=
by
simp only [injectiveSeminorm]
refine le_csSup dualSeminorms_bounded ?_
rw [Set.mem_setOf]
existsi G, inferInstance, inferInstance
rfl
refine le_trans ?_ (mul_le_mul_of_nonneg_left (hle x) (norm_nonneg f'))
simp only [Seminorm.comp_apply, coe_normSeminorm, ← toDualContinuousMultilinearMap_apply_apply]
rw [mul_comm]
exact ContinuousLinearMap.le_opNorm _ _
