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

Let 𝕜 be a 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𝕜} {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] : 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𝕜} {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] (p : FreeAddMonoid (𝕜 × ((i : ι) → E i))) : 0 ≤ projectiveSeminormAux p

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

theorem PiTensorProduct.projectiveSeminormAux_smul {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] (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𝕜} {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (x : PiTensorProduct 𝕜 fun (i : ι) => E i) : BddBelow (Set.range fun (p : ↑x.lifts) => projectiveSeminormAux ↑p)

@[implicit_reducible]

noncomputable instance PiTensorProduct.instNorm {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] : Norm (PiTensorProduct 𝕜 fun (i : ι) => E i)

Equations

• PiTensorProduct.instNorm = { norm := fun (x : PiTensorProduct 𝕜 fun (i : ι) => E i) => ⨅ (p : ↑x.lifts), PiTensorProduct.projectiveSeminormAux ↑p }

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

@[deprecated Norm.norm (since := "2026-03-13")]

def PiTensorProduct.projectiveSeminormFun {E : Type u_8} [self : Norm E] : E → ℝ

Alias of Norm.norm.

Equations

• @PiTensorProduct.projectiveSeminormFun = @norm

theorem PiTensorProduct.projectiveSeminorm_zero {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] : ‖0‖ = 0

theorem PiTensorProduct.projectiveSeminorm_add_le {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (x y : PiTensorProduct 𝕜 fun (i : ι) => E i) : ‖x + y‖ ≤ ‖x‖ + ‖y‖

theorem PiTensorProduct.projectiveSeminorm_smul_le {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (a : 𝕜) (x : PiTensorProduct 𝕜 fun (i : ι) => E i) : ‖a • x‖ ≤ ‖a‖ * ‖x‖

noncomputable def PiTensorProduct.projectiveSeminorm {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(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 norm ⋯ ⋯ ⋯

@[deprecated PiTensorProduct.norm_def (since := "2026-03-06")]

theorem PiTensorProduct.projectiveSeminorm_apply {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(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𝕜} {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(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𝕜} {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] {G : Type u_1} [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) (x : PiTensorProduct 𝕜 fun (i : ι) => E i) : ‖(lift f.toMultilinearMap) x‖ ≤ ‖f‖ * ‖x‖