Tensor products of inner product spaces

Mathlib's ContinuousLinearMap.norm_rTensor_le and ContinuousLinearMap.norm_lTensor_le bound the norm of f ⊗ id and id ⊗ f by the norm of f. Together with additivity in f this says that f ↦ f.rTensor H and f ↦ f.lTensor H are contractions, hence continuous in f, which is the form in which the bound is used to make an operator-valued map into a tensor product continuous.

Mathlib's inner product on E ⊗[𝕜] F also says that the tensor product of two positive definite Hermitian forms is positive definite. TauCeti.apply_self_pos_of_apply_tmul_tmul states this for sesquilinear forms on vector spaces carrying no inner product space structure of their own, such as the Hodge forms of polarized Hodge structures: a sesquilinear form on W₁ ⊗[𝕜] W₂ whose value on pure tensors is the product of the values of two positive definite Hermitian forms is positive definite.

Main statements

• TauCeti.lipschitzWith_one_rTensor and TauCeti.lipschitzWith_one_lTensor: tensoring with the identity, on either side, is 1-Lipschitz in the operator.
• TauCeti.apply_self_pos_of_apply_tmul_tmul: the tensor product of two positive definite Hermitian forms is positive definite.

theorem TauCeti.lipschitzWith_one_rTensor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {H : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] : LipschitzWith 1 fun (f : E →L[𝕜] F) => ContinuousLinearMap.rTensor H f

Tensoring a continuous linear map with the identity on the right is a contraction, hence continuous in the map. This is the elementary continuity statement that Mathlib's ContinuousLinearMap.norm_rTensor_le and additivity give together.

theorem TauCeti.lipschitzWith_one_lTensor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {H : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] : LipschitzWith 1 fun (f : E →L[𝕜] F) => ContinuousLinearMap.lTensor H f

Tensoring a continuous linear map with the identity on the left is a contraction, hence continuous in the map.

theorem TauCeti.apply_self_pos_of_apply_tmul_tmul {𝕜 : Type u_1} [RCLike 𝕜] {W₁ : Type u_5} {W₂ : Type u_6} [AddCommGroup W₁] [Module 𝕜 W₁] [AddCommGroup W₂] [Module 𝕜 W₂] {h₁ : W₁ →ₗ⋆[𝕜] W₁ →ₗ[𝕜] 𝕜} {h₂ : W₂ →ₗ⋆[𝕜] W₂ →ₗ[𝕜] 𝕜} {H : TensorProduct 𝕜 W₁ W₂ →ₗ⋆[𝕜] TensorProduct 𝕜 W₁ W₂ →ₗ[𝕜] 𝕜} (hH : ∀ (a : W₁) (b : W₂) (c : W₁) (d : W₂), (H (a ⊗ₜ[𝕜] b)) (c ⊗ₜ[𝕜] d) = (h₁ a) c * (h₂ b) d) (hh₁ : h₁.IsSymm) (hh₂ : h₂.IsSymm) (hpos₁ : ∀ (x : W₁), x ≠ 0 → 0 < (h₁ x) x) (hpos₂ : ∀ (x : W₂), x ≠ 0 → 0 < (h₂ x) x) {x : TensorProduct 𝕜 W₁ W₂} (hx : x ≠ 0) : 0 < (H x) x

The tensor product of two positive definite Hermitian forms is positive definite. A sesquilinear form H on W₁ ⊗[𝕜] W₂ with H (a ⊗ b) (c ⊗ d) = h₁ a c * h₂ b d, for positive definite Hermitian forms h₁ and h₂, is positive on every nonzero vector.