OAI/Computability/FourierTransform/TensorFibers.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PowerSaving.Binary.choose_pivot line 12
  2. abbrev OAI.PowerSaving.Binary.Minus line 16
  3. def OAI.PowerSaving.Binary.peel line 18
  4. theorem OAI.PowerSaving.Binary.peel_shift line 28
  5. theorem OAI.PowerSaving.Binary.bit_flip line 40
  6. theorem OAI.PowerSaving.Binary.peel_dir line 43
  7. def OAI.PowerSaving.Binary.skySplit line 58
  8. def OAI.PowerSaving.Binary.peelBook line 65
  9. theorem OAI.PowerSaving.Binary.product_dir line 72
  10. lemma OAI.PowerSaving.Binary.act_dir line 86
  11. lemma OAI.PowerSaving.Binary.peel_act line 109
  12. lemma OAI.PowerSaving.Binary.act_shift line 116
  13. lemma OAI.PowerSaving.Binary.card_minus line 125