Helper completeness: fiber operators and Cauchy--Schwarz bounds

This file introduces the fiber operator T_[h(u)=a] and proves the pointwise operator inequalities and averaged Cauchy--Schwarz estimates used in the two analytic moves of the helper-completeness proof.

References

• references/ldt-paper/self_improvement.tex lines 359--394
• blueprint/src/chapter/ch07_self_improvement.tex

noncomputable def MIPStarRE.LDT.SelfImprovement.helperFiberOperator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (T : SubMeas (Polynomial params) ι) (u : Point params) (a : Fq params) : Quantum.Op ι

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

• MIPStarRE.LDT.SelfImprovement.helperFiberOperator params T u a = ∑ h : MIPStarRE.LDT.Polynomial params with h.toFun u = a, T.outcome h

theorem MIPStarRE.LDT.SelfImprovement.helperFiberOperator_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (T : SubMeas (Polynomial params) ι) (u : Point params) (a : Fq params) : 0 ≤ helperFiberOperator params T u a

The helper fiber operator is positive.

theorem MIPStarRE.LDT.SelfImprovement.helperFiberOperator_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (T : SubMeas (Polynomial params) ι) (u : Point params) (a : Fq params) : helperFiberOperator params T u a ≤ 1

The helper fiber operator is bounded by the identity.

theorem MIPStarRE.LDT.SelfImprovement.helperFiberOperator_sum_eq_total {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (T : SubMeas (Polynomial params) ι) (u : Point params) : ∑ a : Fq params, helperFiberOperator params T u a = T.total

The fiber operators over all values at a fixed point sum to the total SDP submeasurement operator.

theorem MIPStarRE.LDT.SelfImprovement.helper_second_move_first_factor_operator_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (T : SubMeas (Polynomial params) ι) (u : Point params) : (∑ a : Fq params, have Tfiber := helperFiberOperator params T u a; leftTensor (Tfiber * Tfiber)) ≤ 1

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.

theorem MIPStarRE.LDT.SelfImprovement.helper_second_move_first_factor_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : (avgOver (uniformDistribution (Point params)) fun (u : Point params) => ∑ a : Fq params, have Tfiber := helperFiberOperator params T u a; ev strategy.state (leftTensor (Tfiber * Tfiber))) ≤ 1

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.

theorem MIPStarRE.LDT.SelfImprovement.helper_second_move_second_factor_pointwise_le_qBipartiteSSCDefect {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (u : Point params) : (∑ a : Fq params, have Au := (strategy.pointMeasurement u).outcome a; ev strategy.state (opTensor (Au * Au) ((1 - Au) * (1 - Au)))) ≤ qBipartiteSSCDefect strategy.state (strategy.pointMeasurement u).toSubMeas

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.

theorem MIPStarRE.LDT.SelfImprovement.helper_second_move_second_factor_le_delta {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (delta : Error) (hssc : BipartiteSSCRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas delta) : (avgOver (uniformDistribution (Point params)) fun (u : Point params) => ∑ a : Fq params, have Au := (strategy.pointMeasurement u).outcome a; ev strategy.state (opTensor (Au * Au) ((1 - Au) * (1 - Au)))) ≤ delta

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.

theorem MIPStarRE.LDT.SelfImprovement.helper_first_move_second_factor_operator_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (u : Point params) : (∑ a : Fq params, have Au := (strategy.pointMeasurement u).outcome a; have Tfiber := helperFiberOperator params T u a; leftTensor (Au * (Tfiber * Tfiber) * Au)) ≤ 1

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.

theorem MIPStarRE.LDT.SelfImprovement.helper_first_move_second_factor_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : (avgOver (uniformDistribution (Point params)) fun (u : Point params) => ∑ a : Fq params, have Au := (strategy.pointMeasurement u).outcome a; have Tfiber := helperFiberOperator params T u a; ev strategy.state (leftTensor (Au * (Tfiber * Tfiber) * Au))) ≤ 1

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.

noncomputable def MIPStarRE.LDT.SelfImprovement.helperFirstMovedCompletenessQuantity {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : Error

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.

noncomputable def MIPStarRE.LDT.SelfImprovement.helperLinearizedCompletenessQuantity {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : Error

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.

theorem MIPStarRE.LDT.SelfImprovement.helper_linearized_completeness_quantity_eq_fiber_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : helperLinearizedCompletenessQuantity params strategy T = avgOver (uniformDistribution (Point params)) fun (u : Point params) => ∑ a : Fq params, have Au := (strategy.pointMeasurement u).outcome a; have Tfiber := helperFiberOperator params T u a; ev strategy.state (leftTensor (Tfiber * Au))

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.

theorem MIPStarRE.LDT.SelfImprovement.helper_second_move_pointwise_abs_le_sqrt {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (u : Point params) (a : Fq params) : |ev strategy.state (opTensor (helperFiberOperator params T u a * (strategy.pointMeasurement u).outcome a) (1 - (strategy.pointMeasurement u).outcome a))| ≤ √(ev strategy.state (leftTensor (helperFiberOperator params T u a * helperFiberOperator params T u a))) * √(ev strategy.state (opTensor ((strategy.pointMeasurement u).outcome a * (strategy.pointMeasurement u).outcome a) ((1 - (strategy.pointMeasurement u).outcome a) * (1 - (strategy.pointMeasurement u).outcome a))))

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.

theorem MIPStarRE.LDT.SelfImprovement.helper_second_move_abs_sub_first_moved_le_sqrt_delta {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (delta : Error) (hssc : BipartiteSSCRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas delta) : |helperLinearizedCompletenessQuantity params strategy T - helperFirstMovedCompletenessQuantity params strategy T| ≤ √delta

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.