Helper completeness: fiber operators and Cauchy--Schwarz bounds #
The fiber operator T_[h(u)=a] of the helper-completeness proof, the pointwise operator
inequalities and the averaged Cauchy--Schwarz estimates of its two analytic moves: the
counterpart of the vendored
SelfImprovement/Theorems/Results/HelperCompleteness/FiberBounds.lean (under
MIPRE/Background/LIDT/MIPStarRE/LDT/) in the port of planning/c6b-plan.md (milestone M10,
section "Port conventions").
A strategy is a SymStrat params 𝔓 K. The fiber operator and its bounds live in the local
algebra 𝔓, where their positivity is proved; the joint operators are strategy.state.L,
strategy.state.opTensor in K →L[ℂ] K.
helper_second_move_first_factor_operator_le_oneplaces without a strategy, so it takes the model(S : SymModel 𝔓 K)as an explicit first argument, as M6's placement lemmas do.- The vendored
ev_one_of_isNormalized strategy.state strategy.isNormalizedisstrategy.state.ev_one_of_isNormalized, a theorem of the model. - The vendored entrywise
kronecker_sub_rightsteps aremul_subwith the keystone'srightTensor_subandrightTensor_one, and the adjoint computations of the Cauchy--Schwarz step are the keystone'sconjTranspose_opTensor,opTensor_mul,leftTensor_mul_opTensorandleftTensor_mul_leftTensor; theMatrix.PosSemidefself-adjointness arguments areIsSelfAdjoint.of_nonneg.
The vendored file imports Basic/ParametersFiniteAnswers.lean (for polynomial_sum_fiberwise)
and SelfImprovement/Theorems/Thresholds/Final.lean, both classical and without a Co file; so
does this one.
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/self_improvement.texlines 359--394blueprint/src/chapter/ch07_self_improvement.tex
The fiber operator T_[h(u)=a] in the helper-completeness proof.
It is the sum of all SDP-measurement outcomes indexed by polynomials whose
value at the point u is a.
Equations
- MIPRE.LIDT.Co.SelfImprovement.helperFiberOperator params T u a = ∑ h : MIPStarRE.LDT.Polynomial params with h.toFun u = a, T.outcome h
Instances For
The helper fiber operator is positive.
The helper fiber operator is bounded by the identity.
The fiber operators over all values at a fixed point sum to the total SDP submeasurement operator.
Pointwise operator form of the identity bound for the first Cauchy--Schwarz factor in the second helper-completeness move.
At a fixed point u, the fiber operators form a submeasurement after grouping
by the value h(u). Thus Σ_a T_[h(u)=a]^2 ≤ Σ_a T_[h(u)=a] = T.total ≤ I.
The first Cauchy--Schwarz factor in the second helper-completeness move is bounded by one.
This is the Lean form of the paper's assertion, following
eq:mysterious-case-of-the-disappearing-a, that
E_u Σ_a ⟨ψ, T_[h(u)=a]^2 ⊗ I ψ⟩ ≤ 1.
Pointwise comparison between the projective residual in the second Cauchy--Schwarz move and the bipartite strong self-consistency defect.
Projectivity gives (A^u_a)^2 = A^u_a and (I - A^u_a)^2 = I - A^u_a.
After summing over a, the residual is the one-register total mass minus the
diagonal cross-register overlap, and hence is bounded by the max 0 defining
qBipartiteSSCDefect.
The second Cauchy--Schwarz factor in the second helper-completeness move is bounded by the bipartite strong self-consistency error.
This is the Lean form of the paper's assertion that
E_u Σ_a ⟨ψ, A^u_a ⊗ (I-A^u_a) ψ⟩ ≤ delta.
Pointwise operator form of the identity bound for the second Cauchy--Schwarz factor in the first helper-completeness move.
For a fixed point u, each fiber operator satisfies
0 ≤ T_[h(u)=a] ≤ I, hence T_[h(u)=a]^2 ≤ I. Sandwiching by the
projection A^u_a gives
A^u_a T_[h(u)=a]^2 A^u_a ≤ A^u_a, and the projective measurement
A^u sums to the identity.
The second Cauchy--Schwarz factor in the first helper-completeness move is bounded by the identity contribution.
This is the Lean form of the paper's assertion, following
eq:yet-another-move-a, that
E_u Σ_a ⟨ψ, (A^u_a T_[h(u)=a]^2 A^u_a) ⊗ I ψ⟩ ≤ 1.
The scalar expression after the first Cauchy--Schwarz move in helper completeness.
This is
E_u Σ_a ⟨ψ, (T_[h(u)=a] A^u_a) ⊗ A^u_a ψ⟩, the right-hand side of
eq:yet-another-move-a in the paper. The fiber
T_[h(u)=a] is represented by the finite sum over polynomials whose value at
u is a.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The scalar expression after removing the remaining point-measurement operator in helper completeness.
This is
E_u Σ_h ⟨ψ, (T_h A^u_{h(u)}) ⊗ I ψ⟩. Complementary slackness identifies this
quantity with the dual mass ⟨ψ, Z ⊗ I ψ⟩.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Fiberwise form of the linearized helper-completeness quantity.
The expression
E_u Σ_h ⟨ψ, (T_h A^u_{h(u)}) ⊗ I ψ⟩ may equivalently be grouped by the value
a = h(u), giving
E_u Σ_a ⟨ψ, (T_[h(u)=a] A^u_a) ⊗ I ψ⟩. This is the algebraic rewrite used
after eq:mysterious-case-of-the-disappearing-a in the paper.
Pointwise Cauchy--Schwarz estimate for the second helper-completeness move.
For fixed u and a, this bounds the residual term
⟨ψ, (T_[h(u)=a] A^u_a) ⊗ (I - A^u_a) ψ⟩ by the product of the two square-root
factors appearing after eq:mysterious-case-of-the-disappearing-a.
The second Cauchy--Schwarz move in the helper-completeness proof.
Assuming bipartite strong self-consistency of the point measurement with error
delta, the first-moved helper-completeness expression
E_u Σ_a ⟨ψ, (T_[h(u)=a] A^u_a) ⊗ A^u_a ψ⟩ differs from the linearized
expression E_u Σ_a ⟨ψ, (T_[h(u)=a] A^u_a) ⊗ I ψ⟩ by at most sqrt delta.
The first factor is bounded by the grouped submeasurement estimate, and the
second is exactly the projective residual controlled by self-consistency.