Preliminary definitions and statement structures

This file collects the lightweight statement and definition layer for the preliminaries chapter of the LDT development. It records the paper's consistency, sandwich, and completion statements in a form used by later files.

Main definitions

• BipartiteSDDRel: the paper-style left/right state-dependent distance relation.
• ConsAgreement: the measurement reformulation of consistency.
• ConsSubMeasStmt, SwitchSandwichStmt, CompTransferStmt, and CompletingToMeasStmt: conclusion statements for the main preliminary propositions.
• completeAtOutcome: completion of a submeasurement at a distinguished outcome.

References

• references/ldt-paper/preliminaries.tex

Consistency and distance statements

structure MIPStarRE.LDT.Preliminaries.BipartiteSDDRel {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A B : IdxSubMeas Question Outcome ι) (δ : Error) : Prop

Source-style left/right relation A^x_a ⊗ I ≈_δ I ⊗ B^x_a.

• leftRightSquaredDistanceBound : sddError ψ 𝒟 A.liftLeft B.liftRight ≤ δ

structure MIPStarRE.LDT.Preliminaries.OpBounded01 {ι : Type u_1} [Fintype ι] [DecidableEq ι] (B : Quantum.Op ι) : Prop

Condition 0 ≤ B ≤ I for the switch-sandwich argument.

• nonnegative : 0 ≤ B
• boundedByIdentity : 0 ≤ 1 - B

noncomputable def MIPStarRE.LDT.Preliminaries.agreementProbability {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A B : IdxMeas Question Outcome ι) : Error

Agreement probability from prop:simeq-for-measurements.

Equations

• MIPStarRE.LDT.Preliminaries.agreementProbability ψ 𝒟 A B = 1 - MIPStarRE.LDT.bipartiteConsError ψ 𝒟 A.toIdxSubMeas B.toIdxSubMeas

structure MIPStarRE.LDT.Preliminaries.ConsAgreement {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A B : IdxMeas Question Outcome ι) (δ : Error) : Prop

Conclusion statement for the measurement reformulation of consistency.

• agreementLowerBound : agreementProbability ψ 𝒟 A B ≥ 1 - δ

noncomputable def MIPStarRE.LDT.Preliminaries.diagonalSandwichFamily {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (A : IdxSubMeas Question Outcome ι) (B : IdxMeas Question Outcome ι) : IdxSubMeas Question Outcome (ι × ι)

A_a ⊗ B_a, the diagonal bipartite family from prop:cons-sub-meas.

This same-space version is the specialization used by the existing main-theorem path. The paper-facing two-space version is heterogeneousDiagonalSandwichFamily.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Preliminaries.totalSandwichFamily {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (A : IdxSubMeas Question Outcome ι) (B : IdxMeas Question Outcome ι) : IdxSubMeas Question Outcome (ι × ι)

A ⊗ B_a, the total bipartite family from prop:cons-sub-meas.

This same-space version is the specialization used by the existing main-theorem path. The paper-facing two-space version is heterogeneousTotalSandwichFamily.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Preliminaries.heterogeneousDiagonalSandwichFamily {Question : Type u_1} {Outcome : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (A : IdxSubMeas Question Outcome ιA) (B : IdxMeas Question Outcome ιB) : IdxSubMeas Question Outcome (ιA × ιB)

A_a ⊗ B_a for the two-space statement of prop:cons-sub-meas.

Here A acts on the left Hilbert space and B acts on the right Hilbert space; the resulting family acts on the tensor-product state space ιA × ιB.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Preliminaries.heterogeneousTotalSandwichFamily {Question : Type u_1} {Outcome : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (A : IdxSubMeas Question Outcome ιA) (B : IdxMeas Question Outcome ιB) : IdxSubMeas Question Outcome (ιA × ιB)

A ⊗ B_a for the two-space statement of prop:cons-sub-meas.

The total operator A^x = ∑_a A^x_a remains on the left tensor factor, while the measurement outcome B^x_a remains on the right tensor factor.

Equations

• One or more equations did not get rendered due to their size.

structure MIPStarRE.LDT.Preliminaries.ConsSubMeasStmt {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ι) (B : IdxMeas Question Outcome ι) (γ : Error) : Prop

Same-space output statement for prop:cons-sub-meas.

The paper-facing two-space output statement is ConsSubMeasHeterogeneousStmt.

• diagonalControl : SDDRel ψ 𝒟 A.liftLeft (diagonalSandwichFamily A B) γ
• sandwichControl : SDDRel ψ 𝒟 (diagonalSandwichFamily A B) (totalSandwichFamily A B) γ
• combinedControl : SDDRel ψ 𝒟 A.liftLeft (totalSandwichFamily A B) (4 * γ)

structure MIPStarRE.LDT.Preliminaries.ConsSubMeasHeterogeneousStmt {Question : Type u_1} {Outcome : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (ψ : QuantumState (ιA × ιB)) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ιA) (B : IdxMeas Question Outcome ιB) (γ : Error) : Prop

Two-space output statement for prop:cons-sub-meas.

It records the two estimates A^x_a ⊗ I ≈_γ A^x_a ⊗ B^x_a and A^x_a ⊗ B^x_a ≈_γ A^x ⊗ B^x_a, and the resulting 4γ estimate from A^x_a ⊗ I to A^x ⊗ B^x_a.

• diagonalControl : SDDRel ψ 𝒟 A.placeLeft (heterogeneousDiagonalSandwichFamily A B) γ

  A^x_a ⊗ I is close to the diagonal family A^x_a ⊗ B^x_a.

• sandwichControl : SDDRel ψ 𝒟 (heterogeneousDiagonalSandwichFamily A B) (heterogeneousTotalSandwichFamily A B) γ

  The diagonal family A^x_a ⊗ B^x_a is close to A^x ⊗ B^x_a.

• combinedControl : SDDRel ψ 𝒟 A.placeLeft (heterogeneousTotalSandwichFamily A B) (4 * γ)

  The two preceding estimates give A^x_a ⊗ I ≈_{4γ} A^x ⊗ B^x_a.

Sandwich expectations

noncomputable def MIPStarRE.LDT.Preliminaries.leftSandwichExpectation {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A : IdxProjSubMeas Question Outcome ι) (B : Quantum.Op ι) : Error

Averaged left term E_x ∑_a ⟨ψ, (A_a B A_a ⊗ I) ψ⟩.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Preliminaries.middleSandwichExpectation {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A : IdxProjSubMeas Question Outcome ι) (B : Quantum.Op ι) : Error

Averaged middle term E_x ∑_a ⟨ψ, (B ⊗ A_a) ψ⟩.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Preliminaries.rightSandwichExpectation {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A : IdxProjSubMeas Question Outcome ι) (B : Quantum.Op ι) : Error

Averaged right term E_x ∑_a ⟨ψ, (B A_a ⊗ I) ψ⟩.

Equations

• MIPStarRE.LDT.Preliminaries.rightSandwichExpectation ψ 𝒟 A B = MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, MIPStarRE.LDT.ev ψ (MIPStarRE.LDT.leftTensor (B * (A q).outcome a))

structure MIPStarRE.LDT.Preliminaries.SwitchSandwichStmt {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A : IdxProjSubMeas Question Outcome ι) (B : Quantum.Op ι) (δ : Error) : Prop

Conclusion statement for prop:switch-sandwich.

• leftSandwichTransfer : |leftSandwichExpectation ψ 𝒟 A B - middleSandwichExpectation ψ 𝒟 A B| ≤ 2 * √δ
• rightSandwichTransfer : |middleSandwichExpectation ψ 𝒟 A B - rightSandwichExpectation ψ 𝒟 A B| ≤ √δ

structure MIPStarRE.LDT.Preliminaries.CompTransferStmt {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ι) (P : IdxProjSubMeas Question Outcome ι) (ε : Error) : Prop

Conclusion statement for prop:completeness-transfer-projective-P.

• completenessTransfer : idxSubMeasMass ψ 𝒟 A ≥ idxSubMeasMass ψ 𝒟 P.toIdxSubMeas - 2 * √ε

Completion

noncomputable def MIPStarRE.LDT.Preliminaries.completeAtOutcome {Outcome : Type u_1} {ι : Type u_2} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (B : SubMeas Outcome ι) (a0 : Outcome) : Measurement Outcome ι

Canonical completion of B by adjoining the residual I - Σ_a B_a to the distinguished outcome a0.

Equations

• One or more equations did not get rendered due to their size.

structure MIPStarRE.LDT.Preliminaries.CompletingToMeasStmt {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (A : Measurement Outcome ι) (B : SubMeas Outcome ι) (C : Measurement Outcome ι) (a0 : Outcome) (δ ζ : Error) : Prop

Analytic conclusion for prop:completing-to-measurement once a witness C has been fixed.

The theorem completingToMeasurement separately records that the chosen witness is the canonical completion completeAtOutcome B a0, so this structure stores only the closeness statement from the paper.

• closenessAfterCompletion : SDDRel ψ (uniformDistribution Unit) (constSubMeasFamily A.liftLeft) (constSubMeasFamily C.liftLeft) (2 * δ + 4 * √δ + 2 * ζ)