OAI/Combinatorics/HalvingLines/BoundaryTokens.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarHalving.Boundary.monotone_pred_changes line 11
  2. def OAI.PlanarHalving.Boundary.InSquare line 27
  3. lemma OAI.PlanarHalving.Boundary.monotone_square_changes line 29
  4. lemma OAI.PlanarHalving.Boundary.square_token_budget line 56
  5. def OAI.PlanarHalving.Boundary.rawNormal line 80
  6. def OAI.PlanarHalving.Boundary.frameWeight line 81
  7. def OAI.PlanarHalving.Boundary.frameParameter line 82
  8. lemma OAI.PlanarHalving.Boundary.frameWeight_pos line 84
  9. lemma OAI.PlanarHalving.Boundary.frameParameter_mem line 92
  10. lemma OAI.PlanarHalving.Boundary.frameParameter_monotone line 101
  11. lemma OAI.PlanarHalving.Boundary.frame_apply line 109
  12. lemma OAI.PlanarHalving.Boundary.frame_projection line 116
  13. lemma OAI.PlanarHalving.Boundary.frame_inverse_nonneg line 126
  14. lemma OAI.PlanarHalving.Boundary.rawNormal_bounds line 146
  15. lemma OAI.PlanarHalving.Boundary.rawNormal_difference line 149
  16. lemma OAI.PlanarHalving.Boundary.separating_threshold line 152
  17. def OAI.PlanarHalving.Boundary.physical line 183
  18. lemma OAI.PlanarHalving.Boundary.physical_sub line 186
  19. lemma OAI.PlanarHalving.Boundary.physical_injective line 192
  20. lemma OAI.PlanarHalving.Boundary.projection_physical line 198
  21. lemma OAI.PlanarHalving.Boundary.actual_transformed_cuts line 210
  22. lemma OAI.PlanarHalving.Boundary.actual_tokens_monotone line 227
  23. def OAI.PlanarHalving.Boundary.clipCut line 267
  24. lemma OAI.PlanarHalving.Boundary.clipCut_mem line 268
  25. lemma OAI.PlanarHalving.Boundary.clipCut_distance line 270
  26. lemma OAI.PlanarHalving.Boundary.rawNormal_dot_bound line 283
  27. lemma OAI.PlanarHalving.Boundary.finite_raw_bound line 295
  28. lemma OAI.PlanarHalving.Spatial.strip_bound_of_disk_nonneg line 385
  29. lemma OAI.PlanarHalving.Spatial.normalize_sqNorm line 412
  30. lemma OAI.PlanarHalving.Spatial.raw_strip_bound line 420
  31. lemma OAI.PlanarHalving.Limits.eventually_gt_open line 456
  32. lemma OAI.PlanarHalving.Limits.open_le_of_eventually_le line 473