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ⱼ ∈ Π 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 p = (List.map (fun (p : 𝕜 × ((i : ι) → E i)) => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) (FreeAddMonoid.toList p)).sum

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

theorem PiTensorProduct.projectiveSeminormAux_add_le {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] (p q : FreeAddMonoid (𝕜 × ((i : ι) → E i))) : projectiveSeminormAux (p + q) ≤ projectiveSeminormAux p + 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 : 𝕜) : projectiveSeminormAux ((FreeAddMonoid.map fun (y : 𝕜 × ((i : ι) → E i)) => (a * y.1, y.2)) p) = ‖a‖ * 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) => 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ⱼ ∈ Π 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) : projectiveSeminorm x = ⨅ (p : ↑x.lifts), 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) : projectiveSeminorm (⨂ₜ[𝕜] (i : ι), m i) ≤ ∏ 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) : ‖(lift f.toMultilinearMap) x‖ ≤ projectiveSeminorm x * ‖f‖