OAI/Topology/CoarseAssembly/BilateralShift.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The separable Hilbert space and bilateral shift for the circle cycle

  1. abbrev OAI.CoarseAssembly.Analytic.CircleSequence line 14
  2. instance OAI.CoarseAssembly.Analytic.circleSequence_secondCountable line 16
  3. abbrev OAI.CoarseAssembly.Analytic.circleSequenceSpace line 25
  4. def OAI.CoarseAssembly.Analytic.reindexSequence line 33

    Source documentation

    Reindex square-summable integer sequences by a permutation.

    def reindexSequence (e : ℤ ≃ ℤ) (x : CircleSequence) : CircleSequence :=
…

    Mentions: OAI.CoarseAssembly.Analytic.CircleSequence

  5. theorem OAI.CoarseAssembly.Analytic.reindexSequence_norm line 39
  6. def OAI.CoarseAssembly.Analytic.reindexSequenceEquiv line 45
  7. def OAI.CoarseAssembly.Analytic.bilateralShiftEquiv line 55

    Source documentation

    The shift sends the basis vector at n to the basis vector at n+1.

    def bilateralShiftEquiv : CircleSequence ≃ₗᵢ[ℂ] CircleSequence :=
…

    Mentions: OAI.CoarseAssembly.Analytic.CircleSequence

  8. def OAI.CoarseAssembly.Analytic.bilateralShift line 58
  9. theorem OAI.CoarseAssembly.Analytic.bilateralShift_apply line 60
  10. theorem OAI.CoarseAssembly.Analytic.bilateralShift_unitary line 63