OAI/Combinatorics/HalvingLines/AtomicBounds.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarHalving.Batches.System.EdgeTrace.match_eq line 11
  2. lemma OAI.PlanarHalving.Batches.System.EdgeTrace.same_path line 26
  3. lemma OAI.PlanarHalving.Batches.System.convexOwner_of_trace line 42
  4. lemma OAI.PlanarHalving.Batches.System.tokenPath_bounds line 50
  5. lemma OAI.PlanarHalving.Batches.System.tokenPath_segment_owner line 60
  6. lemma OAI.PlanarHalving.Batches.System.exists_graph line 70
  7. structure OAI.PlanarHalving.Batches.System.FullGraphs line 128
  8. lemma OAI.PlanarHalving.Batches.System.fullGraphs_nonempty line 144
  9. def OAI.PlanarHalving.Batches.System.fullGraphs line 179
  10. lemma OAI.PlanarHalving.Batches.System.FullGraphs.unique_incidence line 183
  11. lemma OAI.PlanarHalving.RankCoordinates.sigmoid_scale_limit line 199
  12. lemma OAI.PlanarHalving.RankCoordinates.smoothed_scale_limit line 206
  13. theorem OAI.PlanarHalving.RankCoordinates.exists_smoothing_slot_error line 227
  14. lemma OAI.PlanarHalving.Limits.finiteMeasure_tendsto_apply line 251
  15. lemma OAI.PlanarHalving.Limits.finiteMeasure_tendsto_thickening line 269
  16. lemma OAI.PlanarHalving.Limits.cubed_bound_limit_closed line 277
  17. lemma OAI.PlanarHalving.Limits.cubed_bound_of_compact line 300
  18. lemma OAI.PlanarHalving.Limits.cubed_bound_limit line 320
  19. def OAI.PlanarHalving.Batches.System.window line 335
  20. lemma OAI.PlanarHalving.Batches.System.window_edges line 347
  21. lemma OAI.PlanarHalving.Batches.System.window_vertices line 353
  22. lemma OAI.PlanarHalving.Batches.System.windows_disjoint line 358
  23. lemma OAI.PlanarHalving.Batches.System.windows_slopes line 370
  24. lemma OAI.PlanarHalving.Batches.System.FullGraphs.disjoint_bands line 376
  25. theorem OAI.PlanarHalving.Limits.persistent_mass_zero line 388
  26. lemma OAI.PlanarHalving.PlaneGraph.Generic.not_vertex_on_openSegment line 417
  27. def OAI.PlanarHalving.PlaneGraph.Drawing.exteriorCrossings line 435
  28. lemma OAI.PlanarHalving.PlaneGraph.Drawing.exteriorCrossings_not_vertex line 441
  29. lemma OAI.PlanarHalving.PlaneGraph.Drawing.exteriorCrossings_unique line 450
  30. theorem OAI.PlanarHalving.Batches.System.window_coordinate line 481