OAI/Analysis/Cotype/Cube.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Cotype.sign_false line 8
  2. theorem OAI.Cotype.sign_true line 9
  3. theorem OAI.Cotype.sign_sq line 10
  4. theorem OAI.Cotype.sign_not line 11
  5. def OAI.Cotype.character line 15
  6. theorem OAI.Cotype.character_symm line 18
  7. theorem OAI.Cotype.character_sq line 24
  8. theorem OAI.Cotype.character_orthogonality line 32
  9. theorem OAI.Cotype.average_character_mul line 48
  10. def OAI.Cotype.fourier line 56
  11. theorem OAI.Cotype.fourier_inversion line 59
  12. theorem OAI.Cotype.parseval line 83