OAI/Geometry/PlaneColoring/PaletteDensity.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.EuclideanFiveColor.weak_strong_disjoint line 9
  2. def OAI.EuclideanFiveColor.colorIndicator line 80
  3. lemma OAI.EuclideanFiveColor.colorIndicator_measurable line 82
  4. lemma OAI.EuclideanFiveColor.colorIndicator_bounds line 84
  5. lemma OAI.EuclideanFiveColor.sample_pair_disjoint line 87
  6. lemma OAI.EuclideanFiveColor.trace_pair_disjoint line 105
  7. lemma OAI.EuclideanFiveColor.palette_first_exclusion line 121
  8. lemma OAI.EuclideanFiveColor.palette_second_exclusion line 135
  9. lemma OAI.EuclideanFiveColor.palette_transfer_pair line 143
  10. lemma OAI.EuclideanFiveColor.angleMk_quasiMeasurePreserving line 158
  11. lemma OAI.EuclideanFiveColor.anglePair_quasiMeasurePreserving line 178
  12. def OAI.EuclideanFiveColor.FlatDensityZero line 190
  13. def OAI.EuclideanFiveColor.LineDensityZero line 192
  14. lemma OAI.EuclideanFiveColor.volume_image_bound line 194
  15. lemma OAI.EuclideanFiveColor.FlatDensityZero.mono_ae line 212
  16. lemma OAI.EuclideanFiveColor.flatDensityZero_prod line 220
  17. lemma OAI.EuclideanFiveColor.tendsto_pos_mul_nhdsWithin line 233
  18. lemma OAI.EuclideanFiveColor.FlatDensityZero.image line 240
  19. lemma OAI.EuclideanFiveColor.FlatDensityZero.of_locally_le line 278
  20. lemma OAI.EuclideanFiveColor.FlatDensityZero.transport line 291
  21. lemma OAI.EuclideanFiveColor.circleSum_one_lipschitz line 314
  22. lemma OAI.EuclideanFiveColor.circleSum_densityZero line 328
  23. lemma OAI.EuclideanFiveColor.complex_ball_flat_ball line 361
  24. lemma OAI.EuclideanFiveColor.flat_to_complex_densityZero line 367
  25. lemma OAI.EuclideanFiveColor.flat_density_not_one line 397
  26. lemma OAI.EuclideanFiveColor.ae_lineDensityZero_compl line 409
  27. def OAI.EuclideanFiveColor.liftPalette line 431
  28. lemma OAI.EuclideanFiveColor.liftPalette_measurable line 433
  29. lemma OAI.EuclideanFiveColor.palette_spatial_densityZero line 435
  30. lemma OAI.EuclideanFiveColor.palette_spatial_not_densityOne line 451
  31. lemma OAI.EuclideanFiveColor.palette_sample_branch_exclusion line 463