Switch-sandwich preparation: diagonal masses and bounded operators

Bridge lemmas for prop:switch-sandwich: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/SwitchSandwichPrep/Core.lean in the port of planning/c6b-plan.md (milestone M3, section "Port conventions").

The diagonal-mass lemmas use a single state and joint operators, so they take a vector state V : VecState K (a symmetric model is accepted through its coercion) and submeasurements in K →L[ℂ] K. They drop the vendored normalization hypothesis hψ : ψ.IsNormalized, which is a theorem of the vector state (V.ev_one_of_isNormalized). The projective and OpBounded01 lemmas do not mention the state, and are stated for any C*-algebra with its order (local operators in 𝔓, joint ones in K →L[ℂ] K), or for any ordered ⋆-ring where the proof needs no more; opBounded01_hermitian obtains star B = B from IsSelfAdjoint.of_nonneg, in place of the vendored positive semidefiniteness of matrices. leftTensor_opBounded01 takes the model S : SymModel 𝔓 K as a new first explicit argument, as in Co/Preliminaries/Defs.lean.

Not ported

• weightedFinsetCauchySchwarz: classical, imported.
• weightedFinsetCauchySchwarz_on_selectedSupport: classical, imported.

theorem MIPRE.LIDT.Co.Preliminaries.subMeas_diagMass_le_mass {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_2} [Fintype Outcome] (V : VecState K) (A : SubMeas Outcome (K →L[ℂ] K)) : ∑ a : Outcome, V.ev (A.outcome a * A.outcome a) ≤ V.ev A.total

The diagonal mass of a sub-measurement is bounded by its total mass.

theorem MIPRE.LIDT.Co.Preliminaries.subMeas_diagMass_le_one {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_2} [Fintype Outcome] (V : VecState K) (A : SubMeas Outcome (K →L[ℂ] K)) : ∑ a : Outcome, V.ev (A.outcome a * A.outcome a) ≤ 1

The diagonal mass of a sub-measurement is at most 1 (the state is normalized).

theorem MIPRE.LIDT.Co.Preliminaries.projSubMeas_diagMass_eq_mass {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_2} [Fintype Outcome] (V : VecState K) (A : ProjSubMeas Outcome (K →L[ℂ] K)) : ∑ a : Outcome, V.ev (A.outcome a * A.outcome a) = V.ev A.total

Projective outcomes satisfy P_a^2 = P_a, so diagonal mass equals total mass.

theorem MIPRE.LIDT.Co.Preliminaries.projSubMeas_outcome_mul_total_eq_outcome {R : Type u_1} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] {Outcome : Type u_2} [Fintype Outcome] (A : ProjSubMeas Outcome R) (a : Outcome) : A.outcome a * A.total = A.outcome a

Each projective outcome is absorbed by the total projector.

theorem MIPRE.LIDT.Co.Preliminaries.projSubMeas_total_proj {R : Type u_1} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] {Outcome : Type u_2} [Fintype Outcome] (A : ProjSubMeas Outcome R) : A.total * A.total = A.total

The total operator of a projective sub-measurement is itself a projector.

theorem MIPRE.LIDT.Co.Preliminaries.opBounded01_sq_le_one {R : Type u_1} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] {B : R} (hB : OpBounded01 B) : B * B ≤ 1

Any OpBounded01 operator satisfies B * B ≤ 1.

theorem MIPRE.LIDT.Co.Preliminaries.opBounded01_hermitian {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {B : R} (hB : OpBounded01 B) : star B = B

Any OpBounded01 operator is self-adjoint.

theorem MIPRE.LIDT.Co.Preliminaries.leftTensor_opBounded01 {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {B : 𝔓} (hB : OpBounded01 B) : OpBounded01 (S.L B)

Left placement preserves the 0 ≤ B ≤ 1 bounds.