OAI/Analysis/Cotype/WalshExactPairing.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Cotype.average_const_smul line 12
  2. def OAI.Cotype.cubeTranslate line 17
  3. theorem OAI.Cotype.average_translate line 23
  4. theorem OAI.Cotype.cubeL2_translate line 27
  5. theorem OAI.Cotype.character_xor_left line 31
  6. theorem OAI.Cotype.character_pairing_twist line 36
  7. def OAI.Cotype.twistedPrimal line 46
  8. def OAI.Cotype.twistedDual line 50
  9. theorem OAI.Cotype.twistedPrimal_join line 55
  10. theorem OAI.Cotype.twistedDual_join line 60
  11. theorem OAI.Cotype.twistedPrimal_L2 line 64
  12. theorem OAI.Cotype.twistedDual_L2 line 75
  13. theorem OAI.Cotype.twistedPairing line 85
  14. theorem OAI.Cotype.exists_exact_amplified_pairing line 115