@[reducible, inline]

abbrev HilbertSchmidtOperatorSpace.HSIndex (ℋ : Type u) [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : Type

The canonical finite index used for Hilbert-Schmidt coordinates.

Equations

• HilbertSchmidtOperatorSpace.HSIndex ℋ = Fin (Module.finrank ℂ ℋ)

@[reducible, inline]

noncomputable abbrev HilbertSchmidtOperatorSpace.hsOrthonormalBasis {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : OrthonormalBasis (HSIndex ℋ) ℂ ℋ

The standard orthonormal basis on a finite-dimensional Hilbert space.

Equations

• HilbertSchmidtOperatorSpace.hsOrthonormalBasis = stdOrthonormalBasis ℂ ℋ

@[reducible, inline]

abbrev HilbertSchmidtOperatorSpace.HSCoords (ℋ : Type u) [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : Type

Coordinate space for Hilbert-Schmidt operators.

Equations

• HilbertSchmidtOperatorSpace.HSCoords ℋ = EuclideanSpace ℂ (HilbertSchmidtOperatorSpace.HSIndex ℋ × HilbertSchmidtOperatorSpace.HSIndex ℋ)

@[reducible, inline]

abbrev HilbertSchmidtOperatorSpace.HSCoordFun (ℋ : Type u) [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : Type

The underlying coordinate function space for Hilbert-Schmidt operators.

Equations

• HilbertSchmidtOperatorSpace.HSCoordFun ℋ = (HilbertSchmidtOperatorSpace.HSIndex ℋ × HilbertSchmidtOperatorSpace.HSIndex ℋ → ℂ)

def HilbertSchmidtOperatorSpace.HSOp (ℋ : Type u) [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] : Type u

The operator space L ℋ, viewed later with the Hilbert-Schmidt structure.

Equations

• HilbertSchmidtOperatorSpace.HSOp ℋ = LownerHeinzTheorem.L ℋ

@[implicit_reducible]

instance HilbertSchmidtOperatorSpace.instAddCommGroupHSOp {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] : AddCommGroup (HSOp ℋ)

Equations

• HilbertSchmidtOperatorSpace.instAddCommGroupHSOp = id inferInstance

@[implicit_reducible]

instance HilbertSchmidtOperatorSpace.instModuleComplexHSOp {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] : Module ℂ (HSOp ℋ)

Equations

• HilbertSchmidtOperatorSpace.instModuleComplexHSOp = id inferInstance

@[implicit_reducible]

noncomputable instance HilbertSchmidtOperatorSpace.instStarHSOp {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] : Star (HSOp ℋ)

Equations

• HilbertSchmidtOperatorSpace.instStarHSOp = id inferInstance

@[implicit_reducible]

instance HilbertSchmidtOperatorSpace.instMulHSOp {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] : Mul (HSOp ℋ)

Equations

• HilbertSchmidtOperatorSpace.instMulHSOp = id inferInstance

@[implicit_reducible]

instance HilbertSchmidtOperatorSpace.instOneHSOp {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] : One (HSOp ℋ)

Equations

• HilbertSchmidtOperatorSpace.instOneHSOp = id inferInstance

@[implicit_reducible]

instance HilbertSchmidtOperatorSpace.instInhabitedHSOp {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] : Inhabited (HSOp ℋ)

Equations

• HilbertSchmidtOperatorSpace.instInhabitedHSOp = id inferInstance

@[implicit_reducible]

instance HilbertSchmidtOperatorSpace.instZeroHSOp {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] : Zero (HSOp ℋ)

Equations

• HilbertSchmidtOperatorSpace.instZeroHSOp = id inferInstance

instance HilbertSchmidtOperatorSpace.instFiniteDimensionalComplexHSOp {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : FiniteDimensional ℂ (HSOp ℋ)

noncomputable def HilbertSchmidtOperatorSpace.hsCoordsLinearEquiv {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : HSCoords ℋ ≃ₗ[ℂ] HSCoordFun ℋ

Equations

• HilbertSchmidtOperatorSpace.hsCoordsLinearEquiv = id (WithLp.linearEquiv 2 ℂ (HilbertSchmidtOperatorSpace.HSCoordFun ℋ))

def HilbertSchmidtOperatorSpace.matrixToFun {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : Matrix (HSIndex ℋ) (HSIndex ℋ) ℂ ≃ₗ[ℂ] HSCoordFun ℋ

Equations

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

noncomputable def HilbertSchmidtOperatorSpace.matrixToCoords {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : Matrix (HSIndex ℋ) (HSIndex ℋ) ℂ ≃ₗ[ℂ] HSCoords ℋ

Equations

• HilbertSchmidtOperatorSpace.matrixToCoords = HilbertSchmidtOperatorSpace.matrixToFun ≪≫ₗ HilbertSchmidtOperatorSpace.hsCoordsLinearEquiv.symm

noncomputable def HilbertSchmidtOperatorSpace.hsLinearMapEquiv {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : HSOp ℋ ≃ₗ[ℂ] ℋ →ₗ[ℂ] ℋ

Forget continuity and identify continuous linear operators with linear endomorphisms.

Equations

• HilbertSchmidtOperatorSpace.hsLinearMapEquiv = LinearMap.toContinuousLinearMap.symm

noncomputable def HilbertSchmidtOperatorSpace.toHSCoordsLinearEquiv {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : HSOp ℋ ≃ₗ[ℂ] HSCoords ℋ

Hilbert-Schmidt coordinates on L ℋ.

Equations

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

@[simp]

theorem HilbertSchmidtOperatorSpace.toHSCoordsLinearEquiv_apply_apply {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] (T : HSOp ℋ) (i j : HSIndex ℋ) : (toHSCoordsLinearEquiv T).ofLp (i, j) = (LinearMap.toMatrix hsOrthonormalBasis.toBasis hsOrthonormalBasis.toBasis) (hsLinearMapEquiv T) i j

@[implicit_reducible]

noncomputable instance HilbertSchmidtOperatorSpace.instNormedAddCommGroupHSOp {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : NormedAddCommGroup (HSOp ℋ)

Equations

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

@[implicit_reducible]

noncomputable instance HilbertSchmidtOperatorSpace.instNormedSpaceComplexHSOp {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : NormedSpace ℂ (HSOp ℋ)

Equations

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

@[implicit_reducible]

noncomputable instance HilbertSchmidtOperatorSpace.instInnerComplexHSOp {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : Inner ℂ (HSOp ℋ)

Equations

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

@[implicit_reducible]

noncomputable instance HilbertSchmidtOperatorSpace.instInnerProductSpaceComplexHSOp {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : InnerProductSpace ℂ (HSOp ℋ)

Equations

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

noncomputable def HilbertSchmidtOperatorSpace.toHSCoordsLinearIsometryEquiv {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : HSOp ℋ ≃ₗᵢ[ℂ] HSCoords ℋ

Hilbert-Schmidt coordinates as a linear isometry.

Equations

• HilbertSchmidtOperatorSpace.toHSCoordsLinearIsometryEquiv = HilbertSchmidtOperatorSpace.toHSCoordsLinearEquiv.isometryOfInner ⋯

instance HilbertSchmidtOperatorSpace.instCompleteSpaceHSOp {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : CompleteSpace (HSOp ℋ)

instance HilbertSchmidtOperatorSpace.instContinuousSMulComplexHSOp {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : ContinuousSMul ℂ (HSOp ℋ)

@[reducible, inline]

abbrev HilbertSchmidtOperatorSpace.ofOp {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] (T : LownerHeinzTheorem.L ℋ) : HSOp ℋ

Reinterpret an operator as an element of the Hilbert-Schmidt operator space.

Equations

• HilbertSchmidtOperatorSpace.ofOp T = T

@[reducible, inline]

abbrev HilbertSchmidtOperatorSpace.toOp {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] (T : HSOp ℋ) : LownerHeinzTheorem.L ℋ

Forget the Hilbert-Schmidt structure and recover the underlying operator.

Equations

• HilbertSchmidtOperatorSpace.toOp T = T

noncomputable def HilbertSchmidtOperatorSpace.leftMulHS {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] (A : LownerHeinzTheorem.L ℋ) : HSOp ℋ →L[ℂ] HSOp ℋ

Left multiplication on the Hilbert-Schmidt operator space.

Equations

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

noncomputable def HilbertSchmidtOperatorSpace.rightMulHS {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] (B : LownerHeinzTheorem.L ℋ) : HSOp ℋ →L[ℂ] HSOp ℋ

Right multiplication on the Hilbert-Schmidt operator space.

Equations

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

@[simp]

theorem HilbertSchmidtOperatorSpace.leftMulHS_apply {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] (A : LownerHeinzTheorem.L ℋ) (T : HSOp ℋ) : toOp ((leftMulHS A) T) = A * toOp T

@[simp]

theorem HilbertSchmidtOperatorSpace.rightMulHS_apply {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] (B : LownerHeinzTheorem.L ℋ) (T : HSOp ℋ) : toOp ((rightMulHS B) T) = toOp T * B

@[simp]

theorem HilbertSchmidtOperatorSpace.leftMulHS_mul {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] (A B : LownerHeinzTheorem.L ℋ) : leftMulHS (A * B) = leftMulHS A * leftMulHS B

@[simp]

theorem HilbertSchmidtOperatorSpace.rightMulHS_mul {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] (A B : LownerHeinzTheorem.L ℋ) : rightMulHS (A * B) = rightMulHS B * rightMulHS A

@[simp]

theorem HilbertSchmidtOperatorSpace.leftMulHS_one {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : leftMulHS 1 = 1

@[simp]

theorem HilbertSchmidtOperatorSpace.rightMulHS_one {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] : rightMulHS 1 = 1

theorem HilbertSchmidtOperatorSpace.leftMulHS_rightMulHS_commute {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [FiniteDimensional ℂ ℋ] (A B : LownerHeinzTheorem.L ℋ) : Commute (leftMulHS A) (rightMulHS B)

theorem HilbertSchmidtOperatorSpace.hsInner_eq_trace {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] (X Y : LownerHeinzTheorem.L ℋ) : inner ℂ (ofOp X) (ofOp Y) = (LinearMap.trace ℂ ℋ) ↑(star X * Y)

theorem HilbertSchmidtOperatorSpace.re_hsInner_eq_traceRe {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] (X Y : LownerHeinzTheorem.L ℋ) : (inner ℂ (ofOp X) (ofOp Y)).re = ((LinearMap.trace ℂ ℋ) ↑(star X * Y)).re

@[simp]

theorem HilbertSchmidtOperatorSpace.leftMulHS_star {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] (A : LownerHeinzTheorem.L ℋ) : star (leftMulHS A) = leftMulHS (star A)

@[simp]

theorem HilbertSchmidtOperatorSpace.leftMulHS_real_smul_one {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] (r : ℝ) : leftMulHS (r • 1) = r • 1

@[simp]

theorem HilbertSchmidtOperatorSpace.rightMulHS_real_smul_one {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] (r : ℝ) : rightMulHS (r • 1) = r • 1

theorem HilbertSchmidtOperatorSpace.leftMulHS_nonneg {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] {A : LownerHeinzTheorem.L ℋ} (hA0 : 0 ≤ A) : 0 ≤ leftMulHS A

theorem HilbertSchmidtOperatorSpace.leftMulHS_le_leftMulHS {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] {A B : LownerHeinzTheorem.L ℋ} (hAB : A ≤ B) : leftMulHS A ≤ leftMulHS B

theorem HilbertSchmidtOperatorSpace.leftMulHS_pdSet {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] [ContinuousFunctionalCalculus ℝ (LownerHeinzTheorem.L ℋ) IsSelfAdjoint] [Nontrivial (LownerHeinzTheorem.L ℋ)] {A : LownerHeinzTheorem.L ℋ} (hA : A ∈ GeneralizedPerspectiveFunction.pdSet) : leftMulHS A ∈ GeneralizedPerspectiveFunction.pdSet

@[simp]

theorem HilbertSchmidtOperatorSpace.rightMulHS_star {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] (A : LownerHeinzTheorem.L ℋ) : star (rightMulHS A) = rightMulHS (star A)

noncomputable def HilbertSchmidtOperatorSpace.leftMulHSStarAlgHom {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] : LownerHeinzTheorem.L ℋ →⋆ₐ[ℝ] LownerHeinzTheorem.L (HSOp ℋ)

Left multiplication as a real ⋆-algebra homomorphism on the Hilbert-Schmidt operator space.

Equations

• HilbertSchmidtOperatorSpace.leftMulHSStarAlgHom = { toFun := HilbertSchmidtOperatorSpace.leftMulHS, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

noncomputable def HilbertSchmidtOperatorSpace.rightMulHSStarAlgHom {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] : (LownerHeinzTheorem.L ℋ)ᵐᵒᵖ →⋆ₐ[ℝ] LownerHeinzTheorem.L (HSOp ℋ)

Right multiplication as a real ⋆-algebra homomorphism out of the opposite algebra.

Equations

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

@[simp]

theorem HilbertSchmidtOperatorSpace.rightMulHSStarAlgHom_apply {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] (A : (LownerHeinzTheorem.L ℋ)ᵐᵒᵖ) : rightMulHSStarAlgHom A = rightMulHS (MulOpposite.unop A)

noncomputable def HilbertSchmidtOperatorSpace.opStarHSStarAlgHom {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] : LownerHeinzTheorem.L ℋ →⋆ₐ[ℝ] (LownerHeinzTheorem.L ℋ)ᵐᵒᵖ

The ⋆-algebra hom sending A to op (star A). On selfadjoint operators this is just op.

Equations

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

theorem HilbertSchmidtOperatorSpace.op_isSelfAdjoint {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (A : LownerHeinzTheorem.L ℋ) (hA : IsSelfAdjoint A) : IsSelfAdjoint (MulOpposite.op A)

theorem HilbertSchmidtOperatorSpace.spectrum_op_eq {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [ContinuousFunctionalCalculus ℝ (LownerHeinzTheorem.L ℋ) IsSelfAdjoint] [Nontrivial (LownerHeinzTheorem.L ℋ)] (A : LownerHeinzTheorem.L ℋ) (hA : IsSelfAdjoint A) : spectrum ℝ (MulOpposite.op A) = spectrum ℝ A

theorem HilbertSchmidtOperatorSpace.cfc_op_eq_op_cfc {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] [ContinuousFunctionalCalculus ℝ (LownerHeinzTheorem.L ℋ) IsSelfAdjoint] [ContinuousFunctionalCalculus ℝ (LownerHeinzTheorem.L ℋ)ᵐᵒᵖ IsSelfAdjoint] [Nontrivial (LownerHeinzTheorem.L ℋ)] (f : ℝ → ℝ) (A : LownerHeinzTheorem.L ℋ) (hA : IsSelfAdjoint A) (hf : ContinuousOn f (spectrum ℝ A)) : cfc f (MulOpposite.op A) = MulOpposite.op (LownerHeinzTheorem.cfcR f A)

theorem HilbertSchmidtOperatorSpace.leftMulHS_cfcR {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] [ContinuousFunctionalCalculus ℝ (LownerHeinzTheorem.L ℋ) IsSelfAdjoint] [Nontrivial (LownerHeinzTheorem.L ℋ)] (f : ℝ → ℝ) (A : LownerHeinzTheorem.L ℋ) (hA : IsSelfAdjoint A) (hf : ContinuousOn f (spectrum ℝ A)) : leftMulHS (LownerHeinzTheorem.cfcR f A) = LownerHeinzTheorem.cfcR f (leftMulHS A)

theorem HilbertSchmidtOperatorSpace.rightMulHS_cfcR {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] [ContinuousFunctionalCalculus ℝ (LownerHeinzTheorem.L ℋ) IsSelfAdjoint] [ContinuousFunctionalCalculus ℝ (LownerHeinzTheorem.L ℋ)ᵐᵒᵖ IsSelfAdjoint] [Nontrivial (LownerHeinzTheorem.L ℋ)] (f : ℝ → ℝ) (A : LownerHeinzTheorem.L ℋ) (hA : IsSelfAdjoint A) (hf : ContinuousOn f (spectrum ℝ A)) : rightMulHS (LownerHeinzTheorem.cfcR f A) = LownerHeinzTheorem.cfcR f (rightMulHS A)