coupledOperatorInner

formal source

 459  simpa [hidx] using hinner
 460
 461/-- Hilbert-Schmidt-style pairing on coupled-core operators. -/
 462def coupledOperatorInner {N : ℕ}
 463    (A B : CoupledCoreSpace N →ₗ[ℂ] CoupledCoreSpace N) : ℂ :=
 464  ∑ s : CoupledCoreIndex N, ∑ t : CoupledCoreIndex N,
 465    star (A (coupledBasisKet s) t) * B (coupledBasisKet s) t
 466
 467/-- The coupled phase character has unit modulus. -/
 468lemma phaseCharacter_star_mul_self {N : ℕ} (b s : CoupledCoreIndex N) :
 469    star (phaseCharacter b s) * phaseCharacter b s = 1 := by
 470  have hnorm : Complex.normSq (phaseCharacter b s) = 1 := by
 471    unfold phaseCharacter
 472    rw [map_prod Complex.normSq]
 473    apply Finset.prod_eq_one
 474    intro x hx
 475    simp [Complex.normSq_I]
 476  have hconj := Complex.normSq_eq_conj_mul_self (z := phaseCharacter b s)
 477  rw [hnorm] at hconj
 478  exact hconj.symm
 479
 480/-- A tensor-Weyl monomial has Hilbert-Schmidt norm squared equal to the
 481dimension of the coupled-core carrier. -/
 482theorem tensorWeylMonomial_self_inner {N : ℕ} (a b : CoupledCoreIndex N) :
 483    coupledOperatorInner (tensorWeylMonomial a b) (tensorWeylMonomial a b) =
 484      Fintype.card (CoupledCoreIndex N) := by
 485  unfold coupledOperatorInner
 486  have hs : ∀ s : CoupledCoreIndex N,
 487      ∑ t : CoupledCoreIndex N,
 488        star ((tensorWeylMonomial a b (coupledBasisKet s)) t) *
 489          (tensorWeylMonomial a b (coupledBasisKet s)) t = 1 := by
 490    intro s
 491    let c := phaseCharacter b (addedConfig a s)
 492    let m := addedConfig a s