OAI/Combinatorics/HalvingLines/Windows.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PlanarHalving.TimeWindows.Window line 11
  2. def OAI.PlanarHalving.TimeWindows.carrier line 13
  3. lemma OAI.PlanarHalving.TimeWindows.measurable_carrier line 15
  4. def OAI.PlanarHalving.TimeWindows.time line 18
  5. lemma OAI.PlanarHalving.TimeWindows.time_lt_one line 27
  6. lemma OAI.PlanarHalving.TimeWindows.time_strictMono line 32
  7. def OAI.PlanarHalving.TimeWindows.cut line 39
  8. lemma OAI.PlanarHalving.TimeWindows.cut_le line 42
  9. lemma OAI.PlanarHalving.TimeWindows.cut_mono line 45
  10. lemma OAI.PlanarHalving.TimeWindows.lt_cut_iff line 51
  11. def OAI.PlanarHalving.TimeWindows.start line 72
  12. def OAI.PlanarHalving.TimeWindows.stop line 74
  13. lemma OAI.PlanarHalving.TimeWindows.start_le_stop line 77
  14. lemma OAI.PlanarHalving.TimeWindows.stop_le line 84
  15. lemma OAI.PlanarHalving.TimeWindows.mem_carrier_iff line 86
  16. def OAI.PlanarHalving.TimeWindows.length line 105
  17. lemma OAI.PlanarHalving.TimeWindows.start_add_length line 106
  18. lemma OAI.PlanarHalving.TimeWindows.length_card line 109
  19. lemma OAI.PlanarHalving.Limits.weightedAtoms_apply_finset line 138
  20. def OAI.PlanarHalving.Batches.System.vertexMeasure line 154
  21. def OAI.PlanarHalving.Batches.System.endpointMeasure line 158
  22. lemma OAI.PlanarHalving.Batches.System.vertexMeasure_apply line 162
  23. lemma OAI.PlanarHalving.Batches.System.endpointMeasure_apply line 179
  24. theorem OAI.PlanarHalving.Batches.System.atomic_cubed_bound line 196
  25. lemma OAI.PlanarHalving.TimeWindows.cut_time_error line 229
  26. lemma OAI.PlanarHalving.TimeWindows.length_error line 261
  27. lemma OAI.PlanarHalving.TimeWindows.length_tendsto line 282
  28. lemma OAI.PlanarHalving.TimeWindows.eventually_length_pos line 289
  29. lemma OAI.PlanarHalving.Directions.measure_zero_of_null_gaps line 304
  30. lemma OAI.PlanarHalving.Directions.interval_has_rat_interior line 326
  31. lemma OAI.PlanarHalving.Directions.ae_subsingleton line 336
  32. theorem OAI.PlanarHalving.Directions.exists_three_singletons line 356
  33. def OAI.PlanarHalving.Batches.System.timeWindow line 407
  34. lemma OAI.PlanarHalving.Batches.System.timeWindow_edges line 411
  35. def OAI.PlanarHalving.Batches.System.edgeTime line 414
  36. lemma OAI.PlanarHalving.Batches.System.timeWindow_mem line 417
  37. lemma OAI.PlanarHalving.Batches.System.edgeTime_distribution line 450