The bit observables of an encoded measurement

A projective measurement P with outcomes in a finite set Λ, together with an encoding enc : Λ → F₂^k, gives k observables, one per bit of the encoding: encObs P enc i = ∑_λ (-1)^{enc(λ)_i} P_λ (encObs). These are the observables a permutation strategy must supply at a question whose answers are the encoded outcomes of P. This file proves that they have every property of MIPRE.Tailored.PermStrategy but the signed-permutation one, which depends on P:

• encObs_mul_self, star_encObs, commute_encObs: they are commuting self-adjoint involutions;
• fourierProj_encObs: their Fourier transform is the push-forward of P along enc, P'_a = ∑_{enc(λ) = a} P_λ; so the permutation strategy built from them measures exactly the encoded outcomes of P;
• commute_encObs_encObs: they commute with the bit observables of any measurement commuting with P.

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

The observable of the i-th bit of the encoded outcome.

Equations

• MIPRE.Tailored.encObs P enc i = MIPRE.pvmObs P fun (l : Λ) => MIPRE.Tailored.bitSign (enc l i)

theorem MIPRE.Tailored.encObs_mul_self {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {Λ : Type u_2} [Fintype Λ] {k : ℕ} {P : Λ → R} (hP : IsPVMIn P) (enc : Λ → Fin k → Bool) (i : Fin k) : encObs P enc i * encObs P enc i = 1

theorem MIPRE.Tailored.commute_encObs {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {Λ : Type u_2} [Fintype Λ] {k : ℕ} {P : Λ → R} (hP : IsPVMIn P) (enc : Λ → Fin k → Bool) (i j : Fin k) : Commute (encObs P enc i) (encObs P enc j)

theorem MIPRE.Tailored.star_encObs {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {Λ : Type u_2} [Fintype Λ] {k : ℕ} {P : Λ → R} (hP : IsPVMIn P) (enc : Λ → Fin k → Bool) [StarModule ℂ R] (i : Fin k) : star (encObs P enc i) = encObs P enc i

theorem MIPRE.Tailored.sum_filter_eq_pvmObs {R : Type u_1} [Ring R] [Algebra ℂ R] {Λ : Type u_2} [Fintype Λ] {P : Λ → R} (p : Λ → Prop) [DecidablePred p] : ∑ l : Λ with p l, P l = pvmObs P fun (l : Λ) => if p l then 1 else 0

A coarse-graining of P, as the observable of an indicator weighting.

theorem MIPRE.Tailored.half_one_add_bitSign_mul (b c : Bool) : 1 / 2 * (1 + bitSign b * bitSign c) = if c = b then 1 else 0

(1 + (-1)^b (-1)^c) / 2 is the indicator of b = c.

theorem MIPRE.Tailored.fourierFactor_encObs {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {Λ : Type u_2} [Fintype Λ] {k : ℕ} {P : Λ → R} (hP : IsPVMIn P) (enc : Λ → Fin k → Bool) (i : Fin k) (b : Bool) : fourierFactor (encObs P enc i) b = ∑ l : Λ with enc l i = b, P l

The Fourier factor of one bit observable is the coarse-graining of P onto that bit.

theorem MIPRE.Tailored.fourierProj_encObs {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] {Λ : Type u_2} [Fintype Λ] {k : ℕ} {P : Λ → R} (hP : IsPVMIn P) (enc : Λ → Fin k → Bool) (a : Fin k → Bool) : fourierProj (encObs P enc) a = ∑ l : Λ with enc l = a, P l

The Fourier transform of the bit observables is the push-forward of P along enc.

Transports of the measurement

The strategies of the introspection pipeline are carried from one game to the next by merging answers along a map and by extending the answer set by zero; the bit observables follow.

theorem MIPRE.Tailored.encObs_merge {R : Type u_1} [Ring R] [Algebra ℂ R] {Λ : Type u_2} [Fintype Λ] {k : ℕ} {Λ' : Type u_3} [Fintype Λ'] [DecidableEq Λ'] (P : Λ → R) (f : Λ → Λ') (enc : Λ' → Fin k → Bool) (i : Fin k) : encObs (fun (b : Λ') => ∑ a : Λ with f a = b, P a) enc i = encObs P (fun (a : Λ) => enc (f a)) i

Merging answers along f and then encoding is encoding the composite.

theorem MIPRE.Tailored.encObs_extend {R : Type u_1} [Ring R] [Algebra ℂ R] {Λ : Type u_2} [Fintype Λ] {k : ℕ} {Λ' : Type u_3} [Fintype Λ'] (P : Λ → R) {ι : Λ → Λ'} (hι : Function.Injective ι) (enc : Λ' → Fin k → Bool) (i : Fin k) : encObs (Function.extend ι P 0) enc i = encObs P (fun (a : Λ) => enc (ι a)) i

Extending the answers by zero along an injection and then encoding is encoding the composite.

theorem MIPRE.Tailored.commute_encObs_encObs {R : Type u_1} [Ring R] [Algebra ℂ R] {Λ : Type u_2} [Fintype Λ] {k : ℕ} {Λ' : Type u_3} [Fintype Λ'] {k' : ℕ} {P : Λ → R} {Q : Λ' → R} (h : ∀ (l : Λ) (l' : Λ'), Commute (P l) (Q l')) (enc : Λ → Fin k → Bool) (enc' : Λ' → Fin k' → Bool) (i : Fin k) (j : Fin k') : Commute (encObs P enc i) (encObs Q enc' j)

Bit observables of commuting measurements commute.