OAI/Analysis/KadisonKastler/StrongUnitaryCoordinates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A closed Polish coordinate model of the unitary group

Both the operator and its adjoint are evaluated on a fixed dense sequence. The range is closed: coordinate limits extend to contractions, and the inverse and adjoint identities pass to strong limits.

  1. def OAI.KadisonKastler.unitaryCoordinates line 23
  2. theorem OAI.KadisonKastler.unitaryCoordinates_injective line 27
  3. theorem OAI.KadisonKastler.unitary_norm_le_one line 35
  4. theorem OAI.KadisonKastler.isClosed_range_unitaryCoordinates line 41
  5. def OAI.KadisonKastler.StrongUnitarySpace line 111

    Source documentation

    This is the strong-star coordinate model, not the operator-norm topology.

    def StrongUnitarySpace (ξ : ℕ → H) := Set.range (unitaryCoordinates ξ)

    Mentions: OAI.KadisonKastler.unitaryCoordinates

  6. instance OAI.KadisonKastler.(instance at line 113) line 113
  7. instance OAI.KadisonKastler.(instance at line 116) line 116
  8. theorem OAI.KadisonKastler.strongUnitarySpace_polish line 119