Distance measures

This file contains the definitions of the blueprint subsection "Distance measures" (Section 2, "Foundations"): the dimension-normalized Hilbert--Schmidt inner product and squared norm on complex matrices, and the distance between two families of POVMs relative to a question distribution.

Main definitions

• MIPRE.hsInner: the dimension-normalized Hilbert--Schmidt inner product ⟨A, B⟩_hs = τ(Aᴴ B), where τ = Tr/d is the dimension-normalized trace (blueprint def:hs-norm).
• MIPRE.hsNormSq: the squared dimension-normalized Hilbert--Schmidt norm ‖A‖²_hs = τ(Aᴴ A) (blueprint def:hs-norm).
• MIPRE.povmDistance: the squared distance 𝔼_{x ∼ μ} ∑ₐ ‖M^x_a - N^x_a‖²_hs between two families of POVMs (blueprint def:distance).
• MIPRE.IsPOVMClose: the δ-closeness relation M ≈_δ N of the blueprint.

Implementation notes

• As elsewhere in the foundations, question distributions are bare real-valued functions: povmDistance and IsPOVMClose take any μ : X → ℝ, and results about them will assume nonnegativity and normalization as needed.
• ⟨A, A⟩_hs is a nonnegative real for every A, but proving so requires a positivity argument; hsNormSq takes the real part .re so that the definition carries no proof obligations. Nonnegativity is recorded separately in hsNormSq_nonneg.
• The blueprint writes the POVM distance as 𝔼_{x ∼ μ} ∑ₐ τ((M^x_a - N^x_a)²); since differences of POVM elements are Hermitian, this agrees with the definition here (see hsNormSq_of_isHermitian).

The normalized Hilbert--Schmidt inner product

noncomputable def MIPRE.hsInner {n : Type u_1} [Fintype n] (A B : Matrix n n ℂ) : ℂ

The dimension-normalized Hilbert--Schmidt inner product on square complex matrices (blueprint def:hs-norm): ⟨A, B⟩_hs = τ(Aᴴ B), where τ = Tr/d is the dimension-normalized trace.

Equations

• MIPRE.hsInner A B = (A.conjTranspose * B).trace / ↑(Fintype.card n)

noncomputable def MIPRE.hsNormSq {n : Type u_1} [Fintype n] (A : Matrix n n ℂ) : ℝ

The squared dimension-normalized Hilbert--Schmidt norm on square complex matrices (blueprint def:hs-norm): ‖A‖²_hs = τ(Aᴴ A), a nonnegative real (hsNormSq_nonneg).

Equations

• MIPRE.hsNormSq A = (MIPRE.hsInner A A).re

theorem MIPRE.hsNormSq_nonneg {n : Type u_1} [Fintype n] (A : Matrix n n ℂ) : 0 ≤ hsNormSq A

theorem MIPRE.hsNormSq_of_isHermitian {n : Type u_1} [Fintype n] {A : Matrix n n ℂ} (hA : A.IsHermitian) : hsNormSq A = ((A * A).trace / ↑(Fintype.card n)).re

For a Hermitian matrix, the squared normalized Hilbert--Schmidt norm is the normalized trace of the square, which is the form used in blueprint def:distance.

POVM distance

noncomputable def MIPRE.povmDistance {X : Type u_2} {A : Type u_3} {d : Type u_4} [Fintype X] [Fintype A] [Fintype d] [DecidableEq d] (μ : X → ℝ) (M N : X → POVM A d) : ℝ

The squared distance between two families of POVMs relative to a question distribution μ (blueprint def:distance): 𝔼_{x ∼ μ} ∑ₐ ‖M^x_a - N^x_a‖²_hs.

Equations

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

def MIPRE.IsPOVMClose {X : Type u_2} {A : Type u_3} {d : Type u_4} [Fintype X] [Fintype A] [Fintype d] [DecidableEq d] (μ : X → ℝ) (δ : ℝ) (M N : X → POVM A d) : Prop

Two families of POVMs are δ-close relative to the question distribution μ, written M^x_a ≈_δ N^x_a in the blueprint (blueprint def:distance).

Equations

• MIPRE.IsPOVMClose μ δ M N = (MIPRE.povmDistance μ M N ≤ δ)

Constructions on POVMs

noncomputable def MIPRE.POVM.map {A : Type u_3} {d : Type u_4} [Fintype A] [Fintype d] [DecidableEq d] {B : Type u_5} [Fintype B] [DecidableEq B] (f : A → B) (M : POVM A d) : POVM B d

Relabel the outcomes of a POVM along f : A → B (data processing): the operator of the outcome b is the sum of the operators of the outcomes a with f a = b.

Equations

• MIPRE.POVM.map f M = { mats := fun (b : B) => ∑ a : A with f a = b, M.mats a, nonneg := ⋯, normalized := ⋯ }

def MIPRE.ProjectiveMeasurement.toPOVM {X : Type u_2} {A : Type u_3} {d : Type u_4} [Fintype A] [Fintype d] [DecidableEq d] (P : ProjectiveMeasurement X A (Matrix d d ℂ)) (x : X) : POVM A d

The measurement for the question x of a projective measurement family on the matrix algebra ℂ^{d×d}, as a POVM (positivity follows from projectivity).

Equations

• P.toPOVM x = { mats := fun (a : A) => ⟨P.M x a, ⋯⟩, nonneg := ⋯, normalized := ⋯ }

noncomputable def MIPRE.uniform (X : Type u_5) [Fintype X] : X → ℝ

The uniform distribution on a finite type, as a real-valued weight function.

Equations

• MIPRE.uniform X x✝ = (↑(Fintype.card X))⁻¹

Inconsistency of two measurement families on a bipartite state

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

The inconsistency of two families of POVMs M (acting on ℂ^dA) and N (acting on ℂ^dB) with the same question and outcome alphabets, relative to a question distribution μ and a bipartite state ψ ∈ ℂ^dA ⊗ ℂ^dB = ℂ^(dA × dB): the probability that measuring M^x on the first factor and N^x on the second factor yields different outcomes, 𝔼_{x ∼ μ} ∑_{a ≠ b} ⟨ψ| M^x_a ⊗ N^x_b |ψ⟩ (the consistency relation of JNVWY21qld, Definition 4.8, in its two-space form). The tensor product is realized by the Kronecker product, as in TensorProductStrategy.value; the probability is a nonnegative real, and we take the real part so that the definition carries no proof obligation.

Equations

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