OAI/Combinatorics/HalvingLines/Directions.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PlanarHalving.Directions.Plane line 10
  2. def OAI.PlanarHalving.Directions.simplex line 12
  3. lemma OAI.PlanarHalving.Directions.simplex_ne_zero line 14
  4. lemma OAI.PlanarHalving.Directions.simplex_affine line 21
  5. def OAI.PlanarHalving.Directions.allowed line 26
  6. lemma OAI.PlanarHalving.Directions.allowed_convex line 31
  7. lemma OAI.PlanarHalving.Directions.allowed_disjoint line 45
  8. theorem OAI.PlanarHalving.Directions.three_allowed_directions line 57
  9. lemma OAI.PlanarHalving.TimeWindows.time_mem_cell line 79
  10. def OAI.PlanarHalving.TimeWindows.midpointGrid line 94
  11. lemma OAI.PlanarHalving.TimeWindows.midpointGrid_measurable line 96
  12. lemma OAI.PlanarHalving.TimeWindows.midpointGrid_dist line 99
  13. lemma OAI.PlanarHalving.TimeWindows.midpointGrid_tendsto line 102
  14. lemma OAI.PlanarHalving.TimeWindows.integral_midpointGrid line 110
  15. lemma OAI.PlanarHalving.TimeWindows.midpoint_riemann_tendsto line 118
  16. lemma OAI.PlanarHalving.TimeWindows.timeMeasure_tendsto line 131
  17. lemma OAI.PlanarHalving.Limits.restriction_limit_eq line 148
  18. lemma OAI.PlanarHalving.RankCoordinates.smoothed_eVariation line 199
  19. lemma OAI.PlanarHalving.RankCoordinates.sum_interval_eVariation line 210
  20. lemma OAI.PlanarHalving.Limits.map_weightedAtoms line 232
  21. lemma OAI.PlanarHalving.Batches.System.sum_edgeTime line 249
  22. lemma OAI.PlanarHalving.Batches.System.edgeTime_atoms line 258
  23. def OAI.PlanarHalving.Batches.System.labelTimeMeasure line 269
  24. lemma OAI.PlanarHalving.Batches.System.labelTimeMeasure_time line 273
  25. lemma OAI.PlanarHalving.Batches.System.labelTimeMeasure_space line 279
  26. lemma OAI.PlanarHalving.Batches.System.labelTimeMeasure_mass line 285
  27. lemma OAI.PlanarHalving.Batches.ConvexPath.x_monotone line 299
  28. lemma OAI.PlanarHalving.Batches.segment_fst_mem line 307
  29. lemma OAI.PlanarHalving.Batches.ConvexPath.sum_rank_oscillation line 315
  30. lemma OAI.PlanarHalving.Batches.System.sum_edges_le_paths line 355
  31. theorem OAI.PlanarHalving.Batches.System.rank_oscillation line 399