Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.Pasting.ComparisonLemmas.LdSandwichLineOnePoint.CauchySchwarz

Section 12 pasting: line one-point transport — Cauchy-Schwarz chain #

Internal helper module; part of the file-split for #1127.

References #

source
theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_prefix_outcomeSum_cauchySchwarz_facts {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (gamma zeta : Error) {k i : ℕ} (hi : i < k) (hi0 : i ≠ 0) (facts : LdSandwichLineOnePointAdjointRawCoreBound params strategy family gamma zeta hi) :
LdSandwichLineOnePointCSFacts params strategy family gamma zeta hi

Assemble the line-one-point CS facts from the single adjoint raw-core estimate.

source
theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_prefix_outcomeSum_cauchySchwarz_abs_bounds {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (gamma zeta : Error) {k i : ℕ} (hi : i < k) (hi0 : i ≠ 0) (facts : LdSandwichLineOnePointAdjointRawCoreBound params strategy family gamma zeta hi) :
LdSandwichLineOnePointOutcomeSumCSAbsBounds params strategy family gamma zeta hi

Narrow analytic endpoint for the two off-diagonal Cauchy--Schwarz moves in their absolute-value closenessOfIP output shape.

The generic applications of Preliminaries.closenessOfIPAdjoint and Preliminaries.closenessOfIP are now proved here. The CS facts record proves the measurement-completeness/unit bounds and scalar regrouping equalities; the remaining nontrivial estimate is the adjoint raw-core orientation lemma ldSandwichLineOnePoint_prefix_outcomeSum_cauchySchwarz_adjointRawCore.

source
theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_prefix_outcomeSum_cauchySchwarz_route {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (gamma zeta : Error) {k i : ℕ} (hi : i < k) (hi0 : i ≠ 0) (facts : LdSandwichLineOnePointAdjointRawCoreBound params strategy family gamma zeta hi) :
LdSandwichLineOnePointOutcomeSumCSRoute params strategy family gamma zeta hi

One-sided route for the two off-diagonal Cauchy--Schwarz moves in ld-pasting.tex:964--1010.

The substantive analytic residual is the pair of absolute-value estimates ldSandwichLineOnePoint_prefix_outcomeSum_cauchySchwarz_abs_bounds; this lemma only converts those two closenessOfIP-style bounds into the one-sided inequalities consumed by the downstream scalar transport.

source
theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_prefix_outcomeSum_cauchySchwarz_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (gamma zeta : Error) {k i : ℕ} (hi : i < k) (hi0 : i ≠ 0) (facts : LdSandwichLineOnePointAdjointRawCoreBound params strategy family gamma zeta hi) :
(avgOver (uniformDistribution (SandwichedLineQuestion params k)) fun (q : SandwichedLineQuestion params k) => ∑ a : Fq params, ev strategy.state (opTensor ((ldSandwichLineOnePointPrefixOriginalFamily params family hi q).outcome (some a)) (1 - (ldSandwichLineOnePointRightFamily params strategy family k i q).outcome (some a)))) ≤ (avgOver (uniformDistribution (SandwichedLineQuestion params k)) fun (q : SandwichedLineQuestion params k) => ∑ a : Fq params, ev strategy.state (opTensor ((ldSandwichLineOnePointPrefixMovedFamily params family hi q).outcome (some a)) (1 - (ldSandwichLineOnePointRightFamily params strategy family k i q).outcome (some a)))) + 2 * √(commuteGHalfSandwichError params gamma zeta (i + 1))

The remaining expanded off-diagonal scalar transport in lem:ld-sandwich-line-one-point.

This is the exact scalar form of ld-pasting.tex:954--1024 after the linear consistency defect has been expanded as Σ_a ⟨ψ|A_a ⊗ (I - B_a)|ψ⟩. The only remaining analytic content is the paper's two averaged Cauchy--Schwarz moves plus the prefix-completeness collapse; the surrounding qBipartiteLinearConsDefect bookkeeping is proved in ldSandwichLineOnePoint_prefix_linearDefect_average_cauchySchwarz_bound.

source
theorem MIPStarRE.LDT.Pasting.ldSandwichLineOnePoint_prefix_linearDefect_average_cauchySchwarz_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (gamma zeta : Error) {k i : ℕ} (hi : i < k) (hi0 : i ≠ 0) (facts : LdSandwichLineOnePointAdjointRawCoreBound params strategy family gamma zeta hi) :
(avgOver (uniformDistribution (SandwichedLineQuestion params k)) fun (q : SandwichedLineQuestion params k) => qBipartiteLinearConsDefect strategy.state (ldSandwichLineOnePointPrefixOriginalFamily params family hi q) (ldSandwichLineOnePointRightFamily params strategy family k i q)) ≤ (avgOver (uniformDistribution (SandwichedLineQuestion params k)) fun (q : SandwichedLineQuestion params k) => qBipartiteLinearConsDefect strategy.state (ldSandwichLineOnePointPrefixMovedFamily params family hi q) (ldSandwichLineOnePointRightFamily params strategy family k i q)) + 2 * √(commuteGHalfSandwichError params gamma zeta (i + 1))

Linear-defect reduction for the expanded off-diagonal post-deletion transport in lem:ld-sandwich-line-one-point.

The paper's two Cauchy--Schwarz moves and prefix collapse from references/ldt-paper/ld-pasting.tex:954--1024 act on the expanded scalar expression Σ_a ⟨ψ|A_a ⊗ (I - B_a)|ψ⟩. This lemma proves the exact bookkeeping reduction from the averaged linear consistency defects to that expanded residual, using the measurement-valued right family and the fact that both option-valued families have zero none mass. The remaining analytic gap is therefore the split Cauchy--Schwarz route ldSandwichLineOnePoint_prefix_outcomeSum_cauchySchwarz_route; the arithmetic absorption into ν₅ is proved separately in ldSandwichLineOnePoint_endpoint_comm_error_le.