Documentation

MIPRE.Tailored.Intro.Bits

The observable of one bit of an outcome #

Phase 3c of planning/aldous-lyons-track.md (issue #281) computes, question by question, the bit observables encObs P enc i of the honest strategy of the introspection verifier. Each is the observable of one Boolean function of the outcome, bitObs P f = ∑_λ (-1)^{f λ} P_λ, and the computation goes through the constructions the honest strategy is assembled from:

bitObs_congr: only the outcomes with a nonzero projection matter;
bitObs_merge, bitObs_fibSum, bitObs_extend, bitObs_submatrix, bitObs_kronecker_one: coarse-graining, zero extension, relabelling and an ancilla act on the bit function;
bitObs_const, bitObs_xor: a constant bit is ±1, and the observable of an exclusive or is the product;
bitObs_mul_fst, bitObs_mul_snd: a bit of one factor of a joint measurement;
bitObs_kronecker: a bit of an adaptive tensor P a ⊗ Q a b is controlled by P;
bitObs_readout: a bit of a classical read-out is a ±1 diagonal.

IsZBit P f (a signed permutation, diagonal) and IsXBit P f (a signed permutation) are the two properties the ZPC strategy needs of a readable and of a linear bit.

noncomputable def MIPRE.Tailored.bitObs {R : Type u_1} [Ring R] [Algebra ℂ R] {Λ : Type u_2} [Fintype Λ] (P : Λ → R) (f : Λ → Bool) :

R

The observable of the bit f of the outcome of P: ∑_λ (-1)^{f λ} P_λ.

Equations

MIPRE.Tailored.bitObs P f = MIPRE.pvmObs P fun (l : Λ) => MIPRE.Tailored.bitSign (f l)

Instances For

theorem MIPRE.Tailored.encObs_eq_bitObs {R : Type u_1} [Ring R] [Algebra ℂ R] {Λ : Type u_2} [Fintype Λ] (P : Λ → R) {k : ℕ} (enc : Λ → Fin k → Bool) (i : Fin k) :

encObs P enc i = bitObs P fun (l : Λ) => enc l i

theorem MIPRE.Tailored.bitObs_congr {R : Type u_1} [Ring R] [Algebra ℂ R] {Λ : Type u_2} [Fintype Λ] {P : Λ → R} {f g : Λ → Bool} (h : ∀ (l : Λ), P l ≠ 0 → f l = g l) :

bitObs P f = bitObs P g

Only the outcomes with a nonzero projection matter.

theorem MIPRE.Tailored.bitObs_merge {R : Type u_1} [Ring R] [Algebra ℂ R] {Λ : Type u_2} [Fintype Λ] {Λ' : Type u_3} [Fintype Λ'] [DecidableEq Λ'] (P : Λ → R) (φ : Λ → Λ') (f : Λ' → Bool) :

bitObs (fun (b : Λ') => ∑ a : Λ with φ a = b, P a) f = bitObs P (f ∘ φ)

theorem MIPRE.Tailored.bitObs_extend {R : Type u_1} [Ring R] [Algebra ℂ R] {Λ : Type u_2} [Fintype Λ] {Λ' : Type u_3} [Fintype Λ'] (P : Λ → R) {ι : Λ → Λ'} (hι : Function.Injective ι) (f : Λ' → Bool) :

bitObs (Function.extend ι P 0) f = bitObs P (f ∘ ι)

theorem MIPRE.Tailored.bitObs_comp_equiv {R : Type u_1} [Ring R] [Algebra ℂ R] {Λ : Type u_2} [Fintype Λ] {Λ' : Type u_3} [Fintype Λ'] (P : Λ → R) (e : Λ' ≃ Λ) (f : Λ → Bool) :

bitObs (fun (b : Λ') => P (e b)) (f ∘ ⇑e) = bitObs P f

theorem MIPRE.Tailored.bitObs_comp_equiv' {R : Type u_1} [Ring R] [Algebra ℂ R] {Λ : Type u_2} [Fintype Λ] {Λ' : Type u_3} [Fintype Λ'] (P : Λ → R) (e : Λ' ≃ Λ) (f : Λ' → Bool) :

bitObs (fun (b : Λ') => P (e b)) f = bitObs P (f ∘ ⇑e.symm)

theorem MIPRE.Tailored.bitObs_const {R : Type u_1} [Ring R] [Algebra ℂ R] {Λ : Type u_2} [Fintype Λ] [StarRing R] {P : Λ → R} (hP : IsPVMIn P) (c : Bool) :

(bitObs P fun (x : Λ) => c) = bitSign c • 1

theorem MIPRE.Tailored.bitObs_xor {R : Type u_1} [Ring R] [Algebra ℂ R] {Λ : Type u_2} [Fintype Λ] [StarRing R] {P : Λ → R} (hP : IsPVMIn P) (f g : Λ → Bool) :

(bitObs P fun (l : Λ) => f l ^^ g l) = bitObs P f * bitObs P g

The observable of an exclusive or is the product.

theorem MIPRE.Tailored.fibSum_eq_merge {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_3} [Fintype Λ] {Λ' : Type u_4} [DecidableEq Λ'] (P : Λ → Matrix Ω Ω ℂ) (φ : Λ → Λ') :

fibSum P φ = fun (b : Λ') => ∑ a : Λ with φ a = b, P a

theorem MIPRE.Tailored.bitObs_fibSum {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_3} [Fintype Λ] {Λ' : Type u_4} [Fintype Λ'] [DecidableEq Λ'] (P : Λ → Matrix Ω Ω ℂ) (φ : Λ → Λ') (f : Λ' → Bool) :

bitObs (fibSum P φ) f = bitObs P (f ∘ φ)

theorem MIPRE.Tailored.bitObs_submatrix {Ω : Type u_1} {Ω' : Type u_2} [Fintype Ω] [DecidableEq Ω] [Fintype Ω'] [DecidableEq Ω'] {Λ : Type u_3} [Fintype Λ] (P : Λ → Matrix Ω Ω ℂ) (e : Ω' → Ω) (f : Λ → Bool) :

bitObs (fun (a : Λ) => (P a).submatrix e e) f = (bitObs P f).submatrix e e

theorem MIPRE.Tailored.bitObs_kronecker_one {Ω : Type u_1} {Ω' : Type u_2} [Fintype Ω] [DecidableEq Ω] [Fintype Ω'] [DecidableEq Ω'] {Λ : Type u_3} [Fintype Λ] (P : Λ → Matrix Ω Ω ℂ) (f : Λ → Bool) :

bitObs (fun (a : Λ) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P a) 1) f = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (bitObs P f) 1

theorem MIPRE.Tailored.bitObs_zero {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_3} [Fintype Λ] (f : Λ → Bool) :

bitObs (fun (x : Λ) => 0) f = 0

theorem MIPRE.Tailored.bitObs_add_kronecker {Ω : Type u_1} {Ω' : Type u_2} [Fintype Ω] [DecidableEq Ω] [Fintype Ω'] [DecidableEq Ω'] {A : Type u_4} {B : Type u_5} [Fintype A] [Fintype B] (P : A → Matrix Ω Ω ℂ) (Q : A → B → Matrix Ω' Ω' ℂ) (f : A × B → Bool) :

bitObs (fun (ab : A × B) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P ab.1) (Q ab.1 ab.2)) f = ∑ a : A, Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P a) (bitObs (Q a) fun (b : B) => f (a, b))

theorem MIPRE.Tailored.bitObs_mul_fst {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {A : Type u_4} {B : Type u_5} [Fintype A] [Fintype B] (P : A → Matrix Ω Ω ℂ) (Q : B → Matrix Ω Ω ℂ) (hQ : ∑ b : B, Q b = 1) (f : A → Bool) :

(bitObs (fun (ab : A × B) => P ab.1 * Q ab.2) fun (ab : A × B) => f ab.1) = bitObs P f

A bit of one factor of a joint measurement, the other factor summing to one.

theorem MIPRE.Tailored.bitObs_mul_snd {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {A : Type u_4} {B : Type u_5} [Fintype A] [Fintype B] (P : A → Matrix Ω Ω ℂ) (Q : B → Matrix Ω Ω ℂ) (hP : ∑ a : A, P a = 1) (f : B → Bool) :

(bitObs (fun (ab : A × B) => P ab.1 * Q ab.2) fun (ab : A × B) => f ab.2) = bitObs Q f

theorem MIPRE.Tailored.bitObs_readout {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {K : Type u_4} [Fintype K] [DecidableEq K] (φ : Ω → K) (f : K → Bool) :

bitObs (Introspection.readout φ) f = Matrix.diagonal fun (i : Ω) => bitSign (f (φ i))

A bit of a classical read-out is a ±1 diagonal.

The two properties of a bit #

def MIPRE.Tailored.IsZBit {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_3} [Fintype Λ] (P : Λ → Matrix Ω Ω ℂ) (f : Λ → Bool) :

A readable bit: its observable is a diagonal signed permutation.

Equations

MIPRE.Tailored.IsZBit P f = (MIPRE.Tailored.IsSignedPerm (MIPRE.Tailored.bitObs P f) ∧ (MIPRE.Tailored.bitObs P f).IsDiag)

Instances For

def MIPRE.Tailored.IsXBit {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_3} [Fintype Λ] (P : Λ → Matrix Ω Ω ℂ) (f : Λ → Bool) :

A linear bit: its observable is a signed permutation.

Equations

MIPRE.Tailored.IsXBit P f = MIPRE.Tailored.IsSignedPerm (MIPRE.Tailored.bitObs P f)

Instances For

theorem MIPRE.Tailored.IsZBit.isXBit {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_3} [Fintype Λ] {P : Λ → Matrix Ω Ω ℂ} {f : Λ → Bool} (h : IsZBit P f) :

theorem MIPRE.Tailored.isSignedPerm_bitSign_smul_one {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (c : Bool) :

IsSignedPerm (bitSign c • 1)

theorem MIPRE.Tailored.isDiag_bitSign_smul_one {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (c : Bool) :

(bitSign c • 1).IsDiag

theorem MIPRE.Tailored.isZBit_const {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_3} [Fintype Λ] {P : Λ → Matrix Ω Ω ℂ} (hP : IsPVMIn P) (c : Bool) :

IsZBit P fun (x : Λ) => c

theorem MIPRE.Tailored.isZBit_readout {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {K : Type u_4} [Fintype K] [DecidableEq K] (φ : Ω → K) (f : K → Bool) :

IsZBit (Introspection.readout φ) f

theorem MIPRE.Tailored.IsZBit.congr {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_3} [Fintype Λ] {P : Λ → Matrix Ω Ω ℂ} {f g : Λ → Bool} (h : IsZBit P f) (hfg : ∀ (l : Λ), P l ≠ 0 → f l = g l) :

theorem MIPRE.Tailored.IsXBit.congr {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_3} [Fintype Λ] {P : Λ → Matrix Ω Ω ℂ} {f g : Λ → Bool} (h : IsXBit P f) (hfg : ∀ (l : Λ), P l ≠ 0 → f l = g l) :

theorem MIPRE.Tailored.IsXBit.xor {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_3} [Fintype Λ] {P : Λ → Matrix Ω Ω ℂ} (hP : IsPVMIn P) {f g : Λ → Bool} (hf : IsXBit P f) (hg : IsXBit P g) :

IsXBit P fun (l : Λ) => f l ^^ g l

theorem MIPRE.Tailored.IsZBit.xor {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_3} [Fintype Λ] {P : Λ → Matrix Ω Ω ℂ} (hP : IsPVMIn P) {f g : Λ → Bool} (hf : IsZBit P f) (hg : IsZBit P g) :

IsZBit P fun (l : Λ) => f l ^^ g l

theorem MIPRE.Tailored.isZBit_merge_iff {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_3} [Fintype Λ] {Λ' : Type u_4} [Fintype Λ'] [DecidableEq Λ'] (P : Λ → Matrix Ω Ω ℂ) (φ : Λ → Λ') (f : Λ' → Bool) :

IsZBit (fun (b : Λ') => ∑ a : Λ with φ a = b, P a) f ↔ IsZBit P (f ∘ φ)

theorem MIPRE.Tailored.isXBit_merge_iff {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] {Λ : Type u_3} [Fintype Λ] {Λ' : Type u_4} [Fintype Λ'] [DecidableEq Λ'] (P : Λ → Matrix Ω Ω ℂ) (φ : Λ → Λ') (f : Λ' → Bool) :

IsXBit (fun (b : Λ') => ∑ a : Λ with φ a = b, P a) f ↔ IsXBit P (f ∘ φ)

theorem MIPRE.Tailored.IsZBit.submatrix_equiv {Ω : Type u_1} {Ω' : Type u_2} [Fintype Ω] [DecidableEq Ω] [Fintype Ω'] [DecidableEq Ω'] {Λ : Type u_3} [Fintype Λ] {P : Λ → Matrix Ω Ω ℂ} {f : Λ → Bool} (h : IsZBit P f) (e : Ω' ≃ Ω) :

IsZBit (fun (a : Λ) => (P a).submatrix ⇑e ⇑e) f

theorem MIPRE.Tailored.IsXBit.submatrix_equiv {Ω : Type u_1} {Ω' : Type u_2} [Fintype Ω] [DecidableEq Ω] [Fintype Ω'] [DecidableEq Ω'] {Λ : Type u_3} [Fintype Λ] {P : Λ → Matrix Ω Ω ℂ} {f : Λ → Bool} (h : IsXBit P f) (e : Ω' ≃ Ω) :

IsXBit (fun (a : Λ) => (P a).submatrix ⇑e ⇑e) f

theorem MIPRE.Tailored.IsZBit.kronecker_one {Ω : Type u_1} {Ω' : Type u_2} [Fintype Ω] [DecidableEq Ω] [Fintype Ω'] [DecidableEq Ω'] {Λ : Type u_3} [Fintype Λ] {P : Λ → Matrix Ω Ω ℂ} {f : Λ → Bool} (h : IsZBit P f) :

IsZBit (fun (a : Λ) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P a) 1) f

theorem MIPRE.Tailored.IsXBit.kronecker_one {Ω : Type u_1} {Ω' : Type u_2} [Fintype Ω] [DecidableEq Ω] [Fintype Ω'] [DecidableEq Ω'] {Λ : Type u_3} [Fintype Λ] {P : Λ → Matrix Ω Ω ℂ} {f : Λ → Bool} (h : IsXBit P f) :

IsXBit (fun (a : Λ) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (P a) 1) f

theorem MIPRE.Tailored.isXBit_controlled {Ω : Type u_1} {Ω' : Type u_2} [Fintype Ω] [DecidableEq Ω] [Fintype Ω'] [DecidableEq Ω'] {K : Type u_4} {A : Type u_5} [Fintype K] [DecidableEq K] [Fintype A] (φ : Ω → K) (Q : K → A → Matrix Ω' Ω' ℂ) (f : K × A → Bool) (h : ∀ (z : K), IsXBit (Q z) fun (a : A) => f (z, a)) :

IsXBit (fun (za : K × A) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Introspection.readout φ za.1) (Q za.1 za.2)) f

A bit controlled by a classical read-out: if the measurement is readout φ z ⊗ Q z a at (z, a), the bit is a signed permutation when each Q z's is.

theorem MIPRE.Tailored.isZBit_controlled {Ω : Type u_1} {Ω' : Type u_2} [Fintype Ω] [DecidableEq Ω] [Fintype Ω'] [DecidableEq Ω'] {K : Type u_4} {A : Type u_5} [Fintype K] [DecidableEq K] [Fintype A] (φ : Ω → K) (Q : K → A → Matrix Ω' Ω' ℂ) (f : K × A → Bool) (h : ∀ (z : K), IsZBit (Q z) fun (a : A) => f (z, a)) :

IsZBit (fun (za : K × A) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Introspection.readout φ za.1) (Q za.1 za.2)) f