Section 12 pasting: from-H-to-G move lemmas

Tensor, positivity, and Cauchy--Schwarz helper lemmas for the adjacent paper chain.

theorem MIPStarRE.LDT.Pasting.abs_sub_le_four (a b c d e : Error) : |a - e| ≤ |a - b| + |b - c| + |c - d| + |d - e|

theorem MIPStarRE.LDT.Pasting.commuteGHalfSandwichError_mono_length (params : Parameters) (gamma zeta : Error) (hgamma_nonneg : 0 ≤ gamma) (hzeta_nonneg : 0 ≤ zeta) {j k : ℕ} (hjk : j ≤ k) : commuteGHalfSandwichError params gamma zeta j ≤ commuteGHalfSandwichError params gamma zeta k

The displayed half-sandwich commutation error is monotone in the sandwich length.

theorem MIPStarRE.LDT.Pasting.fromHToG_qSDDCore_symm {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Outcome : Type u_2} [Fintype Outcome] (ψ : QuantumState ι) (A B : Outcome → Quantum.Op ι) : qSDDCore ψ A B = qSDDCore ψ B A

Symmetry of the raw pointwise state-dependent distance core. This local form is useful when orienting adjoint half-sandwich commutators for the second paper commutation step.

theorem MIPStarRE.LDT.Pasting.fromHToG_ev_leftTensor_rightTensor_mono_right_of_nonneg_left {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψbi : QuantumState (ι × ι)) {A B C : Quantum.Op ι} (hA : 0 ≤ A) (hBC : B ≤ C) : ev ψbi (leftTensor A * rightTensor B) ≤ ev ψbi (leftTensor A * rightTensor C)

If A is PSD and B ≤ C, then the corresponding bipartite scalar expectations with left/right tensor placement are monotone in the right factor.

theorem MIPStarRE.LDT.Pasting.psd_contraction_comm_sandwich_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S B : Quantum.Op ι} (hS0 : 0 ≤ S) (hS1 : S ≤ 1) (hB0 : 0 ≤ B) (hSB : Commute S B) : S * B * S ≤ B

If S is a PSD contraction commuting with B, then S * B * S ≤ B. This formalizes the paper's eq:S-sandwich domination step without using explicit square roots.

theorem MIPStarRE.LDT.Pasting.fromHToGRecurrenceWeight_sandwich_base_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (prefixLen : ℕ) {tailLen : ℕ} (τtail : GHatType tailLen) : have S := fromHToGRecurrenceWeight params family prefixLen τtail; S * family.averagedSubMeas.total * S ≤ family.averagedSubMeas.total

Paper eq:S-sandwich for the complete branch average G.

theorem MIPStarRE.LDT.Pasting.fromHToGRecurrenceWeight_sandwich_one_sub_base_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (prefixLen : ℕ) {tailLen : ℕ} (τtail : GHatType tailLen) : have S := fromHToGRecurrenceWeight params family prefixLen τtail; S * (1 - family.averagedSubMeas.total) * S ≤ 1 - family.averagedSubMeas.total

Paper eq:S-sandwich for the incomplete branch average I - G.

theorem MIPStarRE.LDT.Pasting.fromHToG_gHatIdxMeas_outcome_isHermitian {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (x : Fq params) (g : GHatOutcome params) : Matrix.conjTranspose ((gHatIdxMeas params family x).outcome g) = (gHatIdxMeas params family x).outcome g

Completed ĝ measurement outcomes are Hermitian. This records the positivity-to-Hermitian conversion used when orienting the adjoint half-sandwich commutator in the M₂ → M₃ move.

theorem MIPStarRE.LDT.Pasting.fromHToG_gHatReverseHalfProductOutcomeOperator_eq_adjoint {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (n : ℕ) (xs : PointTuple params n) (gs : GHatTupleOutcome params n) : gHatReverseHalfProductOutcomeOperator params family n xs gs = Matrix.conjTranspose (gHatHalfProductOutcomeOperator params family n xs gs)

The reverse half-product is the adjoint of the ordered half-product.

def MIPStarRE.LDT.Pasting.fromHToGPointTupleReverseEquiv (params : Parameters) (n : ℕ) : PointTuple params n ≃ PointTuple params n

Reverse a tuple of slice questions.

Equations

• One or more equations did not get rendered due to their size.

def MIPStarRE.LDT.Pasting.fromHToGGHatTupleOutcomeReverseEquiv (params : Parameters) [FieldModel params.q] (n : ℕ) : GHatTupleOutcome params n ≃ GHatTupleOutcome params n

Reverse a tuple of completed-slice outcomes.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.Pasting.fromHToG_pointTupleTail_snoc (params : Parameters) {n : ℕ} (xs : PointTuple params (n + 1)) (x : Fq params) : pointTupleTail (Fin.snoc xs x) = Fin.snoc (pointTupleTail xs) x

Tail of a snoc tuple.

theorem MIPStarRE.LDT.Pasting.fromHToG_gHatTupleOutcomeTail_snoc (params : Parameters) [FieldModel params.q] {n : ℕ} (gs : GHatTupleOutcome params (n + 1)) (g : GHatOutcome params) : gHatTupleOutcomeTail (Fin.snoc gs g) = Fin.snoc (gHatTupleOutcomeTail gs) g

Tail of a snoc completed-outcome tuple.

theorem MIPStarRE.LDT.Pasting.fromHToG_gHatHalfProductOutcomeOperator_snoc {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (n : ℕ) (xs : PointTuple params n) (x : Fq params) (gs : GHatTupleOutcome params n) (g : GHatOutcome params) : gHatHalfProductOutcomeOperator params family (n + 1) (Fin.snoc xs x) (Fin.snoc gs g) = gHatHalfProductOutcomeOperator params family n xs gs * (gHatIdxMeas params family x).outcome g

Ordered half-products satisfy a snoc recursion.

theorem MIPStarRE.LDT.Pasting.fromHToG_gHatHalfProduct_reverse_eq_adjoint {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (n : ℕ) (xs : PointTuple params n) (gs : GHatTupleOutcome params n) : gHatHalfProductOutcomeOperator params family n ((fromHToGPointTupleReverseEquiv params n) xs) ((fromHToGGHatTupleOutcomeReverseEquiv params n) gs) = Matrix.conjTranspose (gHatHalfProductOutcomeOperator params family n xs gs)

Reversing a tuple turns the ordered half-product into its adjoint.

theorem MIPStarRE.LDT.Pasting.fromHToG_sum_product {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (F : α → β → Error) : ∑ a : α, ∑ b : β, F a b = ∑ p : α × β, F p.1 p.2

Rewrite a nested finite sum as a sum over a product index.

theorem MIPStarRE.LDT.Pasting.fromHToG_avgOver_sub {Question : Type u_2} (𝒟 : Distribution Question) (f g : Question → Error) : avgOver 𝒟 f - avgOver 𝒟 g = avgOver 𝒟 fun (q : Question) => f q - g q

theorem MIPStarRE.LDT.Pasting.fromHToG_closenessOfIP_avgContext {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Question : Type u_2} {OutcomeA : Type u_3} {OutcomeB : Type u_4} [Fintype OutcomeA] [Fintype OutcomeB] (ψ : QuantumState (ι × ι)) (_hψ : ψ.IsNormalized) (𝒟 : Distribution Question) (_h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B : Question → OutcomeA → Quantum.Op (ι × ι)) (C : Question → OutcomeA → OutcomeB → Quantum.Op (ι × ι)) (γ : Error) (hAB : (avgOver 𝒟 fun (q : Question) => qSDDCore ψ (A q) (B q)) ≤ γ) (hC : (avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ev ψ ((∑ b : OutcomeB, C q a b) * (∑ b : OutcomeB, C q a b).conjTranspose)) ≤ 1) : |(avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, ev ψ (C q a b * A q a)) - avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, ev ψ (C q a b * B q a)| ≤ √γ

Averaged-context variant of closenessOfIP: the contraction side condition is only required after averaging over the question distribution.

theorem MIPStarRE.LDT.Pasting.fromHToG_type_filtered_outcome_sum (params : Parameters) [FieldModel params.q] {n : ℕ} {R : Type u_2} [AddCommMonoid R] (F : GHatType n → GHatTupleOutcome params n → R) : ∑ τ : GHatType n, ∑ gs : GHatTupleOutcome params n with gHatTupleType gs = τ, F τ gs = ∑ gs : GHatTupleOutcome params n, F (gHatTupleType gs) gs

Collapse a type-filtered completed-outcome sum to an unfiltered sum.

theorem MIPStarRE.LDT.Pasting.fromHToG_bool_type_filtered_outcome_sum (params : Parameters) [FieldModel params.q] {n : ℕ} (F : Bool → GHatType n → GHatOutcome params → GHatTupleOutcome params n → Error) : ∑ b : Bool, ∑ τ : GHatType n, ∑ g : GHatOutcome params with Option.isSome g = b, ∑ gs : GHatTupleOutcome params n with gHatTupleType gs = τ, F b τ g gs = ∑ g : GHatOutcome params, ∑ gs : GHatTupleOutcome params n, F (Option.isSome g) (gHatTupleType gs) g gs

Collapse the paper's Boolean/type-filtered outcome sum to an unfiltered outcome sum, choosing the Boolean and type from the outcomes themselves.

theorem MIPStarRE.LDT.Pasting.fromHToG_sum₂_avgOver₂ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Fintype γ] [Fintype δ] (𝒟α : Distribution α) (𝒟β : Distribution β) (F : γ → δ → α → β → Error) : (∑ c : γ, ∑ d : δ, avgOver 𝒟α fun (a : α) => avgOver 𝒟β fun (b : β) => F c d a b) = avgOver 𝒟α fun (a : α) => avgOver 𝒟β fun (b : β) => ∑ c : γ, ∑ d : δ, F c d a b

Move two finite sums through two nested averages.