Tensor-placement helper lemmas and sandwich tensor estimates

Tensor-sum commutation, positivity/boundedness preservation, factoring lemmas, and sandwich-residual estimates used in the main induction step and polynomial-agreement arguments.

Tensor-placement helper lemmas

theorem MIPStarRE.LDT.leftTensor_finset_sum {α : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (s : Finset α) (f : α → Quantum.Op ι₁) : ∑ a ∈ s, leftTensor (f a) = leftTensor (s.sum f)

Left tensor placement commutes with finite sums.

theorem MIPStarRE.LDT.leftTensor_averageOperatorOverDistribution {α : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (𝒟 : Distribution α) (A : α → Quantum.Op ι₁) : leftTensor (averageOperatorOverDistribution 𝒟 A) = averageOperatorOverDistribution 𝒟 fun (a : α) => leftTensor (A a)

Left tensor placement commutes with operator averages.

theorem MIPStarRE.LDT.ev_leftTensor_total_eq_sum_outcome {α : Type u_1} [Fintype α] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) (A : SubMeas α ι) : ev ψ (leftTensor A.total) = ∑ a : α, ev ψ (leftTensor (A.outcome a))

Expanding the left-tensor mass of a submeasurement on a bipartite state as the sum of per-outcome left-tensor expectations.

This is a generic identity at the level of ev ψ (leftTensor _): applying SubMeas.sum_eq_total, pulling leftTensor through the finite sum via leftTensor_finset_sum, and distributing ev through the sum via ev_finset_sum. Using the definitional equalities subMeasMass ψ A.liftLeft = ev ψ A.liftLeft.total = ev ψ (leftTensor A.total), this immediately yields the helper-stage opening subMeasMass ψ A.liftLeft = ∑ a, ev ψ (leftTensor (A.outcome a)) used in the Section 9 / Section 12 calculations.

theorem MIPStarRE.LDT.ev_leftTensor_averageOperatorOverDistribution {α : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (ψ : QuantumState (ι₁ × ι₂)) (𝒟 : Distribution α) (A : α → Quantum.Op ι₁) : ev ψ (leftTensor (averageOperatorOverDistribution 𝒟 A)) = avgOver 𝒟 fun (a : α) => ev ψ (leftTensor (A a))

Evaluation of a left-placed operator average is the average of the left-placed evaluations.

theorem MIPStarRE.LDT.rightTensor_finset_sum {α : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (s : Finset α) (f : α → Quantum.Op ι₂) : ∑ a ∈ s, rightTensor (f a) = rightTensor (s.sum f)

Right tensor placement commutes with finite sums.

theorem MIPStarRE.LDT.rightTensor_averageOperatorOverDistribution {α : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (𝒟 : Distribution α) (A : α → Quantum.Op ι₂) : rightTensor (averageOperatorOverDistribution 𝒟 A) = averageOperatorOverDistribution 𝒟 fun (a : α) => rightTensor (A a)

Right tensor placement commutes with operator averages.

theorem MIPStarRE.LDT.ev_rightTensor_averageOperatorOverDistribution {α : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (ψ : QuantumState (ι₁ × ι₂)) (𝒟 : Distribution α) (A : α → Quantum.Op ι₂) : ev ψ (rightTensor (averageOperatorOverDistribution 𝒟 A)) = avgOver 𝒟 fun (a : α) => ev ψ (rightTensor (A a))

Evaluation of a right-placed operator average is the average of the right-placed evaluations.

theorem MIPStarRE.LDT.opTensor_averageOperatorOverDistribution_left {α : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (𝒟 : Distribution α) (A : α → Quantum.Op ι₁) (B : Quantum.Op ι₂) : opTensor (averageOperatorOverDistribution 𝒟 A) B = averageOperatorOverDistribution 𝒟 fun (a : α) => opTensor (A a) B

Tensoring on the right commutes with operator averages in the left factor.

theorem MIPStarRE.LDT.opTensor_averageOperatorOverDistribution_right {α : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (𝒟 : Distribution α) (A : Quantum.Op ι₁) (B : α → Quantum.Op ι₂) : opTensor A (averageOperatorOverDistribution 𝒟 B) = averageOperatorOverDistribution 𝒟 fun (a : α) => opTensor A (B a)

Tensoring on the left commutes with operator averages in the right factor.

theorem MIPStarRE.LDT.ev_opTensor_averageOperatorOverDistribution_left {α : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (ψ : QuantumState (ι₁ × ι₂)) (𝒟 : Distribution α) (A : α → Quantum.Op ι₁) (B : Quantum.Op ι₂) : ev ψ (opTensor (averageOperatorOverDistribution 𝒟 A) B) = avgOver 𝒟 fun (a : α) => ev ψ (opTensor (A a) B)

Evaluation of an averaged left tensor factor is the average of the corresponding tensor expectations.

theorem MIPStarRE.LDT.ev_opTensor_averageOperatorOverDistribution_right {α : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (ψ : QuantumState (ι₁ × ι₂)) (𝒟 : Distribution α) (A : Quantum.Op ι₁) (B : α → Quantum.Op ι₂) : ev ψ (opTensor A (averageOperatorOverDistribution 𝒟 B)) = avgOver 𝒟 fun (a : α) => ev ψ (opTensor A (B a))

Evaluation of an averaged right tensor factor is the average of the corresponding tensor expectations.

theorem MIPStarRE.LDT.leftTensor_mul_rightTensor_smul_left {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (c : Error) (A : Quantum.Op ι₁) (B : Quantum.Op ι₂) : leftTensor (↑c • A) * rightTensor B = ↑c • (leftTensor A * rightTensor B)

A complex scalar on the left register factors out of a bipartite tensor product.

This is the tensor-placement version of bilinearity of opTensor: placing c • A on the left and multiplying by the right placement of B equals the same scalar multiplying leftTensor A * rightTensor B.

theorem MIPStarRE.LDT.leftTensor_mul_rightTensor_smul_right {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (c : Error) (A : Quantum.Op ι₁) (B : Quantum.Op ι₂) : leftTensor A * rightTensor (↑c • B) = ↑c • (leftTensor A * rightTensor B)

A complex scalar on the right register factors out of a bipartite tensor product.

This is the tensor-placement version of bilinearity of opTensor: placing c • B on the right and multiplying by the left placement of A equals the same scalar multiplying leftTensor A * rightTensor B.

theorem MIPStarRE.LDT.leftTensor_mul_rightTensor_real_smul_left {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (c : Error) (A : Quantum.Op ι₁) (B : Quantum.Op ι₂) : leftTensor (c • A) * rightTensor B = ↑c • (leftTensor A * rightTensor B)

A real scalar on the left register factors out of a bipartite tensor product.

This restates leftTensor_mul_rightTensor_smul_left for the real scalar action used by averageOperatorOverDistribution, coercing the real scalar to ℂ on the tensor product.

theorem MIPStarRE.LDT.leftTensor_mul_rightTensor_real_smul_right {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] (c : Error) (A : Quantum.Op ι₁) (B : Quantum.Op ι₂) : leftTensor A * rightTensor (c • B) = ↑c • (leftTensor A * rightTensor B)

A real scalar on the right register factors out of a bipartite tensor product.

This restates leftTensor_mul_rightTensor_smul_right for the real scalar action used by averageOperatorOverDistribution, coercing the real scalar to ℂ on the tensor product.

theorem MIPStarRE.LDT.leftTensor_nonneg {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] {A : Quantum.Op ι₁} (hA : 0 ≤ A) : 0 ≤ leftTensor A

Left tensor placement preserves positivity.

theorem MIPStarRE.LDT.rightTensor_nonneg {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] {A : Quantum.Op ι₂} (hA : 0 ≤ A) : 0 ≤ rightTensor A

Right tensor placement preserves positivity.

theorem MIPStarRE.LDT.leftTensor_le_one {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] {A : Quantum.Op ι₁} (hA : A ≤ 1) : leftTensor A ≤ 1

Left tensor placement preserves the operator bound ≤ 1.

theorem MIPStarRE.LDT.sum_ev_leftTensor_outcome_le_one {α : Type u_1} [Fintype α] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) (hnorm : ψ.IsNormalized) (A : SubMeas α ι) : ∑ a : α, ev ψ (leftTensor (A.outcome a)) ≤ 1

The total left-register expectation of a submeasurement is at most one on a normalized bipartite state.

theorem MIPStarRE.LDT.rightTensor_le_one {ι₁ : Type u_1} {ι₂ : Type u_2} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] {A : Quantum.Op ι₂} (hA : A ≤ 1) : rightTensor A ≤ 1

Right tensor placement preserves the operator bound ≤ 1.

theorem MIPStarRE.LDT.SubMeas.opTensor_sum_filter_le_one {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (S T : SubMeas α ι) (P : α → Prop) [DecidablePred P] : ∑ x : α with P x, opTensor (S.outcome x) (T.outcome x) ≤ 1

A filtered diagonal tensor sum of two submeasurements is a contraction.

The estimate uses only positivity and the submeasurement total bound on the left factor, together with the pointwise ≤ 1 bound on the right factor.

Sandwich tensor estimates

theorem MIPStarRE.LDT.sandwichTensorSummand_nonneg {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ιA : Type u_4} {ιB : Type u_5} [Fintype α] [Fintype β] [Fintype γ] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (ψ : QuantumState (ιA × ιB)) (Outer : SubMeas β ιA) (Inner : SubMeas α ιA) (Right : SubMeas γ ιB) (o : β) (i : α) (r : γ) : 0 ≤ ev ψ (leftTensor (Outer.outcome o * Inner.outcome i * Outer.outcome o) * rightTensor (Right.outcome r))

A single tensor summand with a sandwiched left register is nonnegative in expectation.

The left register Outer_o * Inner_i * Outer_o is PSD by sandwich positivity, and the right-register outcome is PSD, so their tensor product is PSD.

theorem MIPStarRE.LDT.sandwichTensor_residual_sum_le_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ιA : Type u_4} {ιB : Type u_5} [Fintype α] [Fintype β] [Fintype γ] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (ψ : QuantumState (ιA × ιB)) (hnorm : ψ.IsNormalized) (Outer : SubMeas β ιA) (Inner : SubMeas α ιA) (Right : SubMeas γ ιB) : ∑ ir : α × γ, ∑ o : β, ev ψ (leftTensor (Outer.outcome o * Inner.outcome ir.1 * Outer.outcome o) * rightTensor (Right.outcome ir.2)) ≤ 1

The residual tensor sum from a sandwiched left-register submeasurement and an independent right-register submeasurement is at most one in a normalized state.

The operator under the sum factors as (∑ o, Outer_o * Inner.total * Outer_o) ⊗ Right.total; the first factor is bounded by 1 by the submeasurement axioms and sandwich monotonicity. The second factor is also bounded by 1.