Documentation

MIPRE.Tailored.Fourier

The three forms of a projective measurement with outcomes in `F₂^k` #

Paper II, §2.1 (II:972–1006) and §3.4 (II:2887–2982). A projective measurement with outcomes in F₂^k can be given in three forms that carry the same data (II:988):

the projective form, projections P_a summing to one, for a ∈ F₂^k;
the observable form, k commuting involutions U i;
the representation form, the homomorphism α ↦ U^α = ∏_i (U i)^{α_i} on F₂^k.

The passage from the observable form to the projective form is the Fourier transform P_a = ∏_i (1 + (-1)^{a_i} U i) / 2 (MIPRE.Tailored.fourierProj, defined with the tailored games in MIPRE.Tailored.Game). This file proves, in any complex ⋆-algebra:

isPVMIn_fourierProj: the Fourier transform of commuting self-adjoint involutions is a projective measurement, by induction on k from the case of one involution (isPVMIn_fourierFactor) and products of commuting measurements (IsPVMIn.prod_of_commute);
mul_fourierProj, obsChar_mul_fourierProj: P_a lies in the (-1)^{a_i}-eigenspace of U i, and in the (-1)^{⟨α, a⟩}-eigenspace of U^α;
pvmObs_fourierProj_bit, pvmObs_fourierProj_dotBit: the inverse transforms, U i = ∑_a (-1)^{a_i} P_a and U^α = ∑_a (-1)^{⟨α, a⟩} P_a (II:982);
Commute.fourierProj_right: whatever commutes with the observables commutes with the projections, so a strategy commuting along edges in observable form does so in projective form (II:1124);
isDiag_fourierProj: diagonal observables have diagonal projections (II:996);
pvmObs_coarse_affine: affine data processing (Claim II:2918) — the observable of the coarse-graining along a ↦ c + ⟨α, a⟩ is (-1)^c U^α; with IsPVMIn.coarse, the diagonal data processing of Claim II:2902 is isDiag_coarse.

`⟨α, a⟩` over `F₂` #

def MIPRE.Tailored.dotBit {k : ℕ} (α a : Fin k → Bool) :

The inner product ⟨α, a⟩ = ∑_i α_i a_i over F₂.

Equations

MIPRE.Tailored.dotBit α a = List.foldr (fun (i : Fin k) (acc : Bool) => α i && a i ^^ acc) false (List.finRange k)

Instances For

@[simp]

theorem MIPRE.Tailored.dotBit_zero (α a : Fin 0 → Bool) :

dotBit α a = false

theorem MIPRE.Tailored.dotBit_succ {k : ℕ} (α a : Fin (k + 1) → Bool) :

dotBit α a = (α 0 && a 0 ^^ dotBit (fun (i : Fin k) => α i.succ) fun (i : Fin k) => a i.succ)

def MIPRE.Tailored.obsChar {R : Type u_1} [Ring R] {k : ℕ} (U : Fin k → R) (α : Fin k → Bool) :

R

The representation form U^α = ∏_i (U i)^{α_i} of a family of commuting involutions.

Equations

MIPRE.Tailored.obsChar U α = (List.map (fun (i : Fin k) => if α i = true then U i else 1) (List.finRange k)).prod

Instances For

@[simp]

theorem MIPRE.Tailored.obsChar_zero {R : Type u_1} [Ring R] (U : Fin 0 → R) (α : Fin 0 → Bool) :

obsChar U α = 1

theorem MIPRE.Tailored.obsChar_succ {R : Type u_1} [Ring R] {k : ℕ} (U : Fin (k + 1) → R) (α : Fin (k + 1) → Bool) :

obsChar U α = (if α 0 = true then U 0 else 1) * obsChar (fun (i : Fin k) => U i.succ) fun (i : Fin k) => α i.succ

theorem Commute.obsChar_right {R : Type u_1} [Ring R] {k : ℕ} {x : R} {U : Fin k → R} (h : ∀ (i : Fin k), Commute x (U i)) (α : Fin k → Bool) :

Commute x (MIPRE.Tailored.obsChar U α)

theorem MIPRE.IsPVMIn.prod_of_commute {R : Type u_1} [Ring R] [StarRing R] {Λ : Type u_2} {Λ' : Type u_3} [Fintype Λ] [Fintype Λ'] {P : Λ → R} {Q : Λ' → R} (hP : IsPVMIn P) (hQ : IsPVMIn Q) (hc : ∀ (a : Λ) (b : Λ'), Commute (P a) (Q b)) :

IsPVMIn fun (p : Λ × Λ') => P p.1 * Q p.2

Products of commuting projective measurements: if every element of P commutes with every element of Q, then (a, b) ↦ P a * Q b is a projective measurement.

One involution #

theorem MIPRE.Tailored.fourierFactor_def {R : Type u_1} [Ring R] [Algebra ℂ R] (u : R) (b : Bool) :

fourierFactor u b = (1 / 2) • (1 + bitSign b • u)

theorem MIPRE.Tailored.fourierFactor_false_add_true {R : Type u_1} [Ring R] [Algebra ℂ R] (u : R) :

fourierFactor u false + fourierFactor u true = 1

theorem MIPRE.Tailored.fourierFactor_mul_self {R : Type u_1} [Ring R] [Algebra ℂ R] {u : R} (hu : u * u = 1) (b : Bool) :

fourierFactor u b * fourierFactor u b = fourierFactor u b

theorem MIPRE.Tailored.fourierFactor_mul_of_ne {R : Type u_1} [Ring R] [Algebra ℂ R] {u : R} (hu : u * u = 1) {b c : Bool} (h : b ≠ c) :

fourierFactor u b * fourierFactor u c = 0

theorem MIPRE.Tailored.mul_fourierFactor {R : Type u_1} [Ring R] [Algebra ℂ R] {u : R} (hu : u * u = 1) (b : Bool) :

u * fourierFactor u b = bitSign b • fourierFactor u b

u acts on the range of (1 + (-1)^b u)/2 as (-1)^b.

theorem Commute.fourierFactor_right {R : Type u_1} [Ring R] [Algebra ℂ R] {x u : R} (h : Commute x u) (b : Bool) :

Commute x (MIPRE.Tailored.fourierFactor u b)

theorem MIPRE.Tailored.star_fourierFactor {R : Type u_1} [Ring R] [Algebra ℂ R] [StarRing R] [StarModule ℂ R] {u : R} (hu : star u = u) (b : Bool) :

star (fourierFactor u b) = fourierFactor u b

theorem MIPRE.Tailored.isPVMIn_fourierFactor {R : Type u_1} [Ring R] [Algebra ℂ R] [StarRing R] [StarModule ℂ R] {u : R} (hu : u * u = 1) (hsa : star u = u) :

IsPVMIn (fourierFactor u)

One involution is a projective measurement with two outcomes.

The Fourier transform #

@[simp]

theorem MIPRE.Tailored.fourierProj_zero {R : Type u_1} [Ring R] [Algebra ℂ R] (U : Fin 0 → R) (a : Fin 0 → Bool) :

fourierProj U a = 1

theorem MIPRE.Tailored.fourierProj_succ {R : Type u_1} [Ring R] [Algebra ℂ R] {k : ℕ} (U : Fin (k + 1) → R) (a : Fin (k + 1) → Bool) :

fourierProj U a = fourierFactor (U 0) (a 0) * fourierProj (fun (i : Fin k) => U i.succ) fun (i : Fin k) => a i.succ

theorem Commute.fourierProj_right {R : Type u_1} [Ring R] [Algebra ℂ R] {k : ℕ} {x : R} {U : Fin k → R} (h : ∀ (i : Fin k), Commute x (U i)) (a : Fin k → Bool) :

Commute x (MIPRE.Tailored.fourierProj U a)

Whatever commutes with the observables commutes with the projections.

theorem Commute.fourierProj_fourierProj {R : Type u_1} [Ring R] [Algebra ℂ R] {k k' : ℕ} {U : Fin k → R} {V : Fin k' → R} (h : ∀ (i : Fin k) (j : Fin k'), Commute (U i) (V j)) (a : Fin k → Bool) (b : Fin k' → Bool) :

Commute (MIPRE.Tailored.fourierProj U a) (MIPRE.Tailored.fourierProj V b)

Observables commuting across two families give projections commuting across them: a strategy commuting along an edge in observable form does so in projective form (II:1124).

theorem MIPRE.Tailored.mul_fourierProj {R : Type u_1} [Ring R] [Algebra ℂ R] {k : ℕ} {U : Fin k → R} (hinv : ∀ (i : Fin k), U i * U i = 1) (hcomm : ∀ (i j : Fin k), Commute (U i) (U j)) (i : Fin k) (a : Fin k → Bool) :

U i * fourierProj U a = bitSign (a i) • fourierProj U a

P_a lies in the (-1)^{a_i}-eigenspace of U i.

theorem MIPRE.Tailored.obsChar_mul_fourierProj {R : Type u_1} [Ring R] [Algebra ℂ R] {k : ℕ} {U : Fin k → R} (hinv : ∀ (i : Fin k), U i * U i = 1) (hcomm : ∀ (i j : Fin k), Commute (U i) (U j)) (α a : Fin k → Bool) :

obsChar U α * fourierProj U a = bitSign (dotBit α a) • fourierProj U a

P_a lies in the (-1)^{⟨α, a⟩}-eigenspace of U^α.

The Fourier transform is a projective measurement #

theorem MIPRE.Tailored.isPVMIn_fourierProj {R : Type u_1} [Ring R] [Algebra ℂ R] {k : ℕ} [StarRing R] [StarModule ℂ R] {U : Fin k → R} (hinv : ∀ (i : Fin k), U i * U i = 1) (hsa : ∀ (i : Fin k), star (U i) = U i) (hcomm : ∀ (i j : Fin k), Commute (U i) (U j)) :

IsPVMIn (fourierProj U)

The Fourier transform of commuting self-adjoint involutions is a projective measurement (II:974): the projective form of the measurement whose observable form is U.

theorem MIPRE.Tailored.pvmObs_fourierProj_bit {R : Type u_1} [Ring R] [Algebra ℂ R] {k : ℕ} [StarRing R] [StarModule ℂ R] {U : Fin k → R} (hinv : ∀ (i : Fin k), U i * U i = 1) (hsa : ∀ (i : Fin k), star (U i) = U i) (hcomm : ∀ (i j : Fin k), Commute (U i) (U j)) (i : Fin k) :

(pvmObs (fourierProj U) fun (a : Fin k → Bool) => bitSign (a i)) = U i

The inverse Fourier transform, in observable form: U i = ∑_a (-1)^{a_i} P_a (II:982).

theorem MIPRE.Tailored.pvmObs_fourierProj_dotBit {R : Type u_1} [Ring R] [Algebra ℂ R] {k : ℕ} [StarRing R] [StarModule ℂ R] {U : Fin k → R} (hinv : ∀ (i : Fin k), U i * U i = 1) (hsa : ∀ (i : Fin k), star (U i) = U i) (hcomm : ∀ (i j : Fin k), Commute (U i) (U j)) (α : Fin k → Bool) :

(pvmObs (fourierProj U) fun (a : Fin k → Bool) => bitSign (dotBit α a)) = obsChar U α

The inverse Fourier transform, in representation form: U^α = ∑_a (-1)^{⟨α, a⟩} P_a (II:982).

theorem MIPRE.Tailored.pvmObs_coarse_affine {R : Type u_1} [Ring R] [Algebra ℂ R] {k : ℕ} [StarRing R] [StarModule ℂ R] {U : Fin k → R} (hinv : ∀ (i : Fin k), U i * U i = 1) (hsa : ∀ (i : Fin k), star (U i) = U i) (hcomm : ∀ (i j : Fin k), Commute (U i) (U j)) (α : Fin k → Bool) (c : Bool) :

pvmObs (fun (b : Bool) => ∑ a : Fin k → Bool with (c ^^ dotBit α a) = b, fourierProj U a) bitSign = bitSign c • obsChar U α

Affine data processing (Claim II:2918): coarse-graining the Fourier transform of U along the affine map a ↦ c + ⟨α, a⟩ gives the measurement whose observable is (-1)^c U^α.

Diagonal measurements #

theorem MIPRE.Tailored.isDiag_mul {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℂ} (hA : A.IsDiag) (hB : B.IsDiag) :

(A * B).IsDiag

A product of diagonal matrices is diagonal.

theorem MIPRE.Tailored.isDiag_fourierProj {n : Type u_1} [Fintype n] [DecidableEq n] {k : ℕ} {U : Fin k → Matrix n n ℂ} (h : ∀ (i : Fin k), (U i).IsDiag) (a : Fin k → Bool) :

(fourierProj U a).IsDiag

Diagonal observables have diagonal projections (II:996).

theorem MIPRE.Tailored.isDiag_coarse {n : Type u_1} {Λ : Type u_2} {Λ' : Type u_3} [Fintype Λ] [DecidableEq Λ'] {P : Λ → Matrix n n ℂ} (h : ∀ (a : Λ), (P a).IsDiag) (f : Λ → Λ') (b : Λ') :

(∑ a : Λ with f a = b, P a).IsDiag

Diagonal data processing (Claim II:2902): coarse-graining a diagonal measurement gives a diagonal measurement.