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

The purpose of this file is to develop the theory of the injective tensor norm.

A first formalization turned out not to capture the common mathematical definition and is now deprecated. See

https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/injectiveSeminorm/with/568798633

Main definitions

• PiTensorProduct.toDualContinuousMultilinearMap: The 𝕜-linear map from ⨂[𝕜] i, Eᵢ to ContinuousMultilinearMap 𝕜 E F →L[𝕜] F sending x to the map f ↦ f x.

TODO

• Reimplement injectiveSeminorm.

noncomputable def PiTensorProduct.toDualContinuousMultilinearMap {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (F : Type u_1) [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : (PiTensorProduct 𝕜 fun (i : ι) => E i) →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] F

The linear map from ⨂[𝕜] i, Eᵢ to ContinuousMultilinearMap 𝕜 E F →L[𝕜] F sending x in ⨂[𝕜] i, Eᵢ to the map f ↦ f.lift x.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PiTensorProduct.toDualContinuousMultilinearMap_apply_apply {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (F : Type u_1) [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (x : PiTensorProduct 𝕜 fun (i : ι) => E i) (x✝ : ContinuousMultilinearMap 𝕜 E F) : ((toDualContinuousMultilinearMap F) x) x✝ = (lift x✝.toMultilinearMap) x

theorem PiTensorProduct.toDualContinuousMultilinearMap_le_projectiveSeminorm {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] {F : Type u_1} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (x : PiTensorProduct 𝕜 fun (i : ι) => E i) : ‖(toDualContinuousMultilinearMap F) x‖ ≤ projectiveSeminorm x

theorem PiTensorProduct.injectiveSeminorm_def {ι : Type u_2} [Fintype ι] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] {E : ι → Type u_4} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] : injectiveSeminorm = sSup {p : Seminorm 𝕜 (PiTensorProduct 𝕜 fun (i : ι) => E i) | ∃ (G : Type (max u_2 u_3 u_4)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G), p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)}

@[irreducible, deprecated "`injectiveSeminorm` is deprecated in favor of the extensionally equal `projectiveSeminorm`" (since := "2026-06-10")]

noncomputable def PiTensorProduct.injectiveSeminorm {ι : Type u_2} [Fintype ι] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] {E : ι → Type u_4} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] : Seminorm 𝕜 (PiTensorProduct 𝕜 fun (i : ι) => E i)

The injective seminorm on ⨂[𝕜] i, Eᵢ. Morally, it sends x in ⨂[𝕜] i, Eᵢ to the sup of the operator norms of the PiTensorProduct.toDualContinuousMultilinearMap F x, for all normed vector spaces F. In fact, we only take in the same universe as ⨂[𝕜] i, Eᵢ, and then prove in PiTensorProduct.norm_eval_le_injectiveSeminorm that this gives the same result.

Equations

• One or more equations did not get rendered due to their size.

@[deprecated "no replacement" (since := "2026-06-10")]

theorem PiTensorProduct.dualSeminorms_bounded {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] : BddAbove {p : Seminorm 𝕜 (PiTensorProduct 𝕜 fun (i : ι) => E i) | ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G), p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)}

@[deprecated "`injectiveSeminorm` is deprecated in favor of the extensionally equal `projectiveSeminorm`" (since := "2026-06-10")]

theorem PiTensorProduct.injectiveSeminorm_apply {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (x : PiTensorProduct 𝕜 fun (i : ι) => E i) : injectiveSeminorm x = ⨆ (p : ↑{p : Seminorm 𝕜 (PiTensorProduct 𝕜 fun (i : ι) => E i) | ∃ (G : Type (max uι u𝕜 uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G), p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)}), ↑p x

@[deprecated "`injectiveSeminorm` is deprecated in favor of the extensionally equal `projectiveSeminorm`" (since := "2026-06-10")]

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

@[deprecated "`injectiveSeminorm` is deprecated in favor of the extensionally equal `projectiveSeminorm`" (since := "2026-06-10")]

theorem PiTensorProduct.injectiveSeminorm_le_projectiveSeminorm {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] : injectiveSeminorm ≤ projectiveSeminorm

@[deprecated "`injectiveSeminorm` is deprecated in favor of the extensionally equal `projectiveSeminorm`" (since := "2026-06-10")]

theorem PiTensorProduct.injectiveSeminorm_tprod_le {ι : Type uι} [Fintype ι] {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] (m : (i : ι) → E i) : injectiveSeminorm (⨂ₜ[𝕜] (i : ι), m i) ≤ ∏ i : ι, ‖m i‖