OAI/Geometry/PlaneColoring/Moser.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanFiveColor.ThreeLabelRegion line 7
  2. lemma OAI.EuclideanFiveColor.square_coordinate_bounds line 10
  3. lemma OAI.EuclideanFiveColor.region_of_rational_bounds line 24
  4. lemma OAI.EuclideanFiveColor.abs_le_of_bounds line 42
  5. lemma OAI.EuclideanFiveColor.sin_sub_add_product line 50
  6. lemma OAI.EuclideanFiveColor.sin_three_using_cos line 57
  7. lemma OAI.EuclideanFiveColor.polynomial_region_angles line 62

    Source documentation

    Exact strict angular form of the manuscript's polynomial region.

    lemma polynomial_region_angles {z : ℂ} (hz : ThreeLabelRegion z.re z.im) :
    ∃ t u : ℝ, (Circle.exp t : ℂ)+(Circle.exp u : ℂ)=z ∧
      Real.sin (u-t)≠0 ∧ Real.sin (3*t)*Real.sin (3*u)<0 := by
…

    Mentions: OAI.EuclideanFiveColor.ThreeLabelRegion

  8. def OAI.EuclideanFiveColor.moserA line 128
  9. def OAI.EuclideanFiveColor.moserB line 129
  10. def OAI.EuclideanFiveColor.moserT line 130
  11. def OAI.EuclideanFiveColor.moserU line 131
  12. def OAI.EuclideanFiveColor.moserPoint line 132
  13. lemma OAI.EuclideanFiveColor.moserPoint_0 line 133
  14. lemma OAI.EuclideanFiveColor.moserPoint_1 line 134
  15. lemma OAI.EuclideanFiveColor.moserPoint_2 line 135
  16. lemma OAI.EuclideanFiveColor.moserPoint_3 line 136
  17. lemma OAI.EuclideanFiveColor.moserPoint_4 line 137
  18. lemma OAI.EuclideanFiveColor.moserPoint_5 line 138
  19. lemma OAI.EuclideanFiveColor.moserPoint_6 line 139
  20. def OAI.EuclideanFiveColor.moserEdges line 140
  21. lemma OAI.EuclideanFiveColor.complex_norm_one_of_sq line 142
  22. lemma OAI.EuclideanFiveColor.moser_edge_unit line 145
  23. lemma OAI.EuclideanFiveColor.three_color_diamond line 156
  24. lemma OAI.EuclideanFiveColor.moser_not_three_colorable line 159
  25. def OAI.EuclideanFiveColor.moserRotation line 168
  26. def OAI.EuclideanFiveColor.placedMoser line 169
  27. lemma OAI.EuclideanFiveColor.moserRotation_unit line 170
  28. lemma OAI.EuclideanFiveColor.placedMoser_edge_unit line 173
  29. def OAI.EuclideanFiveColor.certificateX line 182
  30. def OAI.EuclideanFiveColor.certificateY line 183
  31. lemma OAI.EuclideanFiveColor.radical_bounds line 184
  32. lemma OAI.EuclideanFiveColor.radical_product_bounds line 195
  33. lemma OAI.EuclideanFiveColor.seven_point_box_0 line 199
  34. lemma OAI.EuclideanFiveColor.seven_point_box_1 line 208
  35. lemma OAI.EuclideanFiveColor.seven_point_box_2 line 218
  36. lemma OAI.EuclideanFiveColor.seven_point_box_3 line 228
  37. lemma OAI.EuclideanFiveColor.seven_point_box_4 line 238
  38. lemma OAI.EuclideanFiveColor.seven_point_box_5 line 248
  39. lemma OAI.EuclideanFiveColor.seven_point_box_6 line 258
  40. lemma OAI.EuclideanFiveColor.seven_point_boxes line 268
  41. lemma OAI.EuclideanFiveColor.seven_point_certificate line 285

    Source documentation

    Exact rational interval certificate for the manuscript's seven placed vertices.

    lemma seven_point_certificate (i : Fin 7) :
    ThreeLabelRegion (placedMoser i).re (placedMoser i).im := by
…

    Mentions: OAI.EuclideanFiveColor.ThreeLabelRegion, OAI.EuclideanFiveColor.placedMoser