OAI/Topology/CoarseAssembly/NegativeProjection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The negative-frequency projection for the circle cycle

  1. def OAI.CoarseAssembly.Analytic.negativeCoordinate line 12
  2. theorem OAI.CoarseAssembly.Analytic.negativeCoordinate_norm line 14
  3. def OAI.CoarseAssembly.Analytic.negativeProjection line 20
  4. theorem OAI.CoarseAssembly.Analytic.negativeProjection_apply line 23
  5. theorem OAI.CoarseAssembly.Analytic.negativeProjection_sq line 29
  6. theorem OAI.CoarseAssembly.Analytic.negativeProjection_selfAdjoint line 38
  7. theorem OAI.CoarseAssembly.Analytic.negativeProjection_commutator line 49

    Source documentation

    The projection/shift commutator has exactly one nonzero row.

    theorem negativeProjection_commutator (x : CircleSequence) :
    (negativeProjection * bilateralShift - bilateralShift * negativeProjection) x =
      -lp.single 2 0 (x (-1)) := by
…

    Mentions: OAI.CoarseAssembly.Analytic.CircleSequence, OAI.CoarseAssembly.Analytic.negativeProjection, OAI.CoarseAssembly.Analytic.bilateralShift

  8. theorem OAI.CoarseAssembly.Analytic.negativeProjection_commutator_compact line 66