OAI/Combinatorics/Progressions/Geometry/CoordinateLeafCount.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.CoordinateDecisionTree.trace_eq_of_agree line 13
  2. theorem OAI.Erdos3.CoordinateDecisionTree.trace_outside line 26
  3. def OAI.Erdos3.CoordinateDecisionTree.traceCylinder line 40
  4. theorem OAI.Erdos3.CoordinateDecisionTree.traceCylinder_assignment line 44
  5. theorem OAI.Erdos3.CoordinateDecisionTree.traceCylinder_contains line 54
  6. theorem OAI.Erdos3.CoordinateDecisionTree.traceCylinder_contains_iff line 60
  7. def OAI.Erdos3.CoordinateDecisionTree.leafCylinders line 91
  8. theorem OAI.Erdos3.CoordinateDecisionTree.mem_leafCylinders line 96
  9. theorem OAI.Erdos3.CoordinateDecisionTree.leafCylinders_contains_iff line 102
  10. theorem OAI.Erdos3.CoordinateDecisionTree.leafCylinders_unique line 108
  11. theorem OAI.Erdos3.CoordinateDecisionTree.leafCylinders_indicator_sum line 115
  12. theorem OAI.Erdos3.CoordinateDecisionTree.leafCylinders_partition line 148
  13. theorem OAI.Erdos3.CoordinateDecisionTree.leafCylinders_partition_empty line 154
  14. theorem OAI.Erdos3.CoordinateDecisionTree.leafCylinders_mass_sum line 159
  15. theorem OAI.Erdos3.CoordinateDecisionTree.Valid.leaf_good line 182
  16. theorem OAI.Erdos3.CoordinateDecisionTree.Valid.leaf_card_le line 189
  17. theorem OAI.Erdos3.CoordinateDecisionTree.Valid.leafCylinders_subset_bounded line 194
  18. theorem OAI.Erdos3.CoordinateDecisionTree.Valid.leafCylinders_card_le_exp line 200
  19. def OAI.Erdos3.CoordinateDecisionTree.leafSourceAssignments line 208
  20. theorem OAI.Erdos3.CoordinateDecisionTree.mem_leafSourceAssignments line 213
  21. theorem OAI.Erdos3.CoordinateDecisionTree.Valid.leafSourceAssignments_card_le_exp line 219