Operator expectation infrastructure for the low individual degree test

This is the counterpart, in the port of the low-individual-degree test to the symmetric model (planning/c6b-plan.md, milestone M0, and its section "Port conventions"), of MIPRE/Background/LIDT/MIPStarRE/LDT/Basic/OperatorExpectations.lean: the triangle, Cauchy–Schwarz and Jensen inequalities for the expectation S.ev X = Re ⟪Ψ, X Ψ⟫, and the Cauchy–Schwarz inequality for sandwiched product placements.

The vendored proofs go through the density matrix and the cyclicity of the trace. Here the state is a vector, S.ev (star M * M) = ‖M Ψ‖² (VecState.ev_adjoint_self_eq_norm_sq), and every inequality is one of norms in K: the triangle inequalities are the triangle inequality of K (the per-term forms of StateModel.sum_snorm_sq_triangle and sum_snorm_sq_triangle3), and Cauchy–Schwarz is StateModel.abs_qform_star_mul_le (MIPRE/Foundations/Sandwich.lean) applied to the state model S.toStateModel, whose quadratic form is ev by definition. Every lemma except the sandwich ones uses only the state, so it is a VecState lemma (Co/Basic/QuantumState.lean), which applies as well to S : SymModel 𝔓 K.

The linear and positivity lemmas of the vendored file (ev_add, ev_sub, ev_scale, ev_real_smul, ev_zero, ev_opTensor, ev_one_of_isNormalized, ev_adjoint_self_nonneg, ev_finset_sum, ev_sum, ev_nonneg_of_psd, ev_mono, ev_conjTranspose, ev_mul_comm_of_hermitian, ev_mul_comm_of_psd, ev_conjTranspose_mul_comm) are ported in Co/Basic/QuantumState.lean, with every positivity fact of the port.

Not ported

Matrix-only declarations of the vendored file, about the normalized trace of a density matrix, each replaced by the norm of K:

• normalizedTrace_diff_sq_nonneg: the model has no trace; S.ev_adjoint_self_nonneg is the vector form.
• normalizedTrace_triangle: the model has no trace; its content is ev_diff_triangle, proved from the triangle inequality of K.
• normalizedTrace_triangle_three: the model has no trace; its content is ev_diff_triangle_three, proved from the triangle inequality of K.
• normalizedTrace_conjTranspose: the model has no trace; S.ev_conjTranspose is the vector form.

Operator-level triangle inequality for squared differences

theorem MIPRE.LIDT.Co.VecState.ev_diff_triangle {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (X Y Z : K →L[ℂ] K) : V.ev (star (X - Z) * (X - Z)) ≤ 2 * (V.ev (star (X - Y) * (X - Y)) + V.ev (star (Y - Z) * (Y - Z)))

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)]). This is the per-term inequality of the repository's MIPRE.StateModel.sum_snorm_sq_triangle (MIPRE/Foundations/StateModel.lean).

theorem MIPRE.LIDT.Co.VecState.ev_diff_triangle_three {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (X Y Z W : K →L[ℂ] K) : V.ev (star (X - W) * (X - W)) ≤ 3 * (V.ev (star (X - Y) * (X - Y)) + V.ev (star (Y - Z) * (Y - Z)) + V.ev (star (Z - W) * (Z - W)))

Three-step operator triangle inequality for squared differences.

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, used by the Step 6 projectivization chain in inductive_step.tex:154--158. This is the per-term inequality of the repository's MIPRE.StateModel.sum_snorm_sq_triangle3 (MIPRE/Foundations/StateModel.lean).

Averages

theorem MIPRE.LIDT.Co.VecState.ev_averageOperatorOverDistribution {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {α : Type u_2} (𝒟 : MIPStarRE.LDT.Distribution α) (A : α → K →L[ℂ] K) : V.ev (averageOperatorOverDistribution 𝒟 A) = MIPStarRE.LDT.avgOver 𝒟 fun (a : α) => V.ev (A a)

Evaluation of an operator average is the average of the evaluations.

Cauchy–Schwarz

theorem MIPRE.LIDT.Co.VecState.abs_ev_star_mul_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (A B : K →L[ℂ] K) : |V.ev (star A * B)| ≤ ‖A V.Ψ‖ * ‖B V.Ψ‖

Cauchy–Schwarz in the absolute-value form with state norms: |ev (A* B)| ≤ ‖A Ψ‖ ‖B Ψ‖ (StateModel.abs_qform_star_mul_le on V.toStateModel).

theorem MIPRE.LIDT.Co.VecState.ev_cauchy_schwarz {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (A B : K →L[ℂ] K) : V.ev (star A * B) ^ 2 ≤ V.ev (star A * A) * V.ev (star B * B)

Cauchy-Schwarz for the state-weighted inner product: (ev (A* B))² ≤ ev (A* A) * ev (B* B).

theorem MIPRE.LIDT.Co.VecState.ev_abs_mul_le_sqrt {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (A B : K →L[ℂ] K) : |V.ev (A * B)| ≤ √(V.ev (A * star A)) * √(V.ev (star B * B))

Absolute-value form of Cauchy-Schwarz for ev.

theorem MIPRE.LIDT.Co.VecState.ev_cross_term_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (A B : K →L[ℂ] K) : 2 * V.ev (star A * B) ≤ V.ev (star A * A) + V.ev (star B * B)

AM-GM for the quadratic form: 2 * ev (A* B) ≤ ev (A* A) + ev (B* B).

theorem MIPRE.LIDT.Co.VecState.ev_sum_conjTranspose_mul_sum_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) {α : Type u_2} [Fintype α] (X : α → K →L[ℂ] K) : V.ev (star (∑ a : α, X a) * ∑ a : α, X a) ≤ ↑(Fintype.card α) * ∑ a : α, V.ev (star (X a) * X a)

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 the two players. 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 positive M, T.

theorem MIPRE.LIDT.Co.SymModel.ev_opTensor_sandwich_cauchy_schwarz {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (X Y M T : 𝔓) (hM : 0 ≤ M) (hT : 0 ≤ T) : S.ev (S.opTensor (star X * M * Y) T) ^ 2 ≤ S.ev (S.opTensor (star X * M * X) T) * S.ev (S.opTensor (star Y * M * Y) T)

Bipartite-tensor Cauchy–Schwarz for state expectations.

For positive M, T and arbitrary local 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 (the vendored proof uses the square roots of the continuous functional calculus) and applies ev_cauchy_schwarz to opTensor (m X) t and opTensor (m Y) t.

theorem MIPRE.LIDT.Co.SymModel.ev_opTensor_sandwich_diag_nonneg {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (X M T : 𝔓) (hM : 0 ≤ M) (hT : 0 ≤ T) : 0 ≤ S.ev (S.opTensor (star X * M * X) T)

Diagonal sandwich expectation ev (opTensor (X* M X) T) is nonneg when M, T are positive.

theorem MIPRE.LIDT.Co.SymModel.ev_opTensor_sandwich_abs_le_sqrt {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (X Y M T : 𝔓) (hM : 0 ≤ M) (hT : 0 ≤ T) : |S.ev (S.opTensor (star X * M * Y) T)| ≤ √(S.ev (S.opTensor (star X * M * X) T)) * √(S.ev (S.opTensor (star Y * M * Y) T))

Absolute-value form of the bipartite-tensor sandwich Cauchy–Schwarz.