Documentation

MIPRE.Background.LIDT.MIPStarRE.Quantum.FiniteMatrix.Order

Positive-semidefinite finite matrix order #

This module contains the order-theoretic facts for finite-dimensional complex matrix operators: trace control of positive operators, closedness of the positive-semidefinite cone, the corresponding ProperCone, and basic monotonicity facts for sandwiches, Kronecker products, and reindexing.

These are the matrix-operator facts used by the canonical SDP strong-duality argument in Section 9.

Basic order lemmas #

source
@[instance_reducible]
noncomputable def MIPStarRE.Quantum.instDecidableEq_mIPRE {d : Type u_1} :
DecidableEq d
Equations
Instances For
    source
    theorem MIPStarRE.Quantum.instNonnegSpectrumClassRealOp {d : Type u_1} [Fintype d] :
    NonnegSpectrumClass ℝ (Op d)
    source
    theorem MIPStarRE.Quantum.instNonUnitalContinuousFunctionalCalculusRealOpIsSelfAdjoint {d : Type u_1} [Fintype d] :
    NonUnitalContinuousFunctionalCalculus ℝ (Op d) IsSelfAdjoint
    source
    theorem MIPStarRE.Quantum.norm_apply_le_trace_re_of_nonneg {d : Type u_1} [Fintype d] {A : Op d} (hA : 0 ≤ A) (i j : d) :
    ‖A i j‖ ≤ (Matrix.trace A).re

    Every entry of a positive semidefinite finite matrix is bounded by its real trace.

    source
    theorem MIPStarRE.Quantum.norm_le_trace_re_of_nonneg {d : Type u_1} [Fintype d] {A : Op d} (hA : 0 ≤ A) :
    ‖A‖ ≤ (Matrix.trace A).re

    The elementwise matrix norm of a positive semidefinite finite matrix is bounded by its real trace.

    source
    theorem MIPStarRE.Quantum.isClosed_op_nonnegative {ι : Type u_2} :
    IsClosed {A : Op ι | 0 ≤ A}

    The positive-semidefinite cone in a matrix algebra is closed.

    source
    noncomputable def MIPStarRE.Quantum.opNonnegativeProperCone (d : Type u_2) [Fintype d] [DecidableEq d] :
    ProperCone ℝ (Op d)

    The positive-semidefinite cone in a finite matrix algebra as a proper cone.

    Equations
    Instances For

      Kronecker product order lemmas #

      source
      theorem MIPStarRE.Quantum.kronecker_nonneg {d₁ : Type u_2} {d₂ : Type u_3} [hd₁ : Finite d₁] [hd₂ : Finite d₂] {A : Op d₁} {B : Op d₂} (hA : 0 ≤ A) (hB : 0 ≤ B) :
      0 ≤ Matrix.kronecker A B

      Kronecker products preserve positivity.

      source
      theorem MIPStarRE.Quantum.kronecker_le_kronecker_right_one {d₁ : Type u_2} {d₂ : Type u_3} [hd₁ : Finite d₁] [hd₂ : Finite d₂] [DecidableEq d₂] {A : Op d₁} {B : Op d₂} (hA : 0 ≤ A) (hB : B ≤ 1) :
      Matrix.kronecker A B ≤ Matrix.kronecker A 1

      If 0 ≤ A and B ≤ 1, then A ⊗ B ≤ A ⊗ 1.

      source
      theorem MIPStarRE.Quantum.kronecker_mono_left {d₁ : Type u_2} {d₂ : Type u_3} [hd₁ : Finite d₁] [hd₂ : Finite d₂] {A₁ A₂ : Op d₁} {B : Op d₂} (hA : A₁ ≤ A₂) (hB : 0 ≤ B) :
      Matrix.kronecker A₁ B ≤ Matrix.kronecker A₂ B

      Kronecker product is monotone in the left factor against a PSD right factor.

      source
      theorem MIPStarRE.Quantum.reindex_nonneg {d₁ : Type u_2} {d₂ : Type u_3} [Finite d₁] [Finite d₂] (e : d₁ ≃ d₂) {A : Op d₁} (hA : 0 ≤ A) :
      0 ≤ (Matrix.reindex e e) A

      Simultaneous reindexing of rows and columns preserves positive semidefiniteness.

      source
      theorem MIPStarRE.Quantum.sq_le_self {d : Type u_1} [Fintype d] [DecidableEq d] {X : Op d} (hX : 0 ≤ X) (hXle : X ≤ 1) :
      X * X ≤ X

      An operator between 0 and 1 dominates its square.