Operator expectation infrastructure for the low individual degree test #
Expectation-value and normalized-trace lemmas for quantum operators.
Bridging lemmas: expectation-value linearity #
ev distributes over addition.
ev distributes over subtraction.
Algebraic lemmas for operator expectation values #
ev commutes with complex scalar multiplication by a real number.
ev commutes with the real scalar action on operators.
This is the real-scalar form of ev_scale; it is convenient when expanding
operator averages, whose weights act by the real scalar action before being
coerced to complex matrix scalars.
Self-difference and zero-matrix infrastructure #
ev of the zero operator is zero.
Expectation of a tensor product can be written using left/right placements.
A normalized state has unit expectation on the identity operator.
PSD trace positivity #
For a PSD state ψ and any operator M, E[Mᴴ M] ≥ 0.
Parallelogram inequality for normalized trace #
PSD trace nonnegativity for difference quadratic:
0 ≤ Re τ(ρ (D₁ - D₂)ᴴ(D₁ - D₂)) for PSD ρ.
Triangle inequality for normalized trace of PSD-weighted quadratic forms.
For PSD ρ, the real part of τ(ρ (D₁ + D₂)ᴴ(D₁ + D₂)) is bounded by twice
the sum of the corresponding quadratic forms for D₁ and D₂.
Operator-level triangle inequality for squared differences #
Operator-level triangle inequality for expectation of squared differences:
E[(X-Z)ᴴ(X-Z)] ≤ 2*(E[(X-Y)ᴴ(X-Y)] + E[(Y-Z)ᴴ(Y-Z)]).
Three-vector version of the normalized-trace triangle inequality.
If a difference is decomposed as three successive differences, its squared norm
is bounded by 3 times the sum of the three squared norms. This is the k = 3
case of the paper's prop:triangle-inequality-for-vectors-squared, and it is
used by the Step 6 projectivization chain in inductive_step.tex:154--158.
Three-step operator triangle inequality for squared differences.
Infrastructure for bridge lemma proofs #
ev distributes over finite sums.
ev distributes over univ sums.
Evaluation of an operator average is the average of the evaluations.
ev of a PSD operator is nonneg.
ev is monotone under the matrix order.
For Hermitian ρ, A, B: ev ψ (A * B) = ev ψ (B * A).
Follows from ntr(ρ B A) = conj(ntr(ρ A B)) when all three are Hermitian,
and Re is invariant under conjugation.
Taking the adjoint does not change ev.
ev commutes on PSD operators (convenience wrapper).
Cross-term identity: ev ψ (Bᴴ * A) = ev ψ (Aᴴ * B).
Cauchy-Schwarz for the state-weighted inner product:
(ev ψ (Aᴴ * B))² ≤ ev ψ (Aᴴ * A) * ev ψ (Bᴴ * B).
Absolute-value form of Cauchy-Schwarz for ev.
AM-GM for the quadratic form:
2 * ev ψ (Aᴴ * B) ≤ ev ψ (Aᴴ * A) + ev ψ (Bᴴ * B).
Jensen inequality for the quadratic form: for a finite family of operators,
ev ψ ((∑ Xᵢ)ᴴ * (∑ Xᵢ)) ≤ n * ∑ ev ψ (XᵢᴴXᵢ).
Bipartite-tensor sandwich Cauchy–Schwarz #
The lemmas below give the operator/real Cauchy–Schwarz step for expectations of
sandwiched products lifted to a bipartite tensor space. They are a reusable
primitive toward the raw Q₂ → Q₃ and Q₃ → Q₄ Cauchy–Schwarz estimates of
self_improvement.tex, lines 306–311 and 326–332 (the
eq:change-one-cauchy-schwarz and eq:change-another displays), where the
bilinear form is ⟨X, Y⟩_{M, T} := ev ψ (opTensor (Xᴴ · M · Y) T) with PSD
M, T.
Bipartite-tensor Cauchy–Schwarz for state expectations.
For PSD operators M, T and arbitrary operators X, Y,
(ev ψ (opTensor (Xᴴ M Y) T))² ≤ ev ψ (opTensor (Xᴴ M X) T) * ev ψ (opTensor (Yᴴ M Y) T).
The proof factors M = √M · √M, T = √T · √T (continuous functional calculus
square roots) and applies ev_cauchy_schwarz to
opTensor (√M · X) √T and opTensor (√M · Y) √T.
Absolute-value form of the bipartite-tensor sandwich Cauchy–Schwarz.