OAI/Combinatorics/HadwigerCounterexample/QueryConcentration.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Query Concentration

  1. structure OAI.HadwigerCounterexample.Program line 14
  2. def OAI.HadwigerCounterexample.Program.free line 23
  3. def OAI.HadwigerCounterexample.Program.showKey line 27
  4. def OAI.HadwigerCounterexample.Program.oexpect line 30
  5. theorem OAI.HadwigerCounterexample.forum_law line 34
  6. theorem OAI.HadwigerCounterexample.avg_bound1 line 39
  7. theorem OAI.HadwigerCounterexample.avg_cross_sq line 41
  8. theorem OAI.HadwigerCounterexample.avg_var line 48
  9. theorem OAI.HadwigerCounterexample.Program.oVar line 60
  10. def OAI.HadwigerCounterexample.Program.oFreq line 112
  11. theorem OAI.HadwigerCounterexample.Program.oTail line 117