OAI/Topology/CoarseAssembly/CircleSequenceRepresentation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Continuous circle functions represented by the bilateral shift

  1. def OAI.CoarseAssembly.Analytic.circleCoordinate line 15
  2. theorem OAI.CoarseAssembly.Analytic.bilateralShift_mem_unitary line 17
  3. theorem OAI.CoarseAssembly.Analytic.bilateralShift_spectrum_circle line 20
  4. def OAI.CoarseAssembly.Analytic.circleRepresentation line 27

    Source documentation

    Continuous functional calculus of the actual bilateral shift.

    def circleRepresentation : C(Circle, ℂ) →⋆ₐ[ℂ] End circleSequenceSpace :=
…

    Mentions: OAI.CoarseAssembly.Analytic.End, OAI.CoarseAssembly.Analytic.circleSequenceSpace

  5. theorem OAI.CoarseAssembly.Analytic.circleRepresentation_coordinate line 30