Preliminary comparison theorems: completion and chain rules

Completion lemmas (prop:completing-to-measurement) and the chain inequalities for the operator-family distance (prop:triangle-inequality-for-approx_delta) from the preliminaries chapter. This is the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/CompletionTransfer.lean in the port of planning/c6b-plan.md (milestone M3, section "Port conventions").

The statements whose vendored state is on one space (closenessAfterCompletion_core_local, sddOpRel_triangle, sddOpRel_mono, questionSDDOp_chain, sddOpRel_chain) take a vector state V : VecState K and joint operators in K →L[ℂ] K; the bipartite ones (closenessAfterCompletion_core, completingToMeasurement) take a symmetric model S : SymModel 𝔓 K with local operators in 𝔓. Each takes the state as an explicit first argument in the namespace Preliminaries, as the vendored lemmas do.

The vendored hypotheses hψ : ψ.IsNormalized (of closenessAfterCompletion_core_local, closenessAfterCompletion_core and completingToMeasurement) and hperm : PermInvState ψ (of the last two) are dropped: normalization is V.ev_one_of_isNormalized, and swap symmetry enters through bipartiteSSC_implies_localSSC_liftLeft, which uses the model's S.ev_L_eq_ev_R.

The proof of closenessAfterCompletion_core_local bounds the two overlap gaps with question_overlap_gap_left and question_overlap_gap_right directly, where the vendored proof goes through easyApproxFromApproxDelta_twoFamily on constant families. In closenessAfterCompletion_core the completion of the left lift and the left lift of the completion have the same outcomes by map_add, map_sub and map_one of S.L, where the vendored proof compares Kronecker entries.

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/preliminaries.tex

theorem MIPRE.LIDT.Co.Preliminaries.closenessAfterCompletion_core_local {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_2} [Fintype Outcome] (V : VecState K) (A : Measurement Outcome (K →L[ℂ] K)) (B : SubMeas Outcome (K →L[ℂ] K)) (a0 : Outcome) (δ ζ : ℝ) : V.SSCRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily A.toSubMeas) ζ → V.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily A.toSubMeas) (constSubMeasFamily B) δ → V.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily A.toSubMeas) (constSubMeasFamily (completeAtOutcome B a0).toSubMeas) (2 * δ + 4 * √δ + 2 * ζ)

Local (single-register) version of the completion bound: if the measurement A is ζ-strongly self-consistent and δ-close to B, then A is (2δ + 4√δ + 2ζ)-close to the completion of B at a0. The vendored lemma asks for a normalized state.

theorem MIPRE.LIDT.Co.Preliminaries.sddOpRel_triangle {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A B C : IdxOpFamily Question Outcome (K →L[ℂ] K)) (δ₁ δ₂ : ℝ) : V.SDDOpRel 𝒟 A B δ₁ → V.SDDOpRel 𝒟 B C δ₂ → V.SDDOpRel 𝒟 A C (2 * (δ₁ + δ₂))

Triangle inequality for state-dependent operator distance.

theorem MIPRE.LIDT.Co.Preliminaries.sddOpRel_mono {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxOpFamily Question Outcome (K →L[ℂ] K)) (δ δ' : ℝ) : V.SDDOpRel 𝒟 A B δ → δ ≤ δ' → V.SDDOpRel 𝒟 A B δ'

Monotonicity for SDDOpRel.

theorem MIPRE.LIDT.Co.Preliminaries.questionSDDOp_chain {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_2} [Fintype Outcome] (V : VecState K) (n : ℕ) (families : Fin (n + 1) → OpFamily Outcome (K →L[ℂ] K)) : V.qSDDOp (families 0) (families (Fin.last n)) ≤ ↑n * ∑ i : Fin n, V.qSDDOp (families i.castSucc) (families i.succ)

Questionwise n-step chain bound: the squared distance between the first and last operator family telescopes and is bounded by n * ∑ individual squared distances via ev_sum_conjTranspose_mul_sum_le.

theorem MIPRE.LIDT.Co.Preliminaries.sddOpRel_chain {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (n : ℕ) (families : Fin (n + 1) → IdxOpFamily Question Outcome (K →L[ℂ] K)) (errors : Fin n → ℝ) (hsteps : ∀ (i : Fin n), V.SDDOpRel 𝒟 (families i.castSucc) (families i.succ) (errors i)) : V.SDDOpRel 𝒟 (families 0) (families (Fin.last n)) (↑n * ∑ i : Fin n, errors i)

n-step SDDOpRel chain lemma via vector Cauchy–Schwarz.

Given n consecutive SDDOpRel bounds, the endpoints satisfy an SDDOpRel bound with error n * (∑ individual errors). This improves on naive triangle-inequality chaining, which would give exponential blowup.

Paper reference: prop:triangle-inequality-for-approx_delta.

theorem MIPRE.LIDT.Co.Preliminaries.closenessAfterCompletion_core {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (S : SymModel 𝔓 K) (A : Measurement Outcome 𝔓) (B : SubMeas Outcome 𝔓) (a0 : Outcome) (δ ζ : ℝ) : S.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily A.toSubMeas) ζ → S.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (SubMeas.liftLeft S A.toSubMeas)) (constSubMeasFamily (SubMeas.liftLeft S B)) δ → S.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (SubMeas.liftLeft S A.toSubMeas)) (constSubMeasFamily (SubMeas.liftLeft S (completeAtOutcome B a0).toSubMeas)) (2 * δ + 4 * √δ + 2 * ζ)

Bipartite wrapper for the completion bound.

Bipartite strong self-consistency of A gives local strong self-consistency of its left lift (bipartiteSSC_implies_localSSC_liftLeft); closenessAfterCompletion_core_local, applied to the left-lifted measurement against the vector state of S, then bounds the distance to the completion of the lifted B, which has the same outcomes as the lift of the completion of B. The vendored lemma asks for a permutation-invariant, normalized state.

theorem MIPRE.LIDT.Co.Preliminaries.completingToMeasurement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (S : SymModel 𝔓 K) (A : Measurement Outcome 𝔓) (B : SubMeas Outcome 𝔓) (a0 : Outcome) (δ ζ : ℝ) : S.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily A.toSubMeas) ζ → S.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (SubMeas.liftLeft S A.toSubMeas)) (constSubMeasFamily (SubMeas.liftLeft S B)) δ → ∃ (C : Measurement Outcome 𝔓), C = completeAtOutcome B a0 ∧ CompletingToMeasStmt S A B C a0 δ ζ

prop:completing-to-measurement.

The completion completeAtOutcome B a0 of B is a measurement whose left lift is (2δ + 4√δ + 2ζ)-close to that of A. The vendored theorem asks for a permutation-invariant, normalized state.