Operator bounds on matrices, by hand #
The rigidity arguments of the Pauli basis test's appendix are chains of estimates
‖M |ψ⟩‖ ≤ …, and the only thing they need about the operators in front is a bound
‖M v‖ ≤ K ‖v‖. Bnd M K is that bound, with the four closure properties the chains use ---
sums, products, scalars, and the two sources: a self-adjoint contraction has Bnd M 1, and an
isometry has ‖M v‖ = ‖v‖ on the nose.
This is the ℓ² operator norm, spelled as a relation instead of a number. That is deliberate.
Mathlib has the norm, through Matrix.toEuclideanCLM and the C*-algebra structure on
continuous linear maps, but the Loewner order on EuclideanSpace ℂ n →L[ℂ] EuclideanSpace ℂ n
costs enough instance search to time out the elaborator on a statement as small as
T * T ≤ 1 → ‖T‖ ≤ 1. The order the arguments actually need is the one on matrices
(Matrix.nonneg_iff_posSemidef, which is cheap), so the bridge here goes from a matrix
inequality straight to a vector-norm inequality and never mentions an operator norm.
The instance of the Hilbert-space calculus. The bound, the state norm and the quadratic
form of this file are those of the matrix state model StateModel.mat v
(MIPRE/Foundations/StateModel.lean), where matrices act on EuclideanSpace ℂ N through
Matrix.toEuclideanCLM (bnd_iff, snorm_eq_mat, qform_eq_mat), and their rules are proved
there once, for every represented algebra (Phase 1(b) of planning/mipco-track.md). The state
norm is the model's by definition, so its rules are the model's rules verbatim. What this file
adds is about matrices: the matrix order, and the Kronecker embeddings of the two factors.
A vector of N → ℂ, as a vector of EuclideanSpace ℂ N.
Equations
- MIPRE.evec v = WithLp.toLp 2 v
Instances For
The bound #
The bound is that of the matrix model, whatever its state.
The norm on a fixed state #
snorm v M = ‖M v‖. Every estimate in a rigidity argument is a statement about this, and the
four rules below --- the triangle inequality, scalars, a bound in front, an isometry in front ---
are all of them.
The state norm is that of the matrix model, by definition.
The quadratic form #
The quadratic form is that of the matrix model.
A self-adjoint contraction is bounded by one. The hypothesis is the matrix
inequality M† M ≤ 1, which is Matrix.PosSemidef of the difference.
The bipartite structure #
A soundness argument on a bipartite state works with two commuting copies of a matrix algebra
inside the one on the product space: aOp X = X ⊗ Id for the first factor and bOp Y = Id ⊗ Y
for the second. Both are ring homomorphisms, they commute with each other, and both carry a
matrix contraction to a Bnd _ 1, which is all the estimates need.
A contraction on the first factor is a contraction on the product space.
A contraction on the second factor is a contraction on the product space.