OAI/Combinatorics/HalvingLines/Partition.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarHalving.Limits.probability_overlap_bound line 12
  2. lemma OAI.PlanarHalving.Limits.finite_bad_cover_mass line 42
  3. theorem OAI.PlanarHalving.Limits.ae_exists_partition_small line 77
  4. lemma OAI.PlanarHalving.Limits.kernel_nullSingleton_of_cells line 143
  5. def OAI.PlanarHalving.UniformPartition.boundary line 169
  6. def OAI.PlanarHalving.UniformPartition.cell line 177
  7. lemma OAI.PlanarHalving.UniformPartition.cell_measurable line 181
  8. lemma OAI.PlanarHalving.UniformPartition.cell_lower line 185
  9. lemma OAI.PlanarHalving.UniformPartition.cell_upper line 190
  10. lemma OAI.PlanarHalving.UniformPartition.cell_upper_lt line 197
  11. lemma OAI.PlanarHalving.UniformPartition.cells_disjoint line 202
  12. lemma OAI.PlanarHalving.UniformPartition.mem_some_cell line 218
  13. lemma OAI.PlanarHalving.UniformPartition.cells_cover line 257
  14. lemma OAI.PlanarHalving.UniformPartition.cell_volume line 262
  15. lemma OAI.PlanarHalving.UniformPartition.cell_diameter_bound line 271
  16. def OAI.PlanarHalving.UniformPartition.index line 289
  17. lemma OAI.PlanarHalving.UniformPartition.mem_cell_index line 292
  18. lemma OAI.PlanarHalving.UniformPartition.index_eq line 295
  19. lemma OAI.PlanarHalving.UniformPartition.index_measurable line 302
  20. def OAI.PlanarHalving.UniformPartition.grid line 309
  21. lemma OAI.PlanarHalving.UniformPartition.grid_measurable line 311
  22. lemma OAI.PlanarHalving.UniformPartition.dist_grid line 314
  23. lemma OAI.PlanarHalving.UniformPartition.grid_tendsto line 326
  24. lemma OAI.PlanarHalving.UniformPartition.grid_pair_tendsto line 331
  25. lemma OAI.PlanarHalving.UniformPartition.integral_partition line 335
  26. lemma OAI.PlanarHalving.UniformPartition.integral_grid line 359
  27. lemma OAI.PlanarHalving.UniformPartition.integral_grid_pair line 369
  28. lemma OAI.PlanarHalving.UniformPartition.grid_tendsto_seq line 396
  29. lemma OAI.PlanarHalving.UniformPartition.riemann_tendsto line 403
  30. lemma OAI.PlanarHalving.Limits.measure_le_of_test line 426
  31. def OAI.PlanarHalving.Limits.weightedAtoms line 451
  32. lemma OAI.PlanarHalving.Limits.integral_weightedAtoms line 455
  33. lemma OAI.PlanarHalving.Limits.mass_weightedAtoms line 465
  34. def OAI.PlanarHalving.UniformPartition.gridPoint line 478
  35. lemma OAI.PlanarHalving.UniformPartition.grid_sum_le line 481
  36. lemma OAI.PlanarHalving.UniformPartition.normalized_perturbed_sum_le line 488
  37. lemma OAI.PlanarHalving.UniformPartition.perturbed_grid_limit_le_volume line 508