Section 12 pasting: switcheroo infrastructure

Initial switcheroo infrastructure and aggregate expansion helpers.

Switcheroo infrastructure

theorem MIPStarRE.LDT.Pasting.switcherooSelfConsistency_bip {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (M : IdxProjSubMeas (Fq params) Outcome ι) (omega : Error) (hselfM : SDDRel ψbi (uniformDistribution (SliceQuestion params)) (switcherooSelfConsistencyLeft params M) (switcherooSelfConsistencyRight params M) omega) : Preliminaries.BipartiteSDDRel ψbi (uniformDistribution (SliceQuestion params)) M.toIdxSubMeas M.toIdxSubMeas omega

Convert the one-question switcheroo self-consistency input into the bipartite form used by switchSandwich.

theorem MIPStarRE.LDT.Pasting.switcherooCompletePartSelfConsistency_pairBound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (zeta : Error) (hselfG : GCompleteSelfConsistencyStatement params ψbi family zeta) : (avgOver (uniformDistribution (SlicePairQuestion params)) fun (q : SlicePairQuestion params) => qSDDCore ψbi (fun (g : Polynomial params) => leftTensor ((family.meas q.1).outcome g)) fun (g : Polynomial params) => rightTensor ((family.meas q.1).outcome g)) ≤ zeta

Lift slicewise complete-part self-consistency to the slice-pair distribution.

This states the G^x self-consistency input in the form used by the switcheroo tensor-bound steps.

theorem MIPStarRE.LDT.Pasting.switcherooPointProductCommutation_coreBound {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (M : IdxProjSubMeas (Fq params) Outcome ι) (chi : Error) (hcomm : SDDOpRel ψbi (uniformDistribution (SlicePairQuestion params)) (switcherooPointProductLeft params family M) (switcherooPointProductRight params family M) chi) : (avgOver (uniformDistribution (SlicePairQuestion params)) fun (q : SlicePairQuestion params) => qSDDCore ψbi (fun (go : Polynomial params × Outcome) => (switcherooPointProductLeft params family M q).outcome go) fun (go : Polynomial params × Outcome) => (switcherooPointProductRight params family M q).outcome go) ≤ chi

Read the switcheroo point-product commutation hypothesis as an average qSDDCore bound.

theorem MIPStarRE.LDT.Pasting.avgOver_abs_le_avgOver_abs {α : Type u_2} (𝒟 : Distribution α) (f : α → Error) : |avgOver 𝒟 f| ≤ avgOver 𝒟 fun (a : α) => |f a|

theorem MIPStarRE.LDT.Pasting.projSubMeas_sandwich_sum_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (A : ProjSubMeas Outcome ι) (B : Quantum.Op ι) (hB : B ≤ 1) : ∑ a : Outcome, A.outcome a * B * A.outcome a ≤ 1

A projective sandwich family with middle operator bounded by 1 sums to at most 1.

theorem MIPStarRE.LDT.Pasting.projSubMeas_total_sq {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (P : ProjSubMeas Outcome ι) : P.total * P.total = P.total

The total operator of a projective submeasurement is idempotent.

theorem MIPStarRE.LDT.Pasting.switcherooAggregate_qSDDOp_expand {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (params : Parameters) [FieldModel params.q] (ψbi : QuantumState (ι × ι)) (family : IdxPolyFamily params ι) (M : IdxProjSubMeas (Fq params) Outcome ι) (q : SlicePairQuestion params) : qSDDOp ψbi (switcherooAggregateLeft params family M q) (switcherooAggregateRight params family M q) = ∑ o : Outcome, (ev ψbi (leftTensor ((M q.2).outcome o * (completePartSubMeas params family q.1).total * (M q.2).outcome o)) + ev ψbi (leftTensor ((completePartSubMeas params family q.1).total * (M q.2).outcome o * (completePartSubMeas params family q.1).total)) - ev ψbi (leftTensor ((M q.2).outcome o * (completePartSubMeas params family q.1).total * (M q.2).outcome o * (completePartSubMeas params family q.1).total)) - ev ψbi (leftTensor ((completePartSubMeas params family q.1).total * (M q.2).outcome o * (completePartSubMeas params family q.1).total * (M q.2).outcome o)))

Expand a single-question switcheroo qSDDOp term into its four scalar components.