OAI/Analysis/FiniteFactor/CrossedProduct/TorusOperatorField.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteFactor.sourceTorusOperatorField line 12

    Source documentation

    The proved source field on the actual compact sampling torus.

    def sourceTorusOperatorField
    (H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate) (z : SourceTorus) :
    SourceFiberHilbert →L[ℂ] SourceFiberHilbert :=
…

    Mentions: OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceTorus, OAI.FiniteFactor.SourceFiberHilbert

  2. theorem OAI.FiniteFactor.sourceTorusOperatorField_stronglyMeasurable line 17
  3. theorem OAI.FiniteFactor.sourceTorusOperatorField_norm line 23
  4. theorem OAI.FiniteFactor.sourceTorusOperatorField_projection line 27
  5. theorem OAI.FiniteFactor.sourceTorusOperatorField_invariant line 34
  6. theorem OAI.FiniteFactor.sourceTorusOperatorField_sourceOperator_pow line 43