OAI/Combinatorics/HadwigerCounterexample/FreeBlockFourier.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Free Block Fourier

  1. theorem OAI.HadwigerCounterexample.zavg line 14
  2. def OAI.HadwigerCounterexample.zhat line 36
  3. def OAI.HadwigerCounterexample.zchar line 38
  4. def OAI.HadwigerCounterexample.zim line 40
  5. theorem OAI.HadwigerCounterexample.vpsym line 44
  6. theorem OAI.HadwigerCounterexample.hat_eqn line 46
  7. theorem OAI.HadwigerCounterexample.z_atlas line 59
  8. theorem OAI.HadwigerCounterexample.zhat_replay line 65
  9. theorem OAI.HadwigerCounterexample.zchar_orth line 68
  10. theorem OAI.HadwigerCounterexample.zsplit_orth line 85
  11. theorem OAI.HadwigerCounterexample.zsplit_cost line 92