ConcreteDihedralSpectralArc.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Construction of the published spectral-arc input for an actual finite dihedral von Neumann algebra with its vector trace.

theorem OAI.KadisonSimilarity.centeredDihedralArc_rotation_moment line 14
theorem OAI.KadisonSimilarity.centeredDihedralArc_reflection_moment line 28

theorem OAI.KadisonSimilarity.concreteDihedralSpectralArcInput line 42

Source documentation

The centered arc exists in the specified von Neumann algebra, with all moments derived from the Haar and reflection-coset laws.

theorem concreteDihedralSpectralArcInput (Ω : H) (P : VonNeumannAlgebra H)
    (w d : (H →L[ℂ] H)ˣ) (hwP : (w : H →L[ℂ] H) ∈ P)
    (hw : star (w : H →L[ℂ] H) = (↑w⁻¹ : H →L[ℂ] H))
    (hwn : ‖(w : H →L[ℂ] H)‖ ≤ 1)
    (hd : (d : H →L[ℂ] H) * (d : H →L[ℂ] H) = 1)
    (hds : star (d : H →L[ℂ] H) = (d : H →L[ℂ] H))
    (hconj : (d : H →L[ℂ] H) * (w : H →L[ℂ] H) =
      star (w : H →L[ℂ] H) * (d : H →L[ℂ] H))
    (hhaar : ∀ l : ℤ, vectorTrace Ω (↑(w ^ l) : H →L[ℂ] H) = if l = 0 then 1 else 0)
    (hcoset : ∀ l : ℤ, vectorTrace Ω ((↑(w ^ l) : H →L[ℂ] H) * (d : H →L[ℂ] H)) = 0) :
    DihedralSpectralArcInput (vectorTrace Ω).toLinearMap P.toStarSubalgebra w d := by
…

Mentions: OAI.KadisonSimilarity.vectorTrace, OAI.KadisonSimilarity.DihedralSpectralArcInput