OAI/Analysis/IrrationalRotation/Model/ConcreteSpectral.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Invariant233.vectorFugledeKadisonDeterminant line 13

    Also declared: ComparatorChallenges/IrrationalRotation.lean:428 (same declaration text).

  2. def OAI.Invariant233.IsVectorBrownMeasure line 17

    Also declared: ComparatorChallenges/IrrationalRotation.lean:432 (same declaration text).

  3. def OAI.Invariant233.operatorModulus line 22

    Also declared: ComparatorChallenges/IrrationalRotation.lean:437 (same declaration text).

  4. def OAI.Invariant233.HasCountablyAtomicSpectralType line 24

    Also declared: ComparatorChallenges/IrrationalRotation.lean:439 (same declaration text).

  5. def OAI.Invariant233.polarConjugate line 28

    Also declared: ComparatorChallenges/IrrationalRotation.lean:443 (same declaration text).

  6. def OAI.Invariant233.finitePolarAlgebra line 32

    Also declared: ComparatorChallenges/IrrationalRotation.lean:447 (same declaration text).

  7. def OAI.Invariant233.fullPolarAlgebra line 35

    Also declared: ComparatorChallenges/IrrationalRotation.lean:450 (same declaration text).

  8. def OAI.Invariant233.ProductPolarStructure line 38

    Also declared: ComparatorChallenges/IrrationalRotation.lean:453 (same declaration text).