OAI/Analysis/Unitarizability/Unitarizer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The bounded implementer forced by a unitarizing similarity. The commuting projection onto H ⊕ 0 has upper-right block equal to the negative implementer, avoiding a bounded inverse for graph coordinates.

  1. theorem OAI.Dixmier.Triangular.implementer_of_similar line 16

    Source documentation

    A global cocycle implementer obtained from the similarity itself.

    theorem implementer_of_similar (U : G →* (H →L[ℂ] H)) (D : G → (H →L[ℂ] H))
    (h1 : D 1 = 0) (hD : ∀ g h, D (g*h) = D g + conjugate U g (D h))
    (hπ : SimilarToUnitary (representation U D h1 hD)) :
    ∃ B : H →L[ℂ] H, ∀ g, D g = coboundary U B g := by
…

    Mentions: OAI.Dixmier.conjugate, OAI.Dixmier.SimilarToUnitary, OAI.Dixmier.Triangular.representation, OAI.Dixmier.coboundary