OAI/Analysis/IrrationalRotation/Spectral/ProductFinitePolar.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.ProductModel.rotationIterate_measurePreserving_polar line 13
  2. abbrev OAI.Invariant233.ProductModel.signedShift line 30
  3. theorem OAI.Invariant233.ProductModel.shiftOperator_star_eq line 33
  4. theorem OAI.Invariant233.ProductModel.shiftOperator_pow_eq line 45
  5. theorem OAI.Invariant233.ProductModel.star_shiftOperator_pow_eq line 55
  6. theorem OAI.Invariant233.ProductModel.polarConjugate_eq_signedShift line 64
  7. theorem OAI.Invariant233.ProductModel.multiplier_coordinate_ae line 72
  8. theorem OAI.Invariant233.ProductModel.polarConjugate_multiplier_coordinate_ae line 78
  9. theorem OAI.Invariant233.ProductModel.finitePolarAlgebra_multiplier_atomic line 93
  10. theorem OAI.Invariant233.ProductModel.fullPolarAlgebra_multiplier_abelian line 124
  11. theorem OAI.Invariant233.ProductModel.multiplier_hasCountablyAtomicSpectralType line 141
  12. theorem OAI.Invariant233.ProductModel.multiplier_injective_of_ae_ne_zero line 167