OAI/Geometry/PlaneColoring/BinaryDynamics.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanFiveColor.binaryQ line 8
  2. def OAI.EuclideanFiveColor.binaryR line 9
  3. def OAI.EuclideanFiveColor.binaryB line 10
  4. def OAI.EuclideanFiveColor.binaryM line 11
  5. def OAI.EuclideanFiveColor.binaryCircleMap line 12
  6. lemma OAI.EuclideanFiveColor.binaryQ_range line 14
  7. lemma OAI.EuclideanFiveColor.binaryR_pos line 26
  8. lemma OAI.EuclideanFiveColor.binary_arctan_identity line 30
  9. lemma OAI.EuclideanFiveColor.binary_arctan_recip line 35
  10. lemma OAI.EuclideanFiveColor.binaryCircleMap_hasDeriv_t line 42
  11. lemma OAI.EuclideanFiveColor.binaryCircleMap_hasDeriv_d line 72
  12. lemma OAI.EuclideanFiveColor.periodic_reduce_to_period line 109
  13. lemma OAI.EuclideanFiveColor.compact_periodic_uniform line 114
  14. lemma OAI.EuclideanFiveColor.compact_periodic_bounded line 130
  15. lemma OAI.EuclideanFiveColor.binaryQ_contDiff line 148
  16. lemma OAI.EuclideanFiveColor.binaryB_contDiffAt line 151
  17. lemma OAI.EuclideanFiveColor.binaryM_contDiffAt line 164
  18. lemma OAI.EuclideanFiveColor.binaryB_periodic line 177
  19. lemma OAI.EuclideanFiveColor.binaryM_periodic line 180
  20. def OAI.EuclideanFiveColor.binaryE line 183
  21. lemma OAI.EuclideanFiveColor.binaryE_continuousAt line 184
  22. lemma OAI.EuclideanFiveColor.binaryB_hasDeriv_t line 187
  23. lemma OAI.EuclideanFiveColor.binaryE_periodic line 191
  24. lemma OAI.EuclideanFiveColor.binary_uniform_controls line 205
  25. lemma OAI.EuclideanFiveColor.binaryCircleMap_zero line 235
  26. lemma OAI.EuclideanFiveColor.binaryCircleMap_displacement line 241
  27. lemma OAI.EuclideanFiveColor.binaryR_zero line 256
  28. lemma OAI.EuclideanFiveColor.binaryB_zero line 261
  29. lemma OAI.EuclideanFiveColor.binaryM_zero line 263
  30. lemma OAI.EuclideanFiveColor.binaryB_zero_shift line 265
  31. lemma OAI.EuclideanFiveColor.binaryM_zero_shift line 271
  32. lemma OAI.EuclideanFiveColor.trig_two_large line 277
  33. lemma OAI.EuclideanFiveColor.sign_shift_large line 292
  34. lemma OAI.EuclideanFiveColor.binaryB_zero_large line 298
  35. lemma OAI.EuclideanFiveColor.binaryM_zero_large line 314
  36. lemma OAI.EuclideanFiveColor.expansion_alternation_false line 337
  37. def OAI.EuclideanFiveColor.binaryConjugate line 391
  38. lemma OAI.EuclideanFiveColor.binaryConjugate_hasDeriv line 393
  39. lemma OAI.EuclideanFiveColor.binaryCircleMap_advance line 397
  40. lemma OAI.EuclideanFiveColor.binary_dynamics_controls line 410
  41. lemma OAI.EuclideanFiveColor.binaryConjugate_step line 477
  42. lemma OAI.EuclideanFiveColor.binary_conjugates_invariant line 484
  43. lemma OAI.EuclideanFiveColor.binary_alternating_invariant_false line 497