OAI/Combinatorics/ThinTrees/Selection.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrongThinTree.Geometry.antipode line 16
  2. lemma OAI.StrongThinTree.Geometry.binary_antipode line 18
  3. lemma OAI.StrongThinTree.Geometry.radial_complement line 22
  4. lemma OAI.StrongThinTree.Geometry.radial_max line 38
  5. lemma OAI.StrongThinTree.Geometry.binary_radial_move line 43
  6. lemma OAI.StrongThinTree.Geometry.RadialShell.ball_meets_radial line 100
  7. def OAI.StrongThinTree.AssignedAccounting.base line 133
  8. def OAI.StrongThinTree.AssignedAccounting.fresh line 136
  9. def OAI.StrongThinTree.AssignedAccounting.theta line 138
  10. lemma OAI.StrongThinTree.AssignedAccounting.base_le_width line 140
  11. lemma OAI.StrongThinTree.AssignedAccounting.base_discard line 145
  12. lemma OAI.StrongThinTree.AssignedAccounting.fresh_lower line 150
  13. lemma OAI.StrongThinTree.AssignedAccounting.avoiding_carve line 153
  14. lemma OAI.StrongThinTree.AssignedAccounting.dense_carve line 163
  15. lemma OAI.StrongThinTree.AssignedAccounting.sparse_carve line 176
  16. lemma OAI.StrongThinTree.AssignedAccounting.shrink_cost line 189
  17. lemma OAI.StrongThinTree.AssignedAccounting.border_payment line 211
  18. lemma OAI.StrongThinTree.AssignedSelection.large_neighbor_class line 226
  19. lemma OAI.StrongThinTree.AssignedSelection.radial_range line 255
  20. lemma OAI.StrongThinTree.AssignedSelection.interior_neighbor_in_range line 284
  21. lemma OAI.StrongThinTree.AssignedSelection.dense_count line 294
  22. lemma OAI.StrongThinTree.AssignedSelection.sparse_width line 301