Triangle inequalities for state-dependent distance: core #
The main triangle-substitution estimates for approximate measurements: the counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/Triangles/Core.lean in the port of
planning/c6b-plan.md (milestone M3, section "Port conventions").
The same-space statements (qSDD_symm, sddRel_symm, triangleInequalityForVectorsSquared,
subMeas_total_ev_gap_abs_le_sqrt_card_qSDD, right_match_gap_abs_le_sqrt_qSDD) take a vector
state V : VecState K (a symmetric model is accepted through its coercion) and joint operators
in K βL[β] K. The substitution theorems triangleSub* are about the bipartite relation
S.ConsRel, so they take the symmetric model S : SymModel π K as an ordinary explicit argument
in place of the vendored state, with local families in π, as in Co/Preliminaries/Defs.lean.
Every statement drops the vendored normalization hypothesis hΟ : Ο.IsNormalized, a theorem of
the vector state (V.ev_one_of_isNormalized).
triangleSub_heterogeneous and triangleSub_right_heterogeneous are the vendored statements
with both tensor factors fixed to π (the vendored ones allow two carriers ΞΉA, ΞΉB); in the
symmetric model the placements IdxSubMeas.placeLeft S, IdxSubMeas.placeRight S are the lifts
IdxSubMeas.liftLeft S, IdxSubMeas.liftRight S by rfl
(Co/Basic/SubMeasurementFamilies.lean), so they are the same-space theorems. Their vendored
callers, on the two-space ProjStrat of Test/MainTheorem/SourceRoleRegister, are left to M13
and M14 (planning/c6b-plan.md, "Same-space and bipartite quantities").
The vendored file proves each of its four substitution theorems in full, with the same
pointwise estimate on max 0 (total - match) and the same averaging. Here that argument is
proved once, as consRel_of_matchGap, and each theorem supplies the match-mass gap (by
question_easyApproxFromApproxDelta of Co/Preliminaries/CauchySchwarz.lean on the left, by
right_match_gap_abs_le_sqrt_qSDD on the right) and the change of the total overlap (zero for
measurements). triangleSub_right is triangleSub_right_subMeas_total_le, the totals of
measurements being the identity.
New here #
consRel_of_matchGap: the common substitution step. IfS.ConsRel π A B Ξ΄, the matching masses of(A, B)and(A', B')differ by at mostβ(s q)at each question, withπΌ s β€ Ξ΅, and the total overlap of(A', B')exceeds that of(A, B)by at moste q, withπΌ e β€ Ξ·, thenS.ConsRel π A' B' (Ξ΄ + βΞ΅ + Ξ·).
Not ported #
max_zero_add_le: classical, imported.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/preliminaries.tex
Upstream keeps this helper private since its Lean-module port (LionSR/MIPStarRE at
5fc363b); the port carries its own copy, with upstream's proof.
Symmetry of the question-level state-dependent distance.
Symmetry of the state-dependent distance relation.
prop:triangle-inequality-for-vectors-squared.
For a finite family of operators Dα΅’, the squared norm of the summed vector
(βα΅’ Dα΅’) Ο is controlled by the cardinality times the sum of the squared norms
of the individual vectors Dα΅’ Ο.
The expectation of the difference of two submeasurement totals is controlled by the state-dependent distance between the two outcome families, with the finite-outcome Cauchy--Schwarz loss.
This is the total-operator analogue of the matching-mass estimates used in
triangleSub. It is useful precisely when the right-register families are
submeasurements rather than measurements, so that their total operators need
not be the identity.
Right-register matching gap: |β_a ev (A_a B_a) - β_a ev (A_a D_a)| β€ β(qSDD B D) for
submeasurements A, B, D.
The common substitution step of the triangleSub family. If S.ConsRel π A B Ξ΄, the
matching masses of (A, B) and (A', B') differ by at most β(s q) at each question, and the
total overlap of (A', B') exceeds that of (A, B) by at most e q, then
S.ConsRel π A' B' (Ξ΄ + βΞ΅ + Ξ·) for πΌ s β€ Ξ΅ and πΌ e β€ Ξ·.
prop:triangle-sub.
Both consistency errors are max 0 (ev (I β C.total) - Ξ£β ev (...)); the overlap difference is
bounded by CauchyβSchwarz (question_easyApproxFromApproxDelta) and averaged
(consRel_of_matchGap).
Heterogeneous left-register substitution.
The vendored statement places the two left families on H_A and the right family on H_B; in
the symmetric model these placements are the lifts, and this is triangleSub.
Right-register variants of triangleSub #
Right-register substitution for submeasurements when the right total overlap is monotone in the replacement direction.
The general submeasurement form triangleSub_right_subMeas_totalGap includes
the absolute displacement of the total-overlap term. In the special case where
the new right family has no larger total overlap with the fixed left family,
this displacement is not needed: increasing the total is the only way in which
the total term can worsen the consistency defect. The remaining contribution
is exactly the usual matching-mass Cauchy--Schwarz term.
Right-register substitution: triangleSub with the measurement replaced on the second
factor.
Heterogeneous right-register substitution.
The vendored statement places the left family on H_A and the two right families on H_B; in
the symmetric model these placements are the lifts, and this is triangleSub_right.
Right-register substitution for submeasurements, with the total-overlap displacement stated explicitly.
For complete right-register measurements the total-overlap term
ev Ο (A_total β B_total) is independent of the right family. For general
submeasurements this term may change. The lemma therefore separates the usual
state-dependent-distance contribution from the averaged displacement of the
right total operator.