localOperatorInner

formal source

 258
 259/-- Hilbert-Schmidt-style pairing on single-core operators in the standard
 260ququart basis. -/
 261def localOperatorInner (A B : QuquartState →ₗ[ℂ] QuquartState) : ℂ :=
 262  ∑ s : Fin 4, ∑ t : Fin 4, star (A (basisKet s) t) * B (basisKet s) t
 263
 264/-- The standard ququart basis is orthonormal for the explicit finite sum. -/
 265theorem basisKet_orthonormal (m n : Fin 4) :
 266    ∑ t : Fin 4, star (basisKet m t) * basisKet n t = if m = n then 1 else 0 := by
 267  fin_cases m <;> fin_cases n <;> simp [basisKet]
 268
 269/-- Mod-4 subtraction undoes mod-4 addition. -/
 270theorem sub4_add4_cancel (a s : Fin 4) :
 271    sub4 (add4 a s) a = s := by
 272  fin_cases a <;> fin_cases s <;> rfl
 273
 274/-- Mod-4 addition undoes mod-4 subtraction. -/
 275theorem add4_sub4_cancel (m a : Fin 4) :
 276    add4 a (sub4 m a) = m := by
 277  fin_cases m <;> fin_cases a <;> rfl
 278
 279/-- The local Weyl monomial sends a basis ket to a phased basis ket. -/
 280theorem localWeylMonomial_basisKet (a b s : Fin 4) :
 281    localWeylMonomial a b (basisKet s) =
 282      (Complex.I ^ (b.val * (add4 a s).val)) • basisKet (add4 a s) := by
 283  ext m
 284  by_cases hm : m = add4 a s
 285  · subst hm
 286    simp [localWeylMonomial, basisKet, sub4_add4_cancel_core]
 287  · have hsub : sub4 m a ≠ s := by
 288      intro hEq
 289      apply hm
 290      calc
 291        m = add4 a (sub4 m a) := by symm; exact add4_sub4_cancel_core m a