OAI/Combinatorics/HalvingLines/MeasureBounds.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarHalving.card_filter_attached line 8
  2. def OAI.PlanarHalving.RankLimits.Configuration.longEdges line 20
  3. lemma OAI.PlanarHalving.RankLimits.Configuration.longEdges_bound line 24
  4. lemma OAI.PlanarHalving.RankLimits.longEdges_ratio_zero line 46
  5. lemma OAI.PlanarHalving.RankLimits.Configuration.short_edge_label line 63
  6. lemma OAI.PlanarHalving.Limits.eventually_lt_closed line 85
  7. lemma OAI.PlanarHalving.Limits.eventually_thickening_lower line 99
  8. lemma OAI.PlanarHalving.RankLimits.Configuration.edgeWindow_apply line 118
  9. lemma OAI.PlanarHalving.RankLimits.Configuration.windows_edges_disjoint line 130
  10. def OAI.PlanarHalving.RankLimits.Configuration.selectedEdges line 140
  11. lemma OAI.PlanarHalving.RankLimits.Configuration.selectedEdges_mass line 145
  12. lemma OAI.PlanarHalving.RankLimits.Configuration.selectedEdges_subset line 158
  13. lemma OAI.PlanarHalving.RankLimits.Configuration.retained_near line 165
  14. lemma OAI.PlanarHalving.RankLimits.Configuration.retained_mass_lower line 178
  15. lemma OAI.PlanarHalving.Limits.eventually_sum_lower line 201
  16. lemma OAI.PlanarHalving.Limits.eventually_sum_upper line 214
  17. lemma OAI.PlanarHalving.Limits.cubic_of_eventual_bounds line 223
  18. lemma OAI.PlanarHalving.RankLimits.Configuration.retained_cubic line 249
  19. lemma OAI.PlanarHalving.RankLimits.Converges.partition_cubic_thickening line 283
  20. lemma OAI.PlanarHalving.Limits.finiteMeasure_tendsto_cthickening line 338
  21. lemma OAI.PlanarHalving.RankLimits.Data.partitionQuantity_tendsto line 350
  22. lemma OAI.PlanarHalving.RankLimits.Converges.partition_cubic_closed line 365
  23. lemma OAI.PlanarHalving.UniformPartition.cell_refinement line 387
  24. lemma OAI.PlanarHalving.UniformPartition.exists_cell_refinement line 425
  25. lemma OAI.PlanarHalving.TimeWindows.carrier_refinement line 435
  26. lemma OAI.PlanarHalving.TimeWindows.same_depth_disjoint line 439
  27. lemma OAI.PlanarHalving.TimeWindows.refining_cell_subset line 442
  28. def OAI.PlanarHalving.RankLimits.localPartition line 458
  29. lemma OAI.PlanarHalving.RankLimits.mem_timePartition line 461
  30. lemma OAI.PlanarHalving.RankLimits.timePartition_disjoint line 472
  31. lemma OAI.PlanarHalving.RankLimits.localPartition_cover line 482
  32. lemma OAI.PlanarHalving.RankLimits.localPartition_disjoint line 487
  33. lemma OAI.PlanarHalving.RankLimits.Converges.edgeWindow_apply line 497
  34. lemma OAI.PlanarHalving.RankLimits.Converges.localPartition_sum line 506