TracialDihedralEndgame.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The Fourier matrix computed on the actual dihedral columns is the same matrix tested by the repeated-word propagation estimate.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.commutator_bound_of_actual_dihedral_compression line 25

Source documentation

The exact Fourier compression of the actual normalized columns, together with the derived multiplicity propagation bounds, controls the base symmetry.

theorem commutator_bound_of_actual_dihedral_compression
    (hτ : G.trace 1 = 1) (hf : ScalarFree G.trace D A)
    (d : D) (s : A) (e : D)
    (hdstar : star d = d) (hdsq : d * d = 1) (hd0 : G.trace (d : P) = 0)
    (hsstar : star s = s) (hssq : s * s = 1) (hs0 : G.trace (s : P) = 0)
    (he : IsStarProjection e) {t : ℝ} (ht : 0 < t) (hte : G.trace (e : P) = (t : ℂ))
    (U : OrthogonalWordLevels
      (MultiplicityWordSpace (WordMultiplicity (G.baseVector A 1)) (G.baseSpace D)
        (centeredSubspace (G.baseVector D 1))) H)
    (hU : TracialWordFormula G A D U)
    (Y T : H →L[ℂ] H)
    (B : ∀ n, WordMultiplicity (G.baseVector A 1) n →L[ℂ]
…

Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.OrthogonalWordLevels, OAI.KadisonSimilarity.MultiplicityWordSpace, OAI.KadisonSimilarity.WordMultiplicity, OAI.KadisonSimilarity.centeredSubspace, OAI.KadisonSimilarity.TracialWordFormula