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 := ⋯ }

theorem MIPRE.POVM.ext' {A : Type u_3} {d : Type u_4} [Fintype A] [Fintype d] [DecidableEq d] {M N : POVM A d} (h : ∀ (a : A), ↑(M.mats a) = ↑(N.mats a)) : M = N

A POVM is determined by its operators. The remaining fields are propositions.

@[simp]

theorem MIPRE.POVM.map_mats {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) (b : B) : ↑((map f M).mats b) = ∑ a : A with f a = b, ↑(M.mats a)

theorem MIPRE.POVM.map_map {A : Type u_3} {d : Type u_4} [Fintype A] [Fintype d] [DecidableEq d] {B : Type u_5} {C : Type u_6} [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] (M : POVM A d) (f : A → B) (g : B → C) : map g (map f M) = map (fun (a : A) => g (f a)) M

Relabelling twice is relabelling once: the level sets of g ∘ f are the unions of the level sets of f along the level sets of g.

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.

theorem MIPRE.inconsistency_congr {X : Type u_5} {X' : Type u_6} {A : Type u_7} {A' : Type u_8} {dA : Type u_9} {dB : Type u_10} [Fintype X] [Fintype X'] [Fintype A] [Fintype A'] [DecidableEq A] [DecidableEq A'] [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (μ : X → ℝ) (μ' : X' → ℝ) (ψ : dA × dB → ℂ) (M : X → POVM A dA) (N : X → POVM A dB) (M' : X' → POVM A' dA) (N' : X' → POVM A' dB) (eX : X' ≃ X) (eA : A' ≃ A) (hμ : ∀ (x' : X'), μ' x' = μ (eX x')) (hM : ∀ (x' : X') (a' : A'), ↑((M' x').mats a') = ↑((M (eX x')).mats (eA a'))) (hN : ∀ (x' : X') (b' : A'), ↑((N' x').mats b') = ↑((N (eX x')).mats (eA b'))) : inconsistency μ' ψ M' N' = inconsistency μ ψ M N

inconsistency is invariant under relabelling. The questions may be relabelled by a bijection matching the two distributions, and the outcomes by a bijection --- the same one on both sides, since what is measured is whether the two agree. The state is untouched.

A reduction between two tests needs exactly this to carry a consistency conclusion back: the question alphabets differ by a bijection (here coordinate reversal) and the outcome alphabets by a relabelling of the low-degree polynomials.