OAI/Combinatorics/HadwigerCounterexample/BilinearBlockCorrelation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Bilinear Block Correlation

  1. def OAI.HadwigerCounterexample.spring line 14
  2. theorem OAI.HadwigerCounterexample.spring_update line 17
  3. def OAI.HadwigerCounterexample.dotLB line 32
  4. theorem OAI.HadwigerCounterexample.spark_walsh line 39
  5. theorem OAI.HadwigerCounterexample.spark_uncap line 66