OAI/Combinatorics/HadwigerCounterexample/BilinearCompression.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Bilinear Compression

  1. def OAI.HadwigerCounterexample.dqBound line 14
  2. theorem OAI.HadwigerCounterexample.pullM_fix line 16
  3. def OAI.HadwigerCounterexample.dualSpace line 23
  4. theorem OAI.HadwigerCounterexample.dualSpace_dim line 25
  5. def OAI.HadwigerCounterexample.jointShrink line 31
  6. theorem OAI.HadwigerCounterexample.joint_ip line 36
  7. theorem OAI.HadwigerCounterexample.shrink_pure line 46