Inner product space structure on tensor product spaces

This file provides the inner product space structure on tensor product spaces.

We define the inner product on E ⊗ F by ⟪a ⊗ₜ b, c ⊗ₜ d⟫ = ⟪a, c⟫ * ⟪b, d⟫, when E and F are inner product spaces.

Main definitions:

• TensorProduct.instNormedAddCommGroup: the normed additive group structure on tensor products, where ‖x ⊗ₜ y‖ = ‖x‖ * ‖y‖.
• TensorProduct.instInnerProductSpace: the inner product space structure on tensor products, where ⟪a ⊗ₜ b, c ⊗ₜ d⟫ = ⟪a, c⟫ * ⟪b, d⟫.
• TensorProduct.mapIsometry: the linear isometry version of TensorProduct.map f g when f and g are linear isometries.
• TensorProduct.congrIsometry: the linear isometry equivalence version of TensorProduct.congr f g when f and g are linear isometry equivalences.
• TensorProduct.mapInclIsometry: the linear isometry version of TensorProduct.mapIncl.
• TensorProduct.commIsometry: the linear isometry version of TensorProduct.comm.
• TensorProduct.lidIsometry: the linear isometry version of TensorProduct.lid.
• TensorProduct.assocIsometry: the linear isometry version of TensorProduct.assoc.
• OrthonormalBasis.tensorProduct: the orthonormal basis of the tensor product of two orthonormal bases.

TODO:

• Define the continuous linear map version of TensorProduct.map.
• Complete space of tensor products.
• Define the normed space without needing inner products, this should be analogous to Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean.

instance TensorProduct.instInner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] : Inner 𝕜 (TensorProduct 𝕜 E F)

@[simp]

theorem TensorProduct.inner_tmul (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x x' : E) (y y' : F) : inner 𝕜 (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') = inner 𝕜 x x' * inner 𝕜 y y'

@[simp]

theorem TensorProduct.inner_map_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H) (x y : TensorProduct 𝕜 E F) : inner 𝕜 ((map f.toLinearMap g.toLinearMap) x) ((map f.toLinearMap g.toLinearMap) y) = inner 𝕜 x y

theorem TensorProduct.inner_mapIncl_mapIncl {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (E' : Submodule 𝕜 E) (F' : Submodule 𝕜 F) (x y : TensorProduct 𝕜 ↥E' ↥F') : inner 𝕜 ((mapIncl E' F') x) ((mapIncl E' F') y) = inner 𝕜 x y

noncomputable instance TensorProduct.instNormedAddCommGroup {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] : NormedAddCommGroup (TensorProduct 𝕜 E F)

instance TensorProduct.instInnerProductSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] : InnerProductSpace 𝕜 (TensorProduct 𝕜 E F)

@[simp]

theorem TensorProduct.norm_tmul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : E) (y : F) : ‖x ⊗ₜ[𝕜] y‖ = ‖x‖ * ‖y‖

@[simp]

theorem TensorProduct.nnnorm_tmul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : E) (y : F) : ‖x ⊗ₜ[𝕜] y‖₊ = ‖x‖₊ * ‖y‖₊

@[simp]

theorem TensorProduct.enorm_tmul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : E) (y : F) : ‖x ⊗ₜ[𝕜] y‖ₑ = ‖x‖ₑ * ‖y‖ₑ

theorem TensorProduct.dist_tmul_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x x' : E) (y y' : F) : dist (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖ * ‖y‖ + ‖x'‖ * ‖y'‖

theorem TensorProduct.nndist_tmul_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x x' : E) (y y' : F) : nndist (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖₊ * ‖y‖₊ + ‖x'‖₊ * ‖y'‖₊

theorem TensorProduct.edist_tmul_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x x' : E) (y y' : F) : edist (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖ₑ * ‖y‖ₑ + ‖x'‖ₑ * ‖y'‖ₑ

theorem RCLike.inner_tmul_eq {𝕜 : Type u_1} [RCLike 𝕜] (a b c d : 𝕜) : inner 𝕜 (a ⊗ₜ[𝕜] b) (c ⊗ₜ[𝕜] d) = inner 𝕜 (a * b) (c * d)

In ℝ or ℂ fields, the inner product on tensor products is essentially just the inner product with multiplication instead of tensors, i.e., ⟪a ⊗ₜ b, c ⊗ₜ d⟫ = ⟪a * b, c * d⟫.

theorem TensorProduct.ext_iff_inner_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {x y : TensorProduct 𝕜 E F} : x = y ↔ ∀ (a : E) (b : F), inner 𝕜 x (a ⊗ₜ[𝕜] b) = inner 𝕜 y (a ⊗ₜ[𝕜] b)

Given x, y : E ⊗ F, x = y iff ⟪x, a ⊗ₜ b⟫ = ⟪y, a ⊗ₜ b⟫ for all a, b.

theorem TensorProduct.ext_iff_inner_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {x y : TensorProduct 𝕜 E F} : x = y ↔ ∀ (a : E) (b : F), inner 𝕜 (a ⊗ₜ[𝕜] b) x = inner 𝕜 (a ⊗ₜ[𝕜] b) y

Given x, y : E ⊗ F, x = y iff ⟪a ⊗ₜ b, x⟫ = ⟪a ⊗ₜ b, y⟫ for all a, b.

theorem TensorProduct.ext_iff_inner_right_threefold {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] {x y : TensorProduct 𝕜 (TensorProduct 𝕜 E F) G} : x = y ↔ ∀ (a : E) (b : F) (c : G), inner 𝕜 x (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] c) = inner 𝕜 y (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] c)

Given x, y : E ⊗ F ⊗ G, x = y iff ⟪x, a ⊗ₜ b ⊗ₜ c⟫ = ⟪y, a ⊗ₜ b ⊗ₜ c⟫ for all a, b, c.

See also ext_iff_inner_right_threefold' for when x, y : E ⊗ (F ⊗ G).

theorem TensorProduct.ext_iff_inner_left_threefold {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] {x y : TensorProduct 𝕜 (TensorProduct 𝕜 E F) G} : x = y ↔ ∀ (a : E) (b : F) (c : G), inner 𝕜 (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] c) x = inner 𝕜 (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] c) y

Given x, y : E ⊗ F ⊗ G, x = y iff ⟪a ⊗ₜ b ⊗ₜ c, x⟫ = ⟪a ⊗ₜ b ⊗ₜ c, y⟫ for all a, b, c.

See also ext_iff_inner_left_threefold' for when x, y : E ⊗ (F ⊗ G).

def TensorProduct.mapIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H) : TensorProduct 𝕜 E F →ₗᵢ[𝕜] TensorProduct 𝕜 G H

The tensor product map of two linear isometries is a linear isometry. In particular, this is the linear isometry version of TensorProduct.map f g when f and g are linear isometries.

@[simp]

theorem TensorProduct.mapIsometry_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H) (x : TensorProduct 𝕜 E F) : (mapIsometry f g) x = (map f.toLinearMap g.toLinearMap) x

@[simp]

theorem TensorProduct.toLinearMap_mapIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H) : (mapIsometry f g).toLinearMap = map f.toLinearMap g.toLinearMap

@[simp]

theorem TensorProduct.norm_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H) (x : TensorProduct 𝕜 E F) : ‖(map f.toLinearMap g.toLinearMap) x‖ = ‖x‖

@[simp]

theorem TensorProduct.nnnorm_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H) (x : TensorProduct 𝕜 E F) : ‖(map f.toLinearMap g.toLinearMap) x‖₊ = ‖x‖₊

@[simp]

theorem TensorProduct.enorm_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H) (x : TensorProduct 𝕜 E F) : ‖(map f.toLinearMap g.toLinearMap) x‖ₑ = ‖x‖ₑ

@[simp]

theorem TensorProduct.mapIsometry_id_id {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] : mapIsometry LinearIsometry.id LinearIsometry.id = LinearIsometry.id

def LinearIsometry.lTensor {𝕜 : Type u_1} (E : Type u_2) {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : F →ₗᵢ[𝕜] G) : TensorProduct 𝕜 E F →ₗᵢ[𝕜] TensorProduct 𝕜 E G

This is the natural linear isometry induced by f : F ≃ₗᵢ G.

def LinearIsometry.rTensor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : E →ₗᵢ[𝕜] F) : TensorProduct 𝕜 E G →ₗᵢ[𝕜] TensorProduct 𝕜 F G

This is the natural linear isometry induced by f : E ≃ₗᵢ F.

theorem LinearIsometry.lTensor_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : F →ₗᵢ[𝕜] G) : lTensor E f = TensorProduct.mapIsometry id f

theorem LinearIsometry.rTensor_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : E →ₗᵢ[𝕜] F) : rTensor G f = TensorProduct.mapIsometry f id

@[simp]

theorem LinearIsometry.toLinearMap_lTensor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : F →ₗᵢ[𝕜] G) : (lTensor E f).toLinearMap = LinearMap.lTensor E f.toLinearMap

@[simp]

theorem LinearIsometry.toLinearMap_rTensor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : E →ₗᵢ[𝕜] F) : (rTensor G f).toLinearMap = LinearMap.rTensor G f.toLinearMap

@[simp]

theorem LinearIsometry.lTensor_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : F →ₗᵢ[𝕜] G) (x : TensorProduct 𝕜 E F) : (lTensor E f) x = (LinearMap.lTensor E f.toLinearMap) x

@[simp]

theorem LinearIsometry.rTensor_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : E →ₗᵢ[𝕜] F) (x : TensorProduct 𝕜 E G) : (rTensor G f) x = (LinearMap.rTensor G f.toLinearMap) x

def TensorProduct.congrIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : E ≃ₗᵢ[𝕜] G) (g : F ≃ₗᵢ[𝕜] H) : TensorProduct 𝕜 E F ≃ₗᵢ[𝕜] TensorProduct 𝕜 G H

The tensor product of two linear isometry equivalences is a linear isometry equivalence. In particular, this is the linear isometry equivalence version of TensorProduct.congr f g when f and g are linear isometry equivalences.

@[simp]

theorem TensorProduct.congrIsometry_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : E ≃ₗᵢ[𝕜] G) (g : F ≃ₗᵢ[𝕜] H) (x : TensorProduct 𝕜 E F) : (congrIsometry f g) x = (congr ↑f ↑g) x

theorem TensorProduct.congrIsometry_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : E ≃ₗᵢ[𝕜] G) (g : F ≃ₗᵢ[𝕜] H) : (congrIsometry f g).symm = congrIsometry f.symm g.symm

@[simp]

theorem TensorProduct.toLinearEquiv_congrIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : E ≃ₗᵢ[𝕜] G) (g : F ≃ₗᵢ[𝕜] H) : (congrIsometry f g).toLinearEquiv = congr f.toLinearEquiv g.toLinearEquiv

@[simp]

theorem TensorProduct.congrIsometry_refl_refl {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] : congrIsometry (LinearIsometryEquiv.refl 𝕜 E) (LinearIsometryEquiv.refl 𝕜 F) = LinearIsometryEquiv.refl 𝕜 (TensorProduct 𝕜 E F)

def LinearIsometryEquiv.lTensor {𝕜 : Type u_1} (E : Type u_2) {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : F ≃ₗᵢ[𝕜] G) : TensorProduct 𝕜 E F ≃ₗᵢ[𝕜] TensorProduct 𝕜 E G

This is the natural linear isometric equivalence induced by f : F ≃ₗᵢ G.

def LinearIsometryEquiv.rTensor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : E ≃ₗᵢ[𝕜] F) : TensorProduct 𝕜 E G ≃ₗᵢ[𝕜] TensorProduct 𝕜 F G

This is the natural linear isometric equivalence induced by f : E ≃ₗᵢ F.

theorem LinearIsometryEquiv.lTensor_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : F ≃ₗᵢ[𝕜] G) : lTensor E f = TensorProduct.congrIsometry (refl 𝕜 E) f

theorem LinearIsometryEquiv.rTensor_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : E ≃ₗᵢ[𝕜] F) : rTensor G f = TensorProduct.congrIsometry f (refl 𝕜 G)

theorem LinearIsometryEquiv.symm_lTensor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : F ≃ₗᵢ[𝕜] G) : (lTensor E f).symm = lTensor E f.symm

theorem LinearIsometryEquiv.symm_rTensor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : E ≃ₗᵢ[𝕜] F) : (rTensor G f).symm = rTensor G f.symm

@[simp]

theorem LinearIsometryEquiv.toLinearEquiv_lTensor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : F ≃ₗᵢ[𝕜] G) : (lTensor E f).toLinearEquiv = LinearEquiv.lTensor E f.toLinearEquiv

@[simp]

theorem LinearIsometryEquiv.toLinearIsometry_lTensor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : F ≃ₗᵢ[𝕜] G) : (lTensor E f).toLinearIsometry = LinearIsometry.lTensor E f.toLinearIsometry

@[simp]

theorem LinearIsometryEquiv.toLinearEquiv_rTensor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : E ≃ₗᵢ[𝕜] F) : (rTensor G f).toLinearEquiv = LinearEquiv.rTensor G f.toLinearEquiv

@[simp]

theorem LinearIsometryEquiv.toLinearIsometry_rTensor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : E ≃ₗᵢ[𝕜] F) : (rTensor G f).toLinearIsometry = LinearIsometry.rTensor G f.toLinearIsometry

@[simp]

theorem LinearIsometryEquiv.lTensor_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : F ≃ₗᵢ[𝕜] G) (x : TensorProduct 𝕜 E F) : (lTensor E f) x = (LinearEquiv.lTensor E f.toLinearEquiv) x

@[simp]

theorem LinearIsometryEquiv.rTensor_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (f : E ≃ₗᵢ[𝕜] F) (x : TensorProduct 𝕜 E G) : (rTensor G f) x = (LinearEquiv.rTensor G f.toLinearEquiv) x

def TensorProduct.mapInclIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (E' : Submodule 𝕜 E) (F' : Submodule 𝕜 F) : TensorProduct 𝕜 ↥E' ↥F' →ₗᵢ[𝕜] TensorProduct 𝕜 E F

The linear isometry version of TensorProduct.mapIncl.

@[simp]

theorem TensorProduct.mapInclIsometry_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (E' : Submodule 𝕜 E) (F' : Submodule 𝕜 F) (x : TensorProduct 𝕜 ↥E' ↥F') : (mapInclIsometry E' F') x = (mapIncl E' F') x

@[simp]

theorem TensorProduct.toLinearMap_mapInclIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (E' : Submodule 𝕜 E) (F' : Submodule 𝕜 F) : (mapInclIsometry E' F').toLinearMap = mapIncl E' F'

@[simp]

theorem TensorProduct.inner_comm_comm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x y : TensorProduct 𝕜 E F) : inner 𝕜 ((TensorProduct.comm 𝕜 E F) x) ((TensorProduct.comm 𝕜 E F) y) = inner 𝕜 x y

def TensorProduct.commIsometry (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] : TensorProduct 𝕜 E F ≃ₗᵢ[𝕜] TensorProduct 𝕜 F E

The linear isometry equivalence version of TensorProduct.comm.

@[simp]

theorem TensorProduct.commIsometry_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : TensorProduct 𝕜 E F) : (commIsometry 𝕜 E F) x = (TensorProduct.comm 𝕜 E F) x

@[simp]

theorem TensorProduct.commIsometry_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] : (commIsometry 𝕜 E F).symm = commIsometry 𝕜 F E

@[simp]

theorem TensorProduct.toLinearEquiv_commIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] : (commIsometry 𝕜 E F).toLinearEquiv = TensorProduct.comm 𝕜 E F

@[simp]

theorem TensorProduct.norm_comm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : TensorProduct 𝕜 E F) : ‖(TensorProduct.comm 𝕜 E F) x‖ = ‖x‖

@[simp]

theorem TensorProduct.nnnorm_comm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : TensorProduct 𝕜 E F) : ‖(TensorProduct.comm 𝕜 E F) x‖₊ = ‖x‖₊

@[simp]

theorem TensorProduct.enorm_comm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : TensorProduct 𝕜 E F) : ‖(TensorProduct.comm 𝕜 E F) x‖ₑ = ‖x‖ₑ

@[simp]

theorem TensorProduct.inner_lid_lid {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : TensorProduct 𝕜 𝕜 E) : inner 𝕜 ((TensorProduct.lid 𝕜 E) x) ((TensorProduct.lid 𝕜 E) y) = inner 𝕜 x y

def TensorProduct.lidIsometry (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : TensorProduct 𝕜 𝕜 E ≃ₗᵢ[𝕜] E

The linear isometry equivalence version of TensorProduct.lid.

@[simp]

theorem TensorProduct.lidIsometry_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : TensorProduct 𝕜 𝕜 E) : (lidIsometry 𝕜 E) x = (TensorProduct.lid 𝕜 E) x

@[simp]

theorem TensorProduct.lidIsometry_symm_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : (lidIsometry 𝕜 E).symm x = 1 ⊗ₜ[𝕜] x

@[simp]

theorem TensorProduct.toLinearEquiv_lidIsometry {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : (lidIsometry 𝕜 E).toLinearEquiv = TensorProduct.lid 𝕜 E

@[simp]

theorem TensorProduct.norm_lid {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : TensorProduct 𝕜 𝕜 E) : ‖(TensorProduct.lid 𝕜 E) x‖ = ‖x‖

@[simp]

theorem TensorProduct.nnnorm_lid {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : TensorProduct 𝕜 𝕜 E) : ‖(TensorProduct.lid 𝕜 E) x‖₊ = ‖x‖₊

@[simp]

theorem TensorProduct.enorm_lid {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : TensorProduct 𝕜 𝕜 E) : ‖(TensorProduct.lid 𝕜 E) x‖ₑ = ‖x‖ₑ

@[simp]

theorem TensorProduct.inner_assoc_assoc {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (x y : TensorProduct 𝕜 (TensorProduct 𝕜 E F) G) : inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) x) ((TensorProduct.assoc 𝕜 E F G) y) = inner 𝕜 x y

def TensorProduct.assocIsometry (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) (G : Type u_4) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] : TensorProduct 𝕜 (TensorProduct 𝕜 E F) G ≃ₗᵢ[𝕜] TensorProduct 𝕜 E (TensorProduct 𝕜 F G)

The linear isometry equivalence version of TensorProduct.assoc.

@[simp]

theorem TensorProduct.assocIsometry_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (x : TensorProduct 𝕜 (TensorProduct 𝕜 E F) G) : (assocIsometry 𝕜 E F G) x = (TensorProduct.assoc 𝕜 E F G) x

@[simp]

theorem TensorProduct.assocIsometry_symm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (x : TensorProduct 𝕜 E (TensorProduct 𝕜 F G)) : (assocIsometry 𝕜 E F G).symm x = (TensorProduct.assoc 𝕜 E F G).symm x

@[simp]

theorem TensorProduct.toLinearEquiv_assocIsometry {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] : (assocIsometry 𝕜 E F G).toLinearEquiv = TensorProduct.assoc 𝕜 E F G

@[simp]

theorem TensorProduct.norm_assoc {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (x : TensorProduct 𝕜 (TensorProduct 𝕜 E F) G) : ‖(TensorProduct.assoc 𝕜 E F G) x‖ = ‖x‖

@[simp]

theorem TensorProduct.nnnorm_assoc {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (x : TensorProduct 𝕜 (TensorProduct 𝕜 E F) G) : ‖(TensorProduct.assoc 𝕜 E F G) x‖₊ = ‖x‖₊

@[simp]

theorem TensorProduct.enorm_assoc {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (x : TensorProduct 𝕜 (TensorProduct 𝕜 E F) G) : ‖(TensorProduct.assoc 𝕜 E F G) x‖ₑ = ‖x‖ₑ

@[simp]

theorem TensorProduct.adjoint_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] [FiniteDimensional 𝕜 H] (f : E →ₗ[𝕜] F) (g : G →ₗ[𝕜] H) : LinearMap.adjoint (map f g) = map (LinearMap.adjoint f) (LinearMap.adjoint g)

@[simp]

theorem LinearMap.adjoint_rTensor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] (f : E →ₗ[𝕜] F) : adjoint (rTensor G f) = rTensor G (adjoint f)

@[simp]

theorem LinearMap.adjoint_lTensor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] (f : E →ₗ[𝕜] F) : adjoint (lTensor G f) = lTensor G (adjoint f)

theorem TensorProduct.ext_iff_inner_right_threefold' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] {x y : TensorProduct 𝕜 E (TensorProduct 𝕜 F G)} : x = y ↔ ∀ (a : E) (b : F) (c : G), inner 𝕜 x (a ⊗ₜ[𝕜] (b ⊗ₜ[𝕜] c)) = inner 𝕜 y (a ⊗ₜ[𝕜] (b ⊗ₜ[𝕜] c))

Given x, y : E ⊗ (F ⊗ G), x = y iff ⟪x, a ⊗ₜ (b ⊗ₜ c)⟫ = ⟪y, a ⊗ₜ (b ⊗ₜ c)⟫ for all a, b, c.

See also ext_iff_inner_right_threefold for when x, y : E ⊗ F ⊗ G.

theorem TensorProduct.ext_iff_inner_left_threefold' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] {x y : TensorProduct 𝕜 E (TensorProduct 𝕜 F G)} : x = y ↔ ∀ (a : E) (b : F) (c : G), inner 𝕜 (a ⊗ₜ[𝕜] (b ⊗ₜ[𝕜] c)) x = inner 𝕜 (a ⊗ₜ[𝕜] (b ⊗ₜ[𝕜] c)) y

Given x, y : E ⊗ (F ⊗ G), x = y iff ⟪a ⊗ₜ (b ⊗ₜ c), x⟫ = ⟪a ⊗ₜ (b ⊗ₜ c), y⟫ for all a, b, c.

See also ext_iff_inner_left_threefold for when x, y : E ⊗ F ⊗ G.

theorem Orthonormal.tmul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι₁ : Type u_6} {ι₂ : Type u_7} {b₁ : ι₁ → E} {b₂ : ι₂ → F} (hb₁ : Orthonormal 𝕜 b₁) (hb₂ : Orthonormal 𝕜 b₂) : Orthonormal 𝕜 fun (i : ι₁ × ι₂) => b₁ i.1 ⊗ₜ[𝕜] b₂ i.2

The tensor product of two orthonormal vectors is orthonormal.

theorem Orthonormal.basisTensorProduct {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι₁ : Type u_6} {ι₂ : Type u_7} {b₁ : Module.Basis ι₁ 𝕜 E} {b₂ : Module.Basis ι₂ 𝕜 F} (hb₁ : Orthonormal 𝕜 ⇑b₁) (hb₂ : Orthonormal 𝕜 ⇑b₂) : Orthonormal 𝕜 ⇑(b₁.tensorProduct b₂)

The tensor product of two orthonormal bases is orthonormal.

noncomputable def OrthonormalBasis.tensorProduct {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι₁ : Type u_6} {ι₂ : Type u_7} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) : OrthonormalBasis (ι₁ × ι₂) 𝕜 (TensorProduct 𝕜 E F)

The orthonormal basis of the tensor product of two orthonormal bases.

@[simp]

theorem OrthonormalBasis.tensorProduct_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι₁ : Type u_6} {ι₂ : Type u_7} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) (i : ι₁) (j : ι₂) : (b₁.tensorProduct b₂) (i, j) = b₁ i ⊗ₜ[𝕜] b₂ j

theorem OrthonormalBasis.tensorProduct_apply' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι₁ : Type u_6} {ι₂ : Type u_7} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) (i : ι₁ × ι₂) : (b₁.tensorProduct b₂) i = b₁ i.1 ⊗ₜ[𝕜] b₂ i.2

@[simp]

theorem OrthonormalBasis.tensorProduct_repr_tmul_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι₁ : Type u_6} {ι₂ : Type u_7} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) (x : E) (y : F) (i : ι₁) (j : ι₂) : ((b₁.tensorProduct b₂).repr (x ⊗ₜ[𝕜] y)).ofLp (i, j) = (b₂.repr y).ofLp j * (b₁.repr x).ofLp i

theorem OrthonormalBasis.tensorProduct_repr_tmul_apply' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι₁ : Type u_6} {ι₂ : Type u_7} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) (x : E) (y : F) (i : ι₁ × ι₂) : ((b₁.tensorProduct b₂).repr (x ⊗ₜ[𝕜] y)).ofLp i = (b₂.repr y).ofLp i.2 * (b₁.repr x).ofLp i.1

@[simp]

theorem OrthonormalBasis.toBasis_tensorProduct {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι₁ : Type u_6} {ι₂ : Type u_7} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) : (b₁.tensorProduct b₂).toBasis = b₁.toBasis.tensorProduct b₂.toBasis