OAI/Geometry/PlaneColoring/BinaryPalettes.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanFiveColor.BinaryCenter line 9
  2. lemma OAI.EuclideanFiveColor.binary_alternation line 11
  3. lemma OAI.EuclideanFiveColor.binary_pair_distinct line 28
  4. lemma OAI.EuclideanFiveColor.binary_cover_real line 44
  5. lemma OAI.EuclideanFiveColor.binary_alternation_real line 48
  6. lemma OAI.EuclideanFiveColor.alternating_twostep line 55
  7. lemma OAI.EuclideanFiveColor.liftPalette_shift_periodic line 62
  8. lemma OAI.EuclideanFiveColor.binary_transport_invariant line 76
  9. lemma OAI.EuclideanFiveColor.binary_centers_separated line 123
  10. instance OAI.EuclideanFiveColor.anglesNontrivial line 153
  11. instance OAI.EuclideanFiveColor.angularMeasure_nullSingleton line 159
  12. lemma OAI.EuclideanFiveColor.binary_centers_countable line 167
  13. lemma OAI.EuclideanFiveColor.ae_not_binary_circle line 182
  14. lemma OAI.EuclideanFiveColor.exact_sample_isTrace line 190
  15. lemma OAI.EuclideanFiveColor.trace_positive_le_palette line 193
  16. lemma OAI.EuclideanFiveColor.trace_sample_ae line 197
  17. lemma OAI.EuclideanFiveColor.exact_sample_palette_fixed line 201
  18. lemma OAI.EuclideanFiveColor.typical_sample_palette line 213
  19. lemma OAI.EuclideanFiveColor.ae_circle_palette_exclusion line 218
  20. lemma OAI.EuclideanFiveColor.ae_circle_typicalSampling line 229
  21. lemma OAI.EuclideanFiveColor.two_complement_pred line 236
  22. lemma OAI.EuclideanFiveColor.circle_complement_binary line 243
  23. lemma OAI.EuclideanFiveColor.palette_triple_null line 252
  24. lemma OAI.EuclideanFiveColor.palette_cardinality line 260
  25. def OAI.EuclideanFiveColor.triangleAngle line 274
  26. lemma OAI.EuclideanFiveColor.triangleAngle_cos line 275
  27. lemma OAI.EuclideanFiveColor.triangleAngle_pos line 277
  28. lemma OAI.EuclideanFiveColor.triangleAngle_lt_pi line 278
  29. lemma OAI.EuclideanFiveColor.triangleAngle_ratio_irrational line 279
  30. lemma OAI.EuclideanFiveColor.triangle_rotation_ergodic line 285
  31. lemma OAI.EuclideanFiveColor.equal_triangleAngle_positive line 291
  32. lemma OAI.EuclideanFiveColor.circle_exp_sub_norm_sq line 326
  33. def OAI.EuclideanFiveColor.sourceTriangle line 332
  34. lemma OAI.EuclideanFiveColor.sourceTriangle_eq line 334
  35. lemma OAI.EuclideanFiveColor.sourceTriangle_pair line 343