Preliminary comparison theorems: consistency-to-distance estimates

Estimates converting consistency of a submeasurement and a measurement into state-dependent distance controls for the diagonal and total sandwich families of prop:cons-sub-meas: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/ConsistencyBridges.lean in the port of planning/c6b-plan.md (milestone M3, section "Port conventions").

As in Co/Preliminaries/Defs.lean, the declarations live in MIPRE.LIDT.Co.Preliminaries and take the state as an ordinary explicit argument in place of the vendored state ψ. The pointwise comparison consSubMeas_controlHelper is about joint operators on a single space, so it takes a vector state V : VecState K (a symmetric model is accepted through its coercion); the consistency statements are bipartite and take S : SymModel 𝔓 K.

In both sandwich estimates the difference X a of the two families is a product placement S.opTensor C D with 0 ≤ C ≤ 1 and 0 ≤ D ≤ 1 (A_a ⊗ (I - B_a), resp. (A - A_a) ⊗ B_a), so 0 ≤ X a ≤ 1, hence X a * X a ≤ X a (sq_le_self), and the sum of ev (X a) is the consistency defect. The vendored proofs obtain star (X a) = X a from positive semidefiniteness of matrices; here it is IsSelfAdjoint.of_nonneg.

In the symmetric model both tensor factors are 𝔓, the general placements IdxSubMeas.placeLeft, placeRight are the lifts liftLeft, liftRight, and the two-space sandwich families are the same-space ones, all by rfl (Co/Basic/SubMeasurementFamilies.lean, Co/Preliminaries/Defs.lean). So the _heterogeneous statements are the same-space ones, and their proofs are the same-space proofs.

Not ported

Every declaration of the vendored file has a counterpart here.

Consistency controls for prop:cons-sub-meas

theorem MIPRE.LIDT.Co.Preliminaries.consSubMeas_controlHelper {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (V : VecState K) (P Q M N : SubMeas Outcome (K →L[ℂ] K)) (X : Outcome → K →L[ℂ] K) (hSq : ∀ (a : Outcome), V.ev (star (M.outcome a - N.outcome a) * (M.outcome a - N.outcome a)) = V.ev (X a * X a)) (hX_nonneg : ∀ (a : Outcome), 0 ≤ X a) (hX_le_one : ∀ (a : Outcome), X a ≤ 1) (hSum : ∑ a : Outcome, V.ev (X a) = V.ev (P.total * Q.total) - V.qMatchMass P Q) : V.qSDD M N ≤ V.qConsDefect P Q

Pointwise comparison behind prop:cons-sub-meas: if each squared difference (M_a - N_a)* (M_a - N_a) has the expectation of X_a * X_a for some 0 ≤ X_a ≤ 1, and the X_a account exactly for the off-diagonal mass of P and Q, then the squared distance of M and N is at most the consistency defect of P and Q.

theorem MIPRE.LIDT.Co.Preliminaries.consSubMeas_diagonalControl {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome 𝔓) (B : IdxMeas Question Outcome 𝔓) (γ : ℝ) : S.ConsRel 𝒟 A B.toIdxSubMeas γ → S.SDDRel 𝒟 (IdxSubMeas.liftLeft S A) (diagonalSandwichFamily S A B) γ

prop:cons-sub-meas, first estimate: if A is consistent with the measurement B, then A^x_a ⊗ I ≈_γ A^x_a ⊗ B^x_a.

theorem MIPRE.LIDT.Co.Preliminaries.consSubMeas_sandwichControl {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome 𝔓) (B : IdxMeas Question Outcome 𝔓) (γ : ℝ) : S.ConsRel 𝒟 A B.toIdxSubMeas γ → S.SDDRel 𝒟 (diagonalSandwichFamily S A B) (totalSandwichFamily S A B) γ

prop:cons-sub-meas, second estimate: if A is consistent with the measurement B, then A^x_a ⊗ B^x_a ≈_γ A^x ⊗ B^x_a.

theorem MIPRE.LIDT.Co.Preliminaries.consSubMeas_diagonalControl_heterogeneous {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome 𝔓) (B : IdxMeas Question Outcome 𝔓) (γ : ℝ) : S.ConsRel 𝒟 A B.toIdxSubMeas γ → S.SDDRel 𝒟 (IdxSubMeas.placeLeft S A) (heterogeneousDiagonalSandwichFamily S A B) γ

prop:cons-sub-meas, first estimate, in the two-space form: A^x_a ⊗ I ≈_γ A^x_a ⊗ B^x_a. In the symmetric model this is consSubMeas_diagonalControl.

theorem MIPRE.LIDT.Co.Preliminaries.consSubMeas_sandwichControl_heterogeneous {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome 𝔓) (B : IdxMeas Question Outcome 𝔓) (γ : ℝ) : S.ConsRel 𝒟 A B.toIdxSubMeas γ → S.SDDRel 𝒟 (heterogeneousDiagonalSandwichFamily S A B) (heterogeneousTotalSandwichFamily S A B) γ

prop:cons-sub-meas, second estimate, in the two-space form: A^x_a ⊗ B^x_a ≈_γ A^x ⊗ B^x_a. In the symmetric model this is consSubMeas_sandwichControl.

theorem MIPRE.LIDT.Co.Preliminaries.consSubMeas_heterogeneous {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome 𝔓) (B : IdxMeas Question Outcome 𝔓) (γ : ℝ) : S.ConsRel 𝒟 A B.toIdxSubMeas γ → ConsSubMeasHeterogeneousStmt S 𝒟 A B γ

prop:cons-sub-meas, in the two-space form stated in references/ldt-paper/preliminaries.tex lines 708--744 (upstream LionSR/MIPStarRE).

theorem MIPRE.LIDT.Co.Preliminaries.consSubMeas {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome 𝔓) (B : IdxMeas Question Outcome 𝔓) (γ : ℝ) : S.ConsRel 𝒟 A B.toIdxSubMeas γ → ConsSubMeasStmt S 𝒟 A B γ

Same-space specialization of prop:cons-sub-meas.

The paper-facing two-space theorem is consSubMeas_heterogeneous.