OAI/Combinatorics/HalvingLines/WindowMeasures.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarHalving.RankLimits.Data.conditional line 11
  2. instance OAI.PlanarHalving.RankLimits.(instance at line 13) line 13
  3. lemma OAI.PlanarHalving.RankLimits.Data.edge_toMeasure line 17
  4. lemma OAI.PlanarHalving.RankLimits.Data.conditional_measurable line 21
  5. lemma OAI.PlanarHalving.RankLimits.Converges.conditional_integral line 25
  6. lemma OAI.PlanarHalving.RankLimits.Converges.edgeWindow_mass line 41
  7. lemma OAI.PlanarHalving.RankLimits.Data.conditional_le_one line 53
  8. lemma OAI.PlanarHalving.RankLimits.Data.conditional_sum line 57
  9. lemma OAI.PlanarHalving.Sweep.activity_family_cubic line 70
  10. lemma OAI.PlanarHalving.Sweep.cubic_to_tail line 107
  11. lemma OAI.PlanarHalving.Batches.System.vertices_subset_activity line 125
  12. structure OAI.PlanarHalving.RankLimits.Configuration.SweepEmbedding line 158
  13. def OAI.PlanarHalving.RankLimits.Configuration.SweepEmbedding.start line 164
  14. def OAI.PlanarHalving.RankLimits.Configuration.SweepEmbedding.stop line 166
  15. lemma OAI.PlanarHalving.RankLimits.Configuration.SweepEmbedding.start_le_stop line 169
  16. lemma OAI.PlanarHalving.RankLimits.Configuration.SweepEmbedding.stop_le_start line 172
  17. lemma OAI.PlanarHalving.RankLimits.Configuration.SweepEmbedding.vertices_subset line 176
  18. lemma OAI.PlanarHalving.RankLimits.before_of_same_depth line 194
  19. lemma OAI.PlanarHalving.RankLimits.Configuration.SweepEmbedding.windows_disjoint line 199
  20. lemma OAI.PlanarHalving.RankLimits.Configuration.SweepEmbedding.activity_tail line 206
  21. lemma OAI.PlanarHalving.RankLimits.Converges.activity_tail line 243
  22. def OAI.PlanarHalving.RankLimits.timePartition line 265
  23. lemma OAI.PlanarHalving.RankLimits.timePartition_card line 268
  24. lemma OAI.PlanarHalving.RankLimits.timePartition_cover line 272
  25. lemma OAI.PlanarHalving.RankLimits.sum_timePartition line 279
  26. lemma OAI.PlanarHalving.RankLimits.filter_timePartition line 284
  27. lemma OAI.PlanarHalving.RankLimits.Converges.conditional_nullSingleton line 289
  28. def OAI.PlanarHalving.PlaneGraph.Drawing.pointOfPair line 333
  29. lemma OAI.PlanarHalving.PlaneGraph.Drawing.pointOfPair_eq line 337
  30. lemma OAI.PlanarHalving.Batches.System.restricted_crossing line 348
  31. def OAI.PlanarHalving.Batches.System.crossingsIn line 366
  32. lemma OAI.PlanarHalving.Batches.System.windowCrossMeasure_apply line 371
  33. lemma OAI.PlanarHalving.Batches.System.retained_crossing_cover line 395
  34. lemma OAI.PlanarHalving.Batches.System.retained_crossing_bound line 426