Documentation

MIPRE.Background.LIDT.MIPStarRE.Quantum.FiniteMatrix.NormalizedTrace

Normalized trace, projectors, and spectral truncation #

This module contains the normalized trace τ, the squared τ-norm, the paper-facing orthogonal-projection name, and the spectral-truncation witness used in the low individual degree test formalization.

Normalized trace #

source
noncomputable def MIPStarRE.Quantum.normalizedTrace {d : Type u_1} [Fintype d] (A : Op d) :
ℂ

The normalized trace τ(A) = tr(A) / |d|.

Equations
Instances For
    source
    @[simp]
    theorem MIPStarRE.Quantum.normalizedTrace_zero {d : Type u_1} [Fintype d] :
    normalizedTrace 0 = 0

    The normalized trace of the zero operator is zero.

    source
    @[simp]
    theorem MIPStarRE.Quantum.normalizedTrace_one {d : Type u_1} [Fintype d] [DecidableEq d] [Nonempty d] :
    normalizedTrace 1 = 1

    The normalized trace of the identity operator is one.

    source
    theorem MIPStarRE.Quantum.normalizedTrace_add {d : Type u_1} [Fintype d] (A B : Op d) :
    normalizedTrace (A + B) = normalizedTrace A + normalizedTrace B

    The normalized trace is additive.

    source
    theorem MIPStarRE.Quantum.normalizedTrace_sub {d : Type u_1} [Fintype d] (A B : Op d) :
    normalizedTrace (A - B) = normalizedTrace A - normalizedTrace B

    The normalized trace sends subtraction to subtraction.

    source
    theorem MIPStarRE.Quantum.normalizedTrace_smul {d : Type u_1} [Fintype d] (c : ℂ) (A : Op d) :
    normalizedTrace (c • A) = c * normalizedTrace A

    Scalar multiplication pulls out of the normalized trace.

    source
    theorem MIPStarRE.Quantum.normalizedTrace_mul_comm {d : Type u_1} [Fintype d] (A B : Op d) :
    normalizedTrace (A * B) = normalizedTrace (B * A)

    The normalized trace is invariant under swapping two multiplicative factors.

    source
    theorem MIPStarRE.Quantum.normalizedTrace_reindex {d₁ : Type u_2} {d₂ : Type u_3} [Fintype d₁] [Fintype d₂] (e : d₁ ≃ d₂) (A : Op d₁) :
    normalizedTrace ((Matrix.reindex e e) A) = normalizedTrace A

    Simultaneous reindexing of rows and columns preserves the normalized trace.

    Squared τ-norm #

    source
    noncomputable def MIPStarRE.Quantum.tauNormSq {d : Type u_1} [Fintype d] (A : Op d) :
    ℂ

    The squared τ-norm: ‖A‖²_τ = τ(A⋆ A). In finite dimensions this is (1/d) ∑ᵢⱼ |Aᵢⱼ|², the normalized squared Frobenius norm.

    Equations
    Instances For
      source
      @[simp]
      theorem MIPStarRE.Quantum.tauNormSq_zero {d : Type u_1} [Fintype d] :
      tauNormSq 0 = 0

      The squared τ-norm of the zero operator is zero.

      Projector predicate #

      source
      @[reducible, inline]
      abbrev MIPStarRE.Quantum.IsProj {d : Type u_1} [Fintype d] (P : Op d) :
      Prop

      Paper-facing name for Mathlib's predicate that a matrix is a self-adjoint idempotent.

      Equations
      Instances For

        Spectral truncation #

        source
        structure MIPStarRE.Quantum.SpectralTruncation {d : Type u_1} [Fintype d] (source target : Op d) :
        Prop

        A spectral truncation witness records the passage from a Hermitian matrix source to a projection target by truncating the spectrum to {0, 1}: eigenvalues above 1 / 2 are rounded to 1, and those below are rounded to 0.

        The key output is the τ-distance bound between source and target.

        • sourceHermitian : Matrix.IsHermitian source

          The source matrix is Hermitian.

        • targetProj : IsProj target

          The target matrix is an orthogonal projection.

        • tauDistanceBound : (tauNormSq (source - target)).re ≤ (tauNormSq (source * source - source)).re

          Spectral truncation does not increase the defect measured by tauNormSq.

        Instances For