Projective seminorm on the tensor of a finite family of normed spaces.

Let 𝕜 be a nontrivially normed field and E be a family of normed 𝕜-vector spaces Eᵢ, indexed by a finite type ι. We define a seminorm on ⨂[𝕜] i, Eᵢ, which we call the "projective seminorm". For x an element of ⨂[𝕜] i, Eᵢ, its projective seminorm is the infimum over all expressions of x as ∑ j, ⨂ₜ[𝕜] mⱼ i (with the mⱼ in Π i, Eᵢ) of ∑ j, Π i, ‖mⱼ i‖.

In particular, every norm ‖.‖ on ⨂[𝕜] i, Eᵢ satisfying ‖⨂ₜ[𝕜] i, m i‖ ≤ Π i, ‖m i‖ for every m in Π i, Eᵢ is bounded above by the projective seminorm.

Main definitions

• PiTensorProduct.projectiveSeminorm: The projective seminorm on ⨂[𝕜] i, Eᵢ.

Main results

• PiTensorProduct.norm_eval_le_projectiveSeminorm: If f is a continuous multilinear map on E = Π i, Eᵢ and x is in ⨂[𝕜] i, Eᵢ, then ‖f.lift x‖ ≤ projectiveSeminorm x * ‖f‖.

TODO

• If the base field is ℝ or ℂ (or more generally if the injection of Eᵢ into its bidual is an isometry for every i), then we have projectiveSeminorm ⨂ₜ[𝕜] i, mᵢ = Π i, ‖mᵢ‖.

• The functoriality.

def PiTensorProduct.projectiveSeminormAux {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] : FreeAddMonoid (𝕜 × ((i : ι) → E i)) → ℝ

A lift of the projective seminorm to FreeAddMonoid (𝕜 × Π i, Eᵢ), useful to prove the properties of projectiveSeminorm.

Equations

• PiTensorProduct.projectiveSeminormAux = List.sum ∘ List.map fun (p : 𝕜 × ((i : ι) → E i)) => ‖p.1‖ * Finset.univ.prod fun (i : ι) => ‖p.2 i‖

theorem PiTensorProduct.projectiveSeminormAux_nonneg {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] (p : FreeAddMonoid (𝕜 × ((i : ι) → E i))) : 0 ≤ PiTensorProduct.projectiveSeminormAux p

theorem PiTensorProduct.projectiveSeminormAux_add_le {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] (p : FreeAddMonoid (𝕜 × ((i : ι) → E i))) (q : FreeAddMonoid (𝕜 × ((i : ι) → E i))) : PiTensorProduct.projectiveSeminormAux (p + q) ≤ PiTensorProduct.projectiveSeminormAux p + PiTensorProduct.projectiveSeminormAux q

theorem PiTensorProduct.projectiveSeminormAux_smul {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] (p : FreeAddMonoid (𝕜 × ((i : ι) → E i))) (a : 𝕜) : PiTensorProduct.projectiveSeminormAux (List.map (fun (y : 𝕜 × ((i : ι) → E i)) => (a * y.1, y.2)) p) = ‖a‖ * PiTensorProduct.projectiveSeminormAux p

theorem PiTensorProduct.bddBelow_projectiveSemiNormAux {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (x : PiTensorProduct 𝕜 fun (i : ι) => E i) : BddBelow (Set.range fun (p : ↑x.lifts) => PiTensorProduct.projectiveSeminormAux ↑p)

noncomputable def PiTensorProduct.projectiveSeminorm {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] : Seminorm 𝕜 (PiTensorProduct 𝕜 fun (i : ι) => E i)

The projective seminorm on ⨂[𝕜] i, Eᵢ. It sends an element x of ⨂[𝕜] i, Eᵢ to the infimum over all expressions of x as ∑ j, ⨂ₜ[𝕜] mⱼ i (with the mⱼ in Π i, Eᵢ) of ∑ j, Π i, ‖mⱼ i‖.

Equations

• PiTensorProduct.projectiveSeminorm = Seminorm.ofSMulLE (fun (x : PiTensorProduct 𝕜 fun (i : ι) => E i) => ⨅ (p : ↑x.lifts), PiTensorProduct.projectiveSeminormAux ↑p) ⋯ ⋯ ⋯

theorem PiTensorProduct.projectiveSeminorm_apply {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (x : PiTensorProduct 𝕜 fun (i : ι) => E i) : PiTensorProduct.projectiveSeminorm x = ⨅ (p : ↑x.lifts), PiTensorProduct.projectiveSeminormAux ↑p

theorem PiTensorProduct.projectiveSeminorm_tprod_le {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (m : (i : ι) → E i) : PiTensorProduct.projectiveSeminorm (⨂ₜ[𝕜] (i : ι), m i) ≤ Finset.univ.prod fun (i : ι) => ‖m i‖

theorem PiTensorProduct.norm_eval_le_projectiveSeminorm {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (x : PiTensorProduct 𝕜 fun (i : ι) => E i) (G : Type u_1) [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) : ‖(PiTensorProduct.lift f.toMultilinearMap) x‖ ≤ PiTensorProduct.projectiveSeminorm x * ‖f‖