The concrete coordinate splits for nested CL registers

def MIPRE.Introspection.ambientSplit {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] (V : Finset ι) : (ι → F) ≃ (↥V → F) × (↥Vᶜ → F)

Splitting an ambient assignment into a register and its complement.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Introspection.coordinateSplit {ι : Type u_1} {F : Type u_2} [DecidableEq ι] (U V : Finset ι) (hUV : U ⊆ V) : (↥V → F) ≃ (Fin (Fintype.card ↥U) → F) × (↥(V \ U) → F)

Split V into the selected coordinates U, enumerated by Fin, and V \ U. This is an actual coordinate restriction and assembly, rather than a cardinality choice.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Introspection.coordinateInsert {ι : Type u_1} {F : Type u_2} [DecidableEq ι] [Field F] (U : Finset ι) : (Fin (Fintype.card ↥U) → F) →ₗ[F] ι → F

Insert an enumerated vector into its ambient register, setting all other coordinates to zero.

Equations

• MIPRE.Introspection.coordinateInsert U = { toFun := fun (v : Fin (Fintype.card ↥U) → F) (i : ι) => if h : i ∈ U then v ((Fintype.equivFin ↥U) ⟨i, h⟩) else 0, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def MIPRE.Introspection.coordinateRestrict {ι : Type u_1} {F : Type u_2} [Field F] (U : Finset ι) : (ι → F) →ₗ[F] Fin (Fintype.card ↥U) → F

Restrict the ambient assignment to the enumerated register.

Equations

• MIPRE.Introspection.coordinateRestrict U = { toFun := fun (v : ι → F) (j : Fin (Fintype.card ↥U)) => v ↑((Fintype.equivFin ↥U).symm j), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MIPRE.Introspection.coordinateRestrict_insert {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] (U : Finset ι) (v : Fin (Fintype.card ↥U) → F) : (coordinateRestrict U) ((coordinateInsert U) v) = v

theorem MIPRE.Introspection.coordinateInsert_restrict {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] (U : Finset ι) (v : ι → F) : (coordinateInsert U) ((coordinateRestrict U) v) = (CL.proj U) v

noncomputable def MIPRE.Introspection.coordinateLinear {ι : Type u_1} {F : Type u_2} [DecidableEq ι] [Field F] {U : Finset ι} (L : CL.RegLinear F U) : (Fin (Fintype.card ↥U) → F) →ₗ[F] Fin (Fintype.card ↥U) → F

The paper's map on U in the coordinate presentation used by the Pauli library.

Equations

• MIPRE.Introspection.coordinateLinear L = MIPRE.Introspection.coordinateRestrict U ∘ₗ L.toLinearMap ∘ₗ MIPRE.Introspection.coordinateInsert U

theorem MIPRE.Introspection.coordinateLinear_restrict {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] {U : Finset ι} (L : CL.RegLinear F U) (v : ι → F) : (coordinateLinear L) ((coordinateRestrict U) v) = (coordinateRestrict U) (L v)

Restricting the ambient CL linear map commutes with passing to register coordinates.

theorem MIPRE.Introspection.coordinateInsert_linear {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] {U : Finset ι} (L : CL.RegLinear F U) (v : Fin (Fintype.card ↥U) → F) : (coordinateInsert U) ((coordinateLinear L) v) = L ((coordinateInsert U) v)

Reassembling the coordinate result recovers the original CL linear map exactly.