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: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Basic/TensorPlacement.lean in the port of planning/c6b-plan.md (milestone M0, section "Port conventions").

The vendored placements leftTensor A = A ⊗ 1 and rightTensor A = 1 ⊗ A are Kronecker products, and their identities are proved entrywise or through Matrix.kronecker lemmas. Here they are the ⋆-homomorphisms S.L and S.R of a symmetric model S, so each identity is a map_* lemma of a ⋆-homomorphism (linearity in a real or complex scalar, additivity over a finite sum), and the product placement S.opTensor A B = S.L A * S.R B is linear in each factor by the keystone's opTensor_* lemmas. Statements drop the normalization hypothesis hnorm : ψ.IsNormalized, which is a theorem of the model (VecState.ev_one_of_isNormalized).

Ported elsewhere

leftTensor_finset_sum, rightTensor_finset_sum, leftTensor_nonneg, rightTensor_nonneg, leftTensor_le_one and rightTensor_le_one are ported in Co/Basic/QuantumState.lean, with every operator-positivity fact of the port.

Not ported

Every other declaration of the vendored file has a counterpart here.

Tensor-placement helper lemmas

theorem MIPRE.LIDT.Co.SymModel.leftTensor_averageOperatorOverDistribution {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} (𝒟 : MIPStarRE.LDT.Distribution α) (A : α → 𝔓) : S.L (averageOperatorOverDistribution 𝒟 A) = averageOperatorOverDistribution 𝒟 fun (a : α) => S.L (A a)

Left tensor placement commutes with operator averages.

theorem MIPRE.LIDT.Co.SymModel.ev_leftTensor_total_eq_sum_outcome {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : SubMeas α 𝔓) : S.ev (S.L A.total) = ∑ a : α, S.ev (S.L (A.outcome a))

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

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

theorem MIPRE.LIDT.Co.SymModel.ev_leftTensor_averageOperatorOverDistribution {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} (𝒟 : MIPStarRE.LDT.Distribution α) (A : α → 𝔓) : S.ev (S.L (averageOperatorOverDistribution 𝒟 A)) = MIPStarRE.LDT.avgOver 𝒟 fun (a : α) => S.ev (S.L (A a))

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

theorem MIPRE.LIDT.Co.SymModel.rightTensor_averageOperatorOverDistribution {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} (𝒟 : MIPStarRE.LDT.Distribution α) (A : α → 𝔓) : S.R (averageOperatorOverDistribution 𝒟 A) = averageOperatorOverDistribution 𝒟 fun (a : α) => S.R (A a)

Right tensor placement commutes with operator averages.

theorem MIPRE.LIDT.Co.SymModel.ev_rightTensor_averageOperatorOverDistribution {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} (𝒟 : MIPStarRE.LDT.Distribution α) (A : α → 𝔓) : S.ev (S.R (averageOperatorOverDistribution 𝒟 A)) = MIPStarRE.LDT.avgOver 𝒟 fun (a : α) => S.ev (S.R (A a))

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

theorem MIPRE.LIDT.Co.SymModel.opTensor_averageOperatorOverDistribution_left {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} (𝒟 : MIPStarRE.LDT.Distribution α) (A : α → 𝔓) (B : 𝔓) : S.opTensor (averageOperatorOverDistribution 𝒟 A) B = averageOperatorOverDistribution 𝒟 fun (a : α) => S.opTensor (A a) B

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

theorem MIPRE.LIDT.Co.SymModel.opTensor_averageOperatorOverDistribution_right {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} (𝒟 : MIPStarRE.LDT.Distribution α) (A : 𝔓) (B : α → 𝔓) : S.opTensor A (averageOperatorOverDistribution 𝒟 B) = averageOperatorOverDistribution 𝒟 fun (a : α) => S.opTensor A (B a)

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

theorem MIPRE.LIDT.Co.SymModel.ev_opTensor_averageOperatorOverDistribution_left {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} (𝒟 : MIPStarRE.LDT.Distribution α) (A : α → 𝔓) (B : 𝔓) : S.ev (S.opTensor (averageOperatorOverDistribution 𝒟 A) B) = MIPStarRE.LDT.avgOver 𝒟 fun (a : α) => S.ev (S.opTensor (A a) B)

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

theorem MIPRE.LIDT.Co.SymModel.ev_opTensor_averageOperatorOverDistribution_right {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} (𝒟 : MIPStarRE.LDT.Distribution α) (A : 𝔓) (B : α → 𝔓) : S.ev (S.opTensor A (averageOperatorOverDistribution 𝒟 B)) = MIPStarRE.LDT.avgOver 𝒟 fun (a : α) => S.ev (S.opTensor A (B a))

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

theorem MIPRE.LIDT.Co.SymModel.leftTensor_mul_rightTensor_smul_left {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (c : ℝ) (A B : 𝔓) : S.L (↑c • A) * S.R B = ↑c • (S.L A * S.R B)

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

This is the 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 S.L A * S.R B.

theorem MIPRE.LIDT.Co.SymModel.leftTensor_mul_rightTensor_smul_right {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (c : ℝ) (A B : 𝔓) : S.L A * S.R (↑c • B) = ↑c • (S.L A * S.R B)

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

This is the 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 S.L A * S.R B.

theorem MIPRE.LIDT.Co.SymModel.leftTensor_mul_rightTensor_real_smul_left {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (c : ℝ) (A B : 𝔓) : S.L (c • A) * S.R B = ↑c • (S.L A * S.R B)

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

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

theorem MIPRE.LIDT.Co.SymModel.leftTensor_mul_rightTensor_real_smul_right {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (c : ℝ) (A B : 𝔓) : S.L A * S.R (c • B) = ↑c • (S.L A * S.R B)

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

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

theorem MIPRE.LIDT.Co.SymModel.sum_ev_leftTensor_outcome_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} [Fintype α] (A : SubMeas α 𝔓) : ∑ a : α, S.ev (S.L (A.outcome a)) ≤ 1

The total left-register expectation of a submeasurement is at most one (the vendored hypothesis hnorm : ψ.IsNormalized is a theorem of the model).

theorem MIPRE.LIDT.Co.SubMeas.opTensor_sum_filter_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} [Fintype α] (M : SymModel 𝔓 K) (S T : SubMeas α 𝔓) (P : α → Prop) [DecidablePred P] : ∑ x : α with P x, M.opTensor (S.outcome x) (T.outcome x) ≤ 1

A filtered diagonal product-placement 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. (The model M is an explicit argument here; the vendored statement names the carrier instead.)

Sandwich tensor estimates

theorem MIPRE.LIDT.Co.SymModel.sandwichTensorSummand_nonneg {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Fintype α] [Fintype β] [Fintype γ] (Outer : SubMeas β 𝔓) (Inner : SubMeas α 𝔓) (Right : SubMeas γ 𝔓) (o : β) (i : α) (r : γ) : 0 ≤ S.ev (S.L (Outer.outcome o * Inner.outcome i * Outer.outcome o) * S.R (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 positive by sandwich positivity, and the right-register outcome is positive, so their product placement is positive.

theorem MIPRE.LIDT.Co.SymModel.sandwichTensor_residual_sum_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Fintype α] [Fintype β] [Fintype γ] (Outer : SubMeas β 𝔓) (Inner : SubMeas α 𝔓) (Right : SubMeas γ 𝔓) : ∑ ir : α × γ, ∑ o : β, S.ev (S.L (Outer.outcome o * Inner.outcome ir.1 * Outer.outcome o) * S.R (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 (the vendored hypothesis hnorm : ψ.IsNormalized is a theorem of the model).

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