Matrices of operators on a finite direct sum of copies of a Hilbert space

For a complex Hilbert space H and a finite type ι, the ℓ² direct sum of ι copies of H is the Hilbert space H ⊗ ℂ^ι (OperatorMatrix.Ampl ι H, the ι-fold amplification of H). An ι × ι matrix of operators on H acts on it by (M f) i = ∑ j, M i j (f j), and this action is a unital ⋆-algebra homomorphism from the matrices, with the conjugate transpose, to the bounded operators, with the adjoint (OperatorMatrix.toCLMStarAlgHom). This is what lets a construction written in the ring of operator matrices, where it is plain algebra, be read as a statement about operators on a Hilbert space.

Three facts about the embedding of H as the i₀-th copy (OperatorMatrix.emb, the embedding ξ ↦ ξ ⊗ e_{i₀} at a fixed unit vector of the ancilla ℂ^ι):

• it is isometric (inner_emb_emb, norm_emb);
• the compression of the operator of M to it is the entry M i₀ i₀ (inner_emb_toCLM_emb);
• a diagonal matrix with constant entry c acts as c ⊗ 1, which the embedding intertwines with c (toCLM_diagonal_emb); such an operator is positive when c is (isPositive_toCLM_diagonal).

These are the finite ancillas of planning/mipco-track.md §5, Phase 1: ι → H with the PiLp 2 structure, in place of a tensor product of Hilbert spaces.

@[reducible, inline]

abbrev MIPRE.OperatorMatrix.Ampl (ι : Type u_1) (H : Type u_2) : Type (max u_2 u_1)

The ℓ² direct sum of ι copies of H, that is H ⊗ ℂ^ι.

Equations

• MIPRE.OperatorMatrix.Ampl ι H = PiLp 2 fun (x : ι) => H

noncomputable def MIPRE.OperatorMatrix.toCLM {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (M : Matrix ι ι (H →L[ℂ] H)) : Ampl ι H →L[ℂ] Ampl ι H

The operator of a matrix of operators: (toCLM M f) i = ∑ j, M i j (f j).

Equations

• MIPRE.OperatorMatrix.toCLM M = ↑(PiLp.continuousLinearEquiv 2 ℂ fun (x : ι) => H).symm ∘SL ContinuousLinearMap.pi fun (i : ι) => ∑ j : ι, M i j ∘SL PiLp.proj 2 (fun (x : ι) => H) j

@[simp]

theorem MIPRE.OperatorMatrix.toCLM_apply {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (M : Matrix ι ι (H →L[ℂ] H)) (f : Ampl ι H) (i : ι) : ((toCLM M) f).ofLp i = ∑ j : ι, (M i j) (f.ofLp j)

theorem MIPRE.OperatorMatrix.toCLM_diagonal_apply {ι : Type u_1} {H : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (d : ι → H →L[ℂ] H) (f : Ampl ι H) (i : ι) : ((toCLM (Matrix.diagonal d)) f).ofLp i = (d i) (f.ofLp i)

theorem MIPRE.OperatorMatrix.toCLM_one {ι : Type u_1} {H : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] : toCLM 1 = 1

theorem MIPRE.OperatorMatrix.toCLM_mul {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (M N : Matrix ι ι (H →L[ℂ] H)) : toCLM (M * N) = toCLM M * toCLM N

theorem MIPRE.OperatorMatrix.toCLM_add {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (M N : Matrix ι ι (H →L[ℂ] H)) : toCLM (M + N) = toCLM M + toCLM N

theorem MIPRE.OperatorMatrix.toCLM_zero {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] : toCLM 0 = 0

theorem MIPRE.OperatorMatrix.toCLM_conjTranspose {ι : Type u_1} {H : Type u_2} [Fintype ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : Matrix ι ι (H →L[ℂ] H)) : toCLM M.conjTranspose = star (toCLM M)

The operator of the conjugate transpose is the adjoint.

theorem MIPRE.OperatorMatrix.toCLM_algebraMap {ι : Type u_1} {H : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (r : ℂ) : toCLM ((algebraMap ℂ (Matrix ι ι (H →L[ℂ] H))) r) = (algebraMap ℂ (Ampl ι H →L[ℂ] Ampl ι H)) r

noncomputable def MIPRE.OperatorMatrix.toCLMStarAlgHom {ι : Type u_1} {H : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : Matrix ι ι (H →L[ℂ] H) →⋆ₐ[ℂ] Ampl ι H →L[ℂ] Ampl ι H

The action of operator matrices, as a unital ⋆-algebra homomorphism.

Equations

• MIPRE.OperatorMatrix.toCLMStarAlgHom = { toFun := MIPRE.OperatorMatrix.toCLM, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

@[simp]

theorem MIPRE.OperatorMatrix.toCLMStarAlgHom_apply {ι : Type u_1} {H : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : Matrix ι ι (H →L[ℂ] H)) : toCLMStarAlgHom M = toCLM M

theorem MIPRE.OperatorMatrix.toCLM_sum {ι : Type u_1} {H : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {κ : Type u_3} (s : Finset κ) (M : κ → Matrix ι ι (H →L[ℂ] H)) : toCLM (∑ k ∈ s, M k) = ∑ k ∈ s, toCLM (M k)

noncomputable def MIPRE.OperatorMatrix.amplify {ι : Type u_1} {H : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : (H →L[ℂ] H) →⋆ₐ[ℂ] Ampl ι H →L[ℂ] Ampl ι H

The amplification c ↦ c ⊗ 1, the diagonal action of an operator, as a unital ⋆-algebra homomorphism.

Equations

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

theorem MIPRE.OperatorMatrix.amplify_apply {ι : Type u_1} {H : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (c : H →L[ℂ] H) : amplify c = toCLM (Matrix.diagonal fun (x : ι) => c)

theorem MIPRE.OperatorMatrix.isStarProjection_toCLM {ι : Type u_1} {H : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : Matrix ι ι (H →L[ℂ] H)} (hP : IsStarProjection P) : IsStarProjection (toCLM P)

The operator of a star projection of matrices is a star projection.

theorem MIPRE.OperatorMatrix.isPositive_toCLM_of_isStarProjection {ι : Type u_1} {H : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : Matrix ι ι (H →L[ℂ] H)} (hP : IsStarProjection P) : (toCLM P).IsPositive

The operator of a star projection of matrices is positive.

theorem MIPRE.OperatorMatrix.isPositive_toCLM_diagonal {ι : Type u_1} {H : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {c : H →L[ℂ] H} (hc : c.IsPositive) : (toCLM (Matrix.diagonal fun (x : ι) => c)).IsPositive

The diagonal action c ⊗ 1 of a positive operator is positive.

The embedding at a coordinate

noncomputable def MIPRE.OperatorMatrix.emb {ι : Type u_1} {H : Type u_2} [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (i₀ : ι) : H →L[ℂ] Ampl ι H

The embedding of H as the i₀-th copy, ξ ↦ ξ ⊗ e_{i₀}.

Equations

• MIPRE.OperatorMatrix.emb i₀ = ↑(PiLp.continuousLinearEquiv 2 ℂ fun (x : ι) => H).symm ∘SL ContinuousLinearMap.single ℂ (fun (x : ι) => H) i₀

theorem MIPRE.OperatorMatrix.emb_eq_single {ι : Type u_1} {H : Type u_2} [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (i₀ : ι) (ξ : H) : (emb i₀) ξ = PiLp.single 2 i₀ ξ

@[simp]

theorem MIPRE.OperatorMatrix.emb_apply_self {ι : Type u_1} {H : Type u_2} [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (i₀ : ι) (ξ : H) : ((emb i₀) ξ).ofLp i₀ = ξ

@[simp]

theorem MIPRE.OperatorMatrix.emb_apply_of_ne {ι : Type u_1} {H : Type u_2} [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] {i₀ i : ι} (h : i ≠ i₀) (ξ : H) : ((emb i₀) ξ).ofLp i = 0

theorem MIPRE.OperatorMatrix.inner_emb_emb {ι : Type u_1} {H : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (i₀ : ι) (ξ η : H) : inner ℂ ((emb i₀) ξ) ((emb i₀) η) = inner ℂ ξ η

theorem MIPRE.OperatorMatrix.norm_emb {ι : Type u_1} {H : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (i₀ : ι) (ξ : H) : ‖(emb i₀) ξ‖ = ‖ξ‖

theorem MIPRE.OperatorMatrix.inner_emb_toCLM_emb {ι : Type u_1} {H : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (M : Matrix ι ι (H →L[ℂ] H)) (i₀ : ι) (ξ η : H) : inner ℂ ((emb i₀) ξ) ((toCLM M) ((emb i₀) η)) = inner ℂ ξ ((M i₀ i₀) η)

The compression of the operator of M to the i₀-th copy is the entry M i₀ i₀.

theorem MIPRE.OperatorMatrix.toCLM_diagonal_emb {ι : Type u_1} {H : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup H] [InnerProductSpace ℂ H] (c : H →L[ℂ] H) (i₀ : ι) (ξ : H) : (toCLM (Matrix.diagonal fun (x : ι) => c)) ((emb i₀) ξ) = (emb i₀) (c ξ)

A constant diagonal matrix acts as c ⊗ 1, which the embedding intertwines with c.