OAI/Combinatorics/HalvingLines/RankMeasures.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.PlanarHalving.RankLimits.MeasureIndex line 11
  2. abbrev OAI.PlanarHalving.RankLimits.LimitSpace line 19
  3. instance OAI.PlanarHalving.RankLimits.(instance at line 26) line 26
  4. instance OAI.PlanarHalving.RankLimits.(instance at line 28) line 28
  5. instance OAI.PlanarHalving.RankLimits.(instance at line 30) line 30
  6. instance OAI.PlanarHalving.RankLimits.(instance at line 32) line 32
  7. instance OAI.PlanarHalving.RankLimits.(instance at line 34) line 34
  8. def OAI.PlanarHalving.RankLimits.Configuration.measures line 37
  9. lemma OAI.PlanarHalving.RankLimits.Configuration.measures_mass_le line 44
  10. structure OAI.PlanarHalving.RankLimits.Data line 53
  11. def OAI.PlanarHalving.RankLimits.Data.ofFamily line 60
  12. structure OAI.PlanarHalving.RankLimits.Converges line 67
  13. theorem OAI.PlanarHalving.RankLimits.subsequence line 74
  14. lemma OAI.PlanarHalving.RankLimits.Converges.points_mass line 81
  15. lemma OAI.PlanarHalving.RankLimits.Converges.edgeTime_mass line 86
  16. lemma OAI.PlanarHalving.RankLimits.Converges.time_marginal line 92
  17. lemma OAI.PlanarHalving.UniformPartition.normalized_perturbed_fintype_sum_le line 107
  18. lemma OAI.PlanarHalving.UniformPartition.perturbed_fintype_grid_limit line 119
  19. lemma OAI.PlanarHalving.RankLimits.Converges.crossing_projection line 157
  20. lemma OAI.PlanarHalving.UniformPartition.volume_frontier_cell line 184
  21. lemma OAI.PlanarHalving.RankLimits.Converges.null_time_boundary line 211
  22. lemma OAI.PlanarHalving.RankLimits.Converges.restriction_eq line 221
  23. def OAI.PlanarHalving.RankLimits.Data.edge line 227
  24. def OAI.PlanarHalving.RankLimits.Data.edgeWindow line 228
  25. lemma OAI.PlanarHalving.RankLimits.Converges.restriction_mass line 231
  26. lemma OAI.PlanarHalving.Batches.System.window_endpoint_eq line 250
  27. lemma OAI.PlanarHalving.Batches.System.vertexMass_ratio line 287
  28. def OAI.PlanarHalving.RankLimits.Configuration.edgeWindow line 297
  29. lemma OAI.PlanarHalving.RankLimits.Configuration.edgeWindow_eq line 300
  30. lemma OAI.PlanarHalving.RankLimits.Configuration.vertices_mass_ratio line 304
  31. lemma OAI.PlanarHalving.RankLimits.Configuration.window_cubed_bound line 309
  32. def OAI.PlanarHalving.Batches.System.rankGraphs line 326
  33. lemma OAI.PlanarHalving.Batches.System.rankGraphs_eq line 331
  34. def OAI.PlanarHalving.Batches.System.rankCoordinate line 336
  35. lemma OAI.PlanarHalving.Batches.System.rankCoordinate_value line 343
  36. def OAI.PlanarHalving.Batches.System.rankHomeomorph line 349
  37. lemma OAI.PlanarHalving.Batches.System.rankHomeomorph_coordinates line 355
  38. def OAI.PlanarHalving.Batches.System.rankInCoordinates line 362
  39. lemma OAI.PlanarHalving.Batches.System.rankInCoordinates_eq line 367
  40. lemma OAI.PlanarHalving.Batches.System.rankInCoordinates_before line 376
  41. lemma OAI.PlanarHalving.Batches.System.rankInCoordinates_between line 386
  42. lemma OAI.PlanarHalving.Batches.System.rankInCoordinates_after line 396
  43. lemma OAI.PlanarHalving.Limits.measure_le_of_weak_limits line 411
  44. lemma OAI.PlanarHalving.RankLimits.Configuration.vertices_le_points line 430
  45. lemma OAI.PlanarHalving.RankLimits.Converges.vertices_le_points line 444
  46. lemma OAI.PlanarHalving.RankLimits.Converges.edgeWindow line 448
  47. lemma OAI.PlanarHalving.RankLimits.Converges.local_cubic line 452
  48. lemma OAI.PlanarHalving.RankLimits.Converges.window_absolutelyContinuous line 479
  49. lemma OAI.PlanarHalving.RankLimits.Configuration.normalization_coefficient line 509
  50. lemma OAI.PlanarHalving.RankLimits.Configuration.short_ratio_cube line 517
  51. lemma OAI.PlanarHalving.RankLimits.short_ratio_tendsto_zero line 529
  52. lemma OAI.PlanarHalving.RankLimits.sparse_error_tendsto_zero line 546
  53. lemma OAI.PlanarHalving.RankLimits.normalization_sizes_atTop line 561