The state-dependent distance on a bipartite state

Every soundness argument in the Pauli basis test's appendix compares operators in the distance

A^x ≈_δ B^x ⟺ 𝔼_{x ∼ μ} ⟨ψ| (A^x - B^x)† (A^x - B^x) |ψ⟩ ≤ δ,

where the operators act on Alice's factor of a bipartite state |ψ⟩ ∈ ℂ^{dA} ⊗ ℂ^{dB}. That is not the distance MIPRE/Foundations/Distances.lean defines: povmDistance and IsPOVMClose use the normalized Hilbert--Schmidt norm, which is the tracial — synchronous — specialization, and MIPRE/Foundations/Closeness.lean says so in its own docstring. This file is the state-dependent one, and it is what blueprint def:state-distance names.

Two deliberate departures from the paper's qld-prelim.tex:

• no O(·) inside the definition. The paper writes ≤ O(δ); here the relation is stateDist μ ψ A B ≤ δ and the constants appear in the lemmas that produce them. That is stronger, not weaker: stateSqNorm_avg_le preserves δ exactly and povm_to_obs gives exactly |𝒜| · δ.
• answer-indexed families as well. The paper's ≈_δ is for operators indexed by questions but not answers; the applications also need the form summed over a common outcome set (cor:ortho-from-consistency concludes P_a ⊗ Id ≈ Q_a ⊗ Id). Both are here, the second as povmStateDist.

Implementation

stateVec ψ A = (A ⊗ Id)|ψ⟩, carried in EuclideanSpace ℂ (dA × dB) so that the triangle inequality and ‖c • v‖ = ‖c‖‖v‖ are Mathlib's rather than rebuilt. The bridge to the blueprint's quadratic-form spelling is stateSqNorm_eq, which is the only place the Kronecker adjoint is used.

In a bipartite model

The norm, the distances and the two closeness lemmas are stated for any bipartite model (MIPRE/Foundations/BipartiteModel.lean) with the first player's operators in its algebra, and the matrix ones are their instances in the tensor-product model (stateNorm_eq_tensor, stateDist_eq_tensor, povmStateDist_eq_tensor). What stays about matrices is the vector stateVec itself and the factor swap, which a model does not need: its second player's norm is ‖πB b ψ‖, by the same definition.

The state norm and distance in a bipartite model

def MIPRE.BipartiteModel.stateNorm {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (a : 𝒜) : ℝ

‖πA a ψ‖: the norm of the first player's operator on the state.

Equations

• M.stateNorm a = M.snorm (M.πA a)

def MIPRE.BipartiteModel.stateSqNorm {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (a : 𝒜) : ℝ

⟨ψ| πA(a† a) |ψ⟩, the squared state-dependent norm.

Equations

• M.stateSqNorm a = M.stateNorm a ^ 2

theorem MIPRE.BipartiteModel.stateSqNorm_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (a : 𝒜) : M.stateSqNorm a = M.qform (M.πA (star a * a))

The squared norm is the quadratic form of a† a.

theorem MIPRE.BipartiteModel.inner_stateSqNorm {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (a : 𝒜) : inner ℂ M.ψ ((M.π (M.πA (star a * a))) M.ψ) = ↑(M.stateSqNorm a)

The squared norm is the quadratic form of a† a, as a complex number: the inner product is real.

theorem MIPRE.BipartiteModel.stateNorm_nonneg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (a : 𝒜) : 0 ≤ M.stateNorm a

theorem MIPRE.BipartiteModel.stateSqNorm_nonneg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (a : 𝒜) : 0 ≤ M.stateSqNorm a

theorem MIPRE.BipartiteModel.sqrt_stateSqNorm {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (a : 𝒜) : √(M.stateSqNorm a) = M.stateNorm a

theorem MIPRE.BipartiteModel.stateNorm_smul {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (c : ℂ) (a : 𝒜) : M.stateNorm (c • a) = ‖c‖ * M.stateNorm a

theorem MIPRE.BipartiteModel.stateNorm_sum_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {ι : Type u_4} (s : Finset ι) (f : ι → 𝒜) : M.stateNorm (∑ i ∈ s, f i) ≤ ∑ i ∈ s, M.stateNorm (f i)

theorem MIPRE.BipartiteModel.inner_πA_πB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {q : 𝒜} (hq : star q = q) (r : ℬ) : inner ℂ ((M.π (M.πA q)) M.ψ) ((M.π (M.πB r)) M.ψ) = inner ℂ M.ψ ((M.π (M.πA q * M.πB r)) M.ψ)

The inner product of the two players' vectors is the quadratic form of their product, for a self-adjoint first operator.

def MIPRE.BipartiteModel.stateDist {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} [Fintype X] (μ : X → ℝ) (A B : X → 𝒜) : ℝ

The state-dependent distance of two families of the first player's operators, relative to a question distribution μ: blueprint def:state-distance.

Equations

• M.stateDist μ A B = ∑ x : X, μ x * M.stateSqNorm (A x - B x)

theorem MIPRE.BipartiteModel.stateDist_nonneg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} [Fintype X] {μ : X → ℝ} (hμ : ∀ (x : X), 0 ≤ μ x) (A B : X → 𝒜) : 0 ≤ M.stateDist μ A B

def MIPRE.BipartiteModel.povmStateDist {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} [Fintype X] [PartialOrder 𝒜] {A : Type u_5} [Fintype A] (μ : X → ℝ) (MA NA : X → POVMIn A 𝒜) : ℝ

The same distance for families indexed by answers as well.

Equations

• M.povmStateDist μ MA NA = ∑ x : X, μ x * ∑ a : A, M.stateSqNorm ((MA x).op a - (NA x).op a)

theorem MIPRE.BipartiteModel.stateDist_obsOf_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} [Fintype X] [PartialOrder 𝒜] {A : Type u_5} [Fintype A] {μ : X → ℝ} (hμ0 : ∀ (x : X), 0 ≤ μ x) (MA NA : X → POVMIn A 𝒜) (α : A → ℂ) (hα : ∀ (a : A), ‖α a‖ ≤ 1) : (M.stateDist μ (fun (x : X) => pvmObs (MA x).op α) fun (x : X) => pvmObs (NA x).op α) ≤ ↑(Fintype.card A) * M.povmStateDist μ MA NA

From POVM elements to generalized observables, blueprint lem:qld-povm-to-obs: the weighting costs a factor |𝒜|, from Cauchy--Schwarz over the outcome set.

theorem MIPRE.BipartiteModel.stateSqNorm_avg_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} [Fintype X] {μ : X → ℝ} (hμ0 : ∀ (x : X), 0 ≤ μ x) (hμ1 : ∑ x : X, μ x = 1) (A B : X → 𝒜) (α : X → ℂ) (hα : ∀ (x : X), ‖α x‖ ≤ 1) : M.stateSqNorm (∑ x : X, (↑(μ x) * α x) • A x - ∑ x : X, (↑(μ x) * α x) • B x) ≤ M.stateDist μ A B

Averaging preserves closeness, blueprint lem:qld-averaging.

The vector (A ⊗ Id)|ψ⟩

noncomputable def MIPRE.stateVec {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (M : Matrix dA dA ℂ) : EuclideanSpace ℂ (dA × dB)

(M ⊗ Id)|ψ⟩, as a vector of EuclideanSpace ℂ (dA × dB).

Equations

• MIPRE.stateVec ψ M = WithLp.toLp 2 ((Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M 1).mulVec ψ)

@[simp]

theorem MIPRE.stateVec_add {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (M N : Matrix dA dA ℂ) : stateVec ψ (M + N) = stateVec ψ M + stateVec ψ N

@[simp]

theorem MIPRE.stateVec_smul {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (c : ℂ) (M : Matrix dA dA ℂ) : stateVec ψ (c • M) = c • stateVec ψ M

@[simp]

theorem MIPRE.stateVec_zero {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) : stateVec ψ 0 = 0

@[simp]

theorem MIPRE.stateVec_neg {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (M : Matrix dA dA ℂ) : stateVec ψ (-M) = -stateVec ψ M

@[simp]

theorem MIPRE.stateVec_sub {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (M N : Matrix dA dA ℂ) : stateVec ψ (M - N) = stateVec ψ M - stateVec ψ N

theorem MIPRE.stateVec_sum {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] {ι : Type u_4} (ψ : dA × dB → ℂ) (s : Finset ι) (f : ι → Matrix dA dA ℂ) : stateVec ψ (∑ i ∈ s, f i) = ∑ i ∈ s, stateVec ψ (f i)

The norm, and the distance

noncomputable def MIPRE.stateNorm {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (M : Matrix dA dA ℂ) : ℝ

‖(M ⊗ Id)|ψ⟩‖.

Equations

• MIPRE.stateNorm ψ M = ‖MIPRE.stateVec ψ M‖

noncomputable def MIPRE.stateSqNorm {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (M : Matrix dA dA ℂ) : ℝ

⟨ψ| M† M ⊗ Id |ψ⟩, the squared state-dependent norm.

Equations

• MIPRE.stateSqNorm ψ M = MIPRE.stateNorm ψ M ^ 2

theorem MIPRE.stateNorm_eq_tensor {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] [DecidableEq dA] (ψ : dA × dB → ℂ) (M : Matrix dA dA ℂ) : stateNorm ψ M = (BipartiteModel.tensor ψ).stateNorm M

The matrix state norm is that of the tensor-product model.

theorem MIPRE.stateSqNorm_eq_tensor {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] [DecidableEq dA] (ψ : dA × dB → ℂ) (M : Matrix dA dA ℂ) : stateSqNorm ψ M = (BipartiteModel.tensor ψ).stateSqNorm M

theorem MIPRE.quadForm_eq {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (M : Matrix dA dA ℂ) : star ψ ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (M.conjTranspose * M) 1).mulVec ψ = ↑(stateSqNorm ψ M)

The squared norm is the blueprint's quadratic form, as a complex number: ⟨ψ| M† M ⊗ Id |ψ⟩ is real and equal to stateSqNorm ψ M. It is what makes the Lean definition and def:state-distance's spelling the same object rather than informally the same. The complex form is what a positivity hypothesis on a linear functional wants.

theorem MIPRE.stateSqNorm_eq {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (M : Matrix dA dA ℂ) : stateSqNorm ψ M = (star ψ ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (M.conjTranspose * M) 1).mulVec ψ).re

The real form of quadForm_eq, which is how def:state-distance is written.

theorem MIPRE.stateSqNorm_nonneg {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (M : Matrix dA dA ℂ) : 0 ≤ stateSqNorm ψ M

noncomputable def MIPRE.stateDist {X : Type u_1} [Fintype X] {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] (μ : X → ℝ) (ψ : dA × dB → ℂ) (A B : X → Matrix dA dA ℂ) : ℝ

The state-dependent distance of two families of operators on Alice's factor, relative to a question distribution μ and the state ψ: blueprint def:state-distance.

Equations

• MIPRE.stateDist μ ψ A B = ∑ x : X, μ x * MIPRE.stateSqNorm ψ (A x - B x)

def MIPRE.IsStateClose {X : Type u_1} [Fintype X] {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] (μ : X → ℝ) (ψ : dA × dB → ℂ) (δ : ℝ) (A B : X → Matrix dA dA ℂ) : Prop

A ≈_δ B on ψ, relative to μ.

Equations

• MIPRE.IsStateClose μ ψ δ A B = (MIPRE.stateDist μ ψ A B ≤ δ)

theorem MIPRE.stateDist_eq_tensor {X : Type u_1} [Fintype X] {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] [DecidableEq dA] (μ : X → ℝ) (ψ : dA × dB → ℂ) (A B : X → Matrix dA dA ℂ) : stateDist μ ψ A B = (BipartiteModel.tensor ψ).stateDist μ A B

noncomputable def MIPRE.povmStateDist {X : Type u_1} [Fintype X] {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] {A : Type u_4} [Fintype A] [DecidableEq dA] (μ : X → ℝ) (ψ : dA × dB → ℂ) (M N : X → POVM A dA) : ℝ

The same distance for families indexed by answers as well, which is the form the consistency statements take: the outcome sum is inside the question average.

Equations

• MIPRE.povmStateDist μ ψ M N = ∑ x : X, μ x * ∑ a : A, MIPRE.stateSqNorm ψ (↑((M x).mats a) - ↑((N x).mats a))

def MIPRE.IsPOVMStateClose {X : Type u_1} [Fintype X] {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] {A : Type u_4} [Fintype A] [DecidableEq dA] (μ : X → ℝ) (ψ : dA × dB → ℂ) (δ : ℝ) (M N : X → POVM A dA) : Prop

M_a ≈_δ N_a on ψ, relative to μ.

Equations

• MIPRE.IsPOVMStateClose μ ψ δ M N = (MIPRE.povmStateDist μ ψ M N ≤ δ)

theorem MIPRE.povmStateDist_eq_tensor {X : Type u_1} [Fintype X] {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] {A : Type u_4} [Fintype A] [DecidableEq dA] (μ : X → ℝ) (ψ : dA × dB → ℂ) (M N : X → POVM A dA) : povmStateDist μ ψ M N = (BipartiteModel.tensor ψ).povmStateDist μ (fun (x : X) => (M x).toIn) fun (x : X) => (N x).toIn

The two closeness lemmas of the appendix's preliminaries

noncomputable def MIPRE.obsOf {X : Type u_1} {dA : Type u_2} [Fintype dA] {A : Type u_4} [Fintype A] [DecidableEq dA] (α : A → ℂ) (M : X → POVM A dA) (x : X) : Matrix dA dA ℂ

The generalized observable of a POVM family and a weighting of the outcomes: A^x = ∑_a α_a A^x_a.

Equations

• MIPRE.obsOf α M x = ∑ a : A, α a • ↑((M x).mats a)

theorem MIPRE.stateDist_obsOf_le {X : Type u_1} [Fintype X] {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] {A : Type u_4} [Fintype A] [DecidableEq dA] {μ : X → ℝ} (hμ0 : ∀ (x : X), 0 ≤ μ x) (ψ : dA × dB → ℂ) (M N : X → POVM A dA) (α : A → ℂ) (hα : ∀ (a : A), ‖α a‖ ≤ 1) : stateDist μ ψ (obsOf α M) (obsOf α N) ≤ ↑(Fintype.card A) * povmStateDist μ ψ M N

From POVM elements to generalized observables, blueprint lem:qld-povm-to-obs: the weighting costs a factor |𝒜|, from Cauchy--Schwarz over the outcome set. The paper asks the weights to be of unit modulus; ‖α a‖ ≤ 1 is all the proof uses.

Bob's factor, by the swap

cor:ortho-from-consistency compares (Q_a ⊗ Id)|ψ⟩ against (Id ⊗ R_a)|ψ⟩, so it needs the vectors of the other factor too. Rather than duplicate the calculus above, observe that Bob's factor is Alice's factor of the swapped state: swapVec exchanges the two tensor factors, and norm_stateVecB identifies the two norms. Every lemma proved above then applies on Bob's side with dA and dB exchanged.

def MIPRE.swapVec {dA : Type u_2} {dB : Type u_3} (ψ : dA × dB → ℂ) : dB × dA → ℂ

|ψ⟩ with its two tensor factors exchanged.

Equations

• MIPRE.swapVec ψ p = ψ p.swap

noncomputable def MIPRE.stateVecB {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dA] (ψ : dA × dB → ℂ) (N : Matrix dB dB ℂ) : EuclideanSpace ℂ (dA × dB)

(Id ⊗ N)|ψ⟩, as a vector of EuclideanSpace ℂ (dA × dB): the stateVec of Bob's factor.

Equations

• MIPRE.stateVecB ψ N = WithLp.toLp 2 ((Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 N).mulVec ψ)

theorem MIPRE.stateVecB_entry {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dA] (ψ : dA × dB → ℂ) (N : Matrix dB dB ℂ) (i : dA) (j : dB) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 N).mulVec ψ (i, j) = ∑ l : dB, N j l * ψ (i, l)

theorem MIPRE.norm_stateVecB_eq_tensor {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] [DecidableEq dA] (ψ : dA × dB → ℂ) (N : Matrix dB dB ℂ) : ‖stateVecB ψ N‖ = (BipartiteModel.tensor ψ).swap.stateNorm N

Bob's norm is the first player's norm in the swapped tensor-product model.

theorem MIPRE.normSq_stateVecB_eq_tensor {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] [DecidableEq dA] (ψ : dA × dB → ℂ) (N : Matrix dB dB ℂ) : ‖stateVecB ψ N‖ ^ 2 = (BipartiteModel.tensor ψ).swap.stateSqNorm N

@[simp]

theorem MIPRE.stateVecB_smul {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dA] (ψ : dA × dB → ℂ) (c : ℂ) (N : Matrix dB dB ℂ) : stateVecB ψ (c • N) = c • stateVecB ψ N

theorem MIPRE.stateVecB_sum {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dA] {ι : Type u_4} (ψ : dA × dB → ℂ) (t : Finset ι) (f : ι → Matrix dB dB ℂ) : stateVecB ψ (∑ i ∈ t, f i) = ∑ i ∈ t, stateVecB ψ (f i)

theorem MIPRE.stateVec_swapVec_entry {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dA] (ψ : dA × dB → ℂ) (N : Matrix dB dB ℂ) (i : dA) (j : dB) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) N 1).mulVec (swapVec ψ) (j, i) = ∑ l : dB, N j l * ψ (i, l)

theorem MIPRE.norm_stateVecB {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dA] (ψ : dA × dB → ℂ) (N : Matrix dB dB ℂ) : ‖stateVecB ψ N‖ = stateNorm (swapVec ψ) N

Bob's norm is Alice's norm of the swapped state.

theorem MIPRE.inner_stateVec_stateVecB {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] [DecidableEq dA] (ψ : dA × dB → ℂ) {Q : Matrix dA dA ℂ} (hQ : Q.conjTranspose = Q) (R : Matrix dB dB ℂ) : inner ℂ (stateVec ψ Q) (stateVecB ψ R) = star ψ ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) Q R).mulVec ψ

The inner product of the two factors' vectors is the blueprint's ⟨ψ| Q ⊗ R |ψ⟩, for self-adjoint Q: the inner product of the two players' vectors in the tensor-product model.

theorem MIPRE.swapVec_dotProduct {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] (ψ : dA × dB → ℂ) : star (swapVec ψ) ⬝ᵥ swapVec ψ = star ψ ⬝ᵥ ψ

The swap is a reindexing, so it preserves the norm of the state.

theorem MIPRE.stateSqNorm_avg_le {X : Type u_1} [Fintype X] {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] [DecidableEq dB] {μ : X → ℝ} (hμ0 : ∀ (x : X), 0 ≤ μ x) (hμ1 : ∑ x : X, μ x = 1) (ψ : dA × dB → ℂ) (A B : X → Matrix dA dA ℂ) (α : X → ℂ) (hα : ∀ (x : X), ‖α x‖ ≤ 1) : stateSqNorm ψ (∑ x : X, (↑(μ x) * α x) • A x - ∑ x : X, (↑(μ x) * α x) • B x) ≤ stateDist μ ψ A B

Averaging preserves closeness, blueprint lem:qld-averaging: a weighted average with weights of modulus at most one is no further apart than the families are. Triangle inequality, then Jensen for the square root (sum_mul_sqrt_le).