OAI/Geometry/PlaneColoring/DiskAverages.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanFiveColor.diskLaw line 9
  2. lemma OAI.EuclideanFiveColor.diskLaw_absolutelyContinuous line 11
  3. lemma OAI.EuclideanFiveColor.diskLaw_probability line 13
  4. def OAI.EuclideanFiveColor.colorFn line 18
  5. lemma OAI.EuclideanFiveColor.colorFn_measurable line 19
  6. lemma OAI.EuclideanFiveColor.colorFn_nonneg line 22
  7. lemma OAI.EuclideanFiveColor.colorFn_le_one line 24
  8. lemma OAI.EuclideanFiveColor.colorFn_integrable line 26
  9. def OAI.EuclideanFiveColor.diskAverage line 33
  10. lemma OAI.EuclideanFiveColor.diskAverage_nonneg line 35
  11. lemma OAI.EuclideanFiveColor.diskAverage_le_one line 37
  12. lemma OAI.EuclideanFiveColor.diskAverage_sum line 42
  13. lemma OAI.EuclideanFiveColor.colorFn_unit_pair line 48
  14. lemma OAI.EuclideanFiveColor.diskAverage_unit_pair line 63
  15. lemma OAI.EuclideanFiveColor.volumeReal_ball line 77
  16. lemma OAI.EuclideanFiveColor.diskAverage_area line 79
  17. lemma OAI.EuclideanFiveColor.ball_ne_top line 97
  18. lemma OAI.EuclideanFiveColor.symmDiff_balls_subset_annulus line 99
  19. lemma OAI.EuclideanFiveColor.measure_inter_ball_difference line 120
  20. lemma OAI.EuclideanFiveColor.diskAverage_lipschitz line 141
  21. lemma OAI.EuclideanFiveColor.colorFn_norm_le_one line 168
  22. lemma OAI.EuclideanFiveColor.diskAverage_product line 171
  23. lemma OAI.EuclideanFiveColor.disk_overlap_swap line 176
  24. lemma OAI.EuclideanFiveColor.root_overlap_bound line 192
  25. lemma OAI.EuclideanFiveColor.root_overlap_zero line 238
  26. lemma OAI.EuclideanFiveColor.missing_edge_uniform line 253
  27. lemma OAI.EuclideanFiveColor.diskLaw_mem_ball line 276
  28. lemma OAI.EuclideanFiveColor.disk_overlap_bound line 279
  29. lemma OAI.EuclideanFiveColor.missing_edge_overlap line 307