feat(Analysis/NormedSpace/PiTensorProduct/{InjectiveNorm, ProjectiveN…

…orm}, LinearAlgebra/PiTensorProduct): define the injective and projective norms on `PiTensorProduct` and prove the universal property of the first one (#11534)

Define the injective and projective cross norms on a `PiTensorProduct` of normed vector spaces `Eᵢ` over a nontrivially normed field `𝕜` (cf https://en.wikipedia.org/wiki/Topological_tensor_product#Cross_norms_and_tensor_products_of_Banach_spaces).

The projective norm, defined in `Analysis/NormedSpace/PiTensorProduct/ProjectiveNorm.lean`, is the biggest norm on the `PiTensorProduct` satisfying  `‖⨂ₜ[𝕜] i, m i‖ ≤ Π i, ‖m i‖` for every `m` in `Π i, Eᵢ`. We are mainly interested in the injective norm in this PR, so we just give the definition of the projective norm and its basic properties. To help with the proofs, we introduce some lemmas in `LinearAlgebra/PiTensorProduct.lean` about the set of lifts in `FreeAddMonoid (R × Π i, s i)` of an element `x` of `⨂[R] i, s i`.

The injective norm, defined in `Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean`, is chosen to satisfy the following property: for every normed `𝕜`-vector space `F`, the linear equivalence `MultilinearMap 𝕜 E F ≃ₗ[𝕜] (⨂[𝕜] i, Eᵢ) →ₗ[𝕜] F` expressing the universal property of the tensor product induces an isometric linear equivalence `ContinuousMultilinearMap 𝕜 E F ≃ₗᵢ[𝕜] (⨂[𝕜] i, Eᵢ) →L[𝕜] F`.

The idea is the following: Every normed `𝕜`-vector space `F` defines a linear map from `⨂[𝕜] i, Eᵢ` to `ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] F`, which sends `x` to the map `f ↦ f.lift x`. Thanks to `PiTensorProduct.projectiveSeminorm_bound`, this map lands in `ContinuousMultilinearMap 𝕜 E F →L[𝕜] F`. As this last space has a natural operator seminorm, we get an induced seminorm on `⨂[𝕜] i, Eᵢ`, which, by `PiTensorProduct.projectiveSeminorm_bound`, is bounded above by the projective seminorm. We then take the `sup` of these seminorms as `F` varies; as this family of seminorms is bounded, its `sup` has good properties.

In fact, we cannot take the `sup` over all normed spaces `F` because of set-theoretical issues, so we only take spaces `F` in the same universe as `⨂[𝕜] i, Eᵢ`. We then prove in `PiTensorProduct.norm_eval_le_injectiveSeminorm` that this gives the same result, because every multilinear map from `E` to `F` factors though a normed vector space in the same universe as `⨂[𝕜] i, Eᵢ`.

# Main definitions

* `PiTensorProduct.projectiveSeminorm`: The projective seminorm on `⨂[𝕜] i, Eᵢ`.
* `PiTensorProduct.toDualContinuousMultilinearMap`: The `𝕜`-linear map from `⨂[𝕜] i, Eᵢ` to `ContinuousMultilinearMap 𝕜 E F →L[𝕜] F` sending `x` to the map `f ↦ f x`.
* `PiTensorProduct.injectiveSeminorm`: The injective seminorm on `⨂[𝕜] i, Eᵢ`.
* `PiTensorProduct.liftEquiv`: The bijection between `ContinuousMultilinearMap 𝕜 E F`
and `(⨂[𝕜] i, Eᵢ) →L[𝕜] F`, as a continuous linear equivalence.
* `PiTensorProduct.liftIsometry`: The bijection between `ContinuousMultilinearMap 𝕜 E F`
and `(⨂[𝕜] i, Eᵢ) →L[𝕜] F`, as an isometric linear equivalence.
* `PiTensorProduct.tprodL`: The cacnonical continuous multilinear map from `E`
to `⨂[𝕜] i, Eᵢ`.
* `PiTensorProduct.mapL`: The continuous linear map from `⨂[𝕜] i, Eᵢ` to `⨂[𝕜] i, E'ᵢ`
induced by a family of continuous linear maps `Eᵢ →L[𝕜] E'ᵢ`.
* `PiTensorProduct.mapLMultilinear`: The continuous multilinear map from
`fun i ↦ (Eᵢ →L[𝕜] E'ᵢ)` to `(⨂[𝕜] i, Eᵢ) →L[𝕜] (⨂[𝕜] i, E'ᵢ)` sending a family
`f` to `PiTensorProduct.mapL f`.

# Main results

* `PiTensorProduct.norm_eval_le_projectiveSeminorm`: For every `x` in `⨂[𝕜] i, Eᵢ` and every continuous multilinear map `f` from `E` to a normed space `F`, we have `‖f.lift  x‖ ≤ ‖f‖ * projectiveSeminorm x `. This implies in particular:
* `PiTensorProduct.injectiveSeminorm_le_projectiveSeminorm`: The injective seminorm is bounded above by the projective seminorm.
* `PiTensorProduct.norm_eval_le_injectiveSeminorm`: The main property of the injective seminorm on
`⨂[𝕜] i, Eᵢ`: for every `x` in `⨂[𝕜] i, Eᵢ` and every continuous multilinear map `f` from `E`
to a normed space `F`, we have `‖f.lift  x‖ ≤ ‖f‖ * injectiveSeminorm x `.
* `PiTensorProduct.mapL_opNorm`: If `f` is a family of continuous linear maps
`fᵢ : Eᵢ →L[𝕜] Fᵢ`, then `‖PiTensorProduct.mapL f‖ ≤ ∏ i, ‖fᵢ‖`.
* `PiTensorProduct.mapLMultilinear_opNorm` : If `F` is a normed vecteor space, then
`‖mapLMultilinear 𝕜 E F‖ ≤ 1`.

# TODO (in a future PR)

If all `Eᵢ` are separated and satisfy `SeparatingDual`, then the seminorm on `⨂[𝕜] i, Eᵢ` is a norm. This uses the construction of a basis of the `PiTensorProduct`, hence depends on PR #11156. It should probably go in a separate file, which is why I am creating a directory Analysis/NormedSpace/PiTensorProduct.

# Technical issues

* Ideally, I would prefer not to define `liftEquiv` and to have only `liftIsometry`, but I am using `liftEquiv.left_inv` in the proof that `liftIsometry` preserves norms.



Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>

Mathlib.lean

@@ -904,6 +904,8 @@ import Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm
 import Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Prod
 import Mathlib.Analysis.NormedSpace.PiLp
+import Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm
+import Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm
 import Mathlib.Analysis.NormedSpace.Pointwise
 import Mathlib.Analysis.NormedSpace.ProdLp
 import Mathlib.Analysis.NormedSpace.QuaternionExponential