Documentation

MIPRE.Foundations.Introspection.LinearMeasurement

Fourier formulas for a linear-map measurement #

The two identities of lem:pauli-linear-fourier, in characteristic two. The formulas hold for either Weyl family, and more generally for any operator family with its Fourier-defined spectral operators. Orthogonality is the actual dot product perpendicular subspace, not a canonical direct-sum complement.

source
theorem MIPRE.Introspection.instCharPOfNatNat_mIPRE {F : Type u_1} [Field F] [Algebra (ZMod 2) F] :
CharP F 2
source
noncomputable def MIPRE.Introspection.subspaceTrace {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {n : ℕ} (S : Submodule F (Fin n → F)) (c : Fin n → F) :
↥S →ₗ[ZMod 2] ZMod 2

Restrict the trace character to a linear subspace, viewed over the binary field.

Equations
Instances For
    source
    @[simp]
    theorem MIPRE.Introspection.subspaceTrace_apply {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (S : Submodule F (Fin n → F)) (c : Fin n → F) (v : ↥S) :
    (subspaceTrace S c) v = Weyl.trDot (↑v) c
    source
    theorem MIPRE.Introspection.subspaceTrace_eq_zero_iff {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (S : Submodule F (Fin n → F)) (c : Fin n → F) :
    subspaceTrace S c = 0 ↔ c ∈ CL.perp S

    The trace annihilator of an F-subspace is its ordinary dot-product perpendicular.

    source
    theorem MIPRE.Introspection.sum_subspace_sign {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (S : Submodule F (Fin n → F)) (c : Fin n → F) :
    ∑ v : ↥S, sgn (Weyl.trDot (↑v) c) = if c ∈ CL.perp S then ↑(Fintype.card ↥S) else 0

    Character cancellation on a subspace.

    source
    theorem MIPRE.Introspection.trDot_eq_of_same_fiber {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (L : (Fin n → F) →ₗ[F] Fin n → F) {v x y : Fin n → F} (hv : v ∈ CL.perp L.ker) (hxy : L x = L y) :
    Weyl.trDot v x = Weyl.trDot v y

    On a fiber, every trace character perpendicular to the kernel is constant.

    source
    noncomputable def MIPRE.Introspection.linearPreimage {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (L : (Fin n → F) →ₗ[F] Fin n → F) (a : Fin n → F) :
    Fin n → F

    Pick a preimage only to state the Fourier coefficients; this is not an executable choice.

    Equations
    Instances For
      source
      theorem MIPRE.Introspection.linearPreimage_image {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (L : (Fin n → F) →ₗ[F] Fin n → F) (x : Fin n → F) :
      L (linearPreimage L (L x)) = L x
      source
      theorem MIPRE.Introspection.linear_measurement_fourier {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (w : (Fin n → F) → Matrix (Fin n → F) (Fin n → F) ℂ) (L : (Fin n → F) →ₗ[F] Fin n → F) (v : Fin n → F) (hv : v ∈ CL.perp L.ker) :
      w v = ∑ a : Fin n → F, sgn (Weyl.trDot v (linearPreimage L a)) • Weyl.synOf w (⇑L) a

      Expand an allowed Pauli operator in the projectors of the linear-map measurement.

      source
      theorem MIPRE.Introspection.linear_measurement_fourier_inverse {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (w : (Fin n → F) → Matrix (Fin n → F) (Fin n → F) ℂ) (L : (Fin n → F) →ₗ[F] Fin n → F) (x : Fin n → F) :
      (↑(Fintype.card ↥(CL.perp L.ker)))⁻¹ • ∑ v : ↥(CL.perp L.ker), sgn (Weyl.trDot (↑v) x) • w ↑v = Weyl.synOf w (⇑L) (L x)

      Recover the projector on a fiber by averaging only over the kernel's perpendicular.