OAI/Analysis/IrrationalRotation/Sampling/ProductCharacters.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InvariantProjection.ProductRotation.characterPhase_zero line 13
  2. theorem OAI.InvariantProjection.ProductRotation.characterPhase_add line 17
  3. theorem OAI.InvariantProjection.ProductRotation.characterPhase_add_index line 21
  4. theorem OAI.InvariantProjection.ProductRotation.characterPhase_single line 26
  5. theorem OAI.InvariantProjection.ProductRotation.productCharacter_zero line 30
  6. theorem OAI.InvariantProjection.ProductRotation.productCharacter_add line 34
  7. theorem OAI.InvariantProjection.ProductRotation.productCharacter_add_index line 38
  8. theorem OAI.InvariantProjection.ProductRotation.productCharacter_single_one line 43
  9. theorem OAI.InvariantProjection.ProductRotation.productCharacter_neg line 47
  10. theorem OAI.InvariantProjection.ProductRotation.productFourierAlgebra_separatesPoints line 54
  11. theorem OAI.InvariantProjection.ProductRotation.productFourierAlgebra_closure_eq_top line 67
  12. theorem OAI.InvariantProjection.ProductRotation.productFourierAlgebra_toSubmodule line 72
  13. theorem OAI.InvariantProjection.ProductRotation.span_productCharacter_closure_eq_top line 94
  14. theorem OAI.InvariantProjection.ProductRotation.mul_sum_ne_int line 100
  15. theorem OAI.InvariantProjection.ProductRotation.characterPhase_coe line 111
  16. theorem OAI.InvariantProjection.ProductRotation.productCharacter_ne_one line 123
  17. theorem OAI.InvariantProjection.ProductRotation.product_rotation_free line 139
  18. theorem OAI.InvariantProjection.ProductRotation.productCharacter_translation line 156