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.

source

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)

Equations

TensorProduct.instInner = { inner := fun (x y : TensorProduct 𝕜 E F) => (TensorProduct.inner_✝ x) y }

source

@[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'

source

@[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

source

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

source

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)

Equations

TensorProduct.instNormedAddCommGroup = InnerProductSpace.Core.toNormedAddCommGroup

source

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)

Equations

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

source

@[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‖

source

@[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‖₊

source

@[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‖ₑ

source

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'‖

source

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'‖₊

source

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'‖ₑ

source

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⟫.

source

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.

source

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.

source

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).

source

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).

source

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.

Equations

TensorProduct.mapIsometry f g = (TensorProduct.map f.toLinearMap g.toLinearMap).isometryOfInner ⋯

Instances For

source

@[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

source

@[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

source

@[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‖

source

@[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‖₊

source

@[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‖ₑ

source

@[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

source

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.

Equations

LinearIsometry.lTensor E f = TensorProduct.mapIsometry LinearIsometry.id f

Instances For

source

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.

Equations

LinearIsometry.rTensor G f = TensorProduct.mapIsometry f LinearIsometry.id

Instances For

source

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

source

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

source

@[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

source

@[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

source

@[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

source

@[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

source

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.

Equations

TensorProduct.congrIsometry f g = (TensorProduct.congr f.toLinearEquiv g.toLinearEquiv).isometryOfInner ⋯

Instances For

source

@[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

source

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

source

@[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

source

@[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)

source

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.

Equations

LinearIsometryEquiv.lTensor E f = TensorProduct.congrIsometry (LinearIsometryEquiv.refl 𝕜 E) f

Instances For

source

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.

Equations

LinearIsometryEquiv.rTensor G f = TensorProduct.congrIsometry f (LinearIsometryEquiv.refl 𝕜 G)

Instances For

source

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

source

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)

source

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

source

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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

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.

Equations

TensorProduct.mapInclIsometry E' F' = TensorProduct.mapIsometry E'.subtypeₗᵢ F'.subtypeₗᵢ

Instances For

source

@[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

source

@[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'

source

@[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

source

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.

Equations

TensorProduct.commIsometry 𝕜 E F = (TensorProduct.comm 𝕜 E F).isometryOfInner ⋯

Instances For

source

@[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

source

@[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

source

@[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

source

@[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‖

source

@[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‖₊

source

@[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‖ₑ

source

@[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

source

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.

Equations

TensorProduct.lidIsometry 𝕜 E = (TensorProduct.lid 𝕜 E).isometryOfInner ⋯

Instances For

source

@[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

source

@[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

source

@[simp]

theorem TensorProduct.toLinearEquiv_lidIsometry {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :

(lidIsometry 𝕜 E).toLinearEquiv = TensorProduct.lid 𝕜 E

source

@[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‖

source

@[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‖₊

source

@[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‖ₑ

source

@[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

source

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.

Equations

TensorProduct.assocIsometry 𝕜 E F G = (TensorProduct.assoc 𝕜 E F G).isometryOfInner ⋯

Instances For

source

@[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

source

@[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

source

@[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

source

@[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‖

source

@[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‖₊

source

@[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‖ₑ

source

@[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)

source

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.

source

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.

source

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} [DecidableEq ι₁] [DecidableEq ι₂] {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.

source

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} [DecidableEq ι₁] [DecidableEq ι₂] {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.

source

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} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) :

OrthonormalBasis (ι₁ × ι₂) 𝕜 (TensorProduct 𝕜 E F)

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

Equations

b₁.tensorProduct b₂ = (b₁.toBasis.tensorProduct b₂.toBasis).toOrthonormalBasis ⋯

Instances For

source

@[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} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) (i : ι₁) (j : ι₂) :

(b₁.tensorProduct b₂) (i, j) = b₁ i ⊗ₜ[𝕜] b₂ j

source

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} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) (i : ι₁ × ι₂) :

(b₁.tensorProduct b₂) i = b₁ i.1 ⊗ₜ[𝕜] b₂ i.2

source

@[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} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) (x : E) (y : F) (i : ι₁) (j : ι₂) :

(b₁.tensorProduct b₂).repr (x ⊗ₜ[𝕜] y) (i, j) = b₂.repr y j * b₁.repr x i

source

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} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) (x : E) (y : F) (i : ι₁ × ι₂) :

(b₁.tensorProduct b₂).repr (x ⊗ₜ[𝕜] y) i = b₂.repr y i.2 * b₁.repr x i.1

source

@[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} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) :

(b₁.tensorProduct b₂).toBasis = b₁.toBasis.tensorProduct b₂.toBasis

Documentation

Mathlib.Analysis.InnerProductSpace.TensorProduct

Inner product space structure on tensor product spaces #

Main definitions: #

TODO: #