OAI/Geometry/PlaneColoring/BorelTransfer.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlaneFiveColor.LabelModel.colorValue line 12
  2. lemma OAI.PlaneFiveColor.LabelModel.color_memLp line 13
  3. abbrev OAI.PlaneFiveColor.LabelModel.colorVector line 20
  4. lemma OAI.PlaneFiveColor.LabelModel.color_ae line 21
  5. lemma OAI.PlaneFiveColor.LabelModel.color_rotation_fixed line 22
  6. lemma OAI.PlaneFiveColor.LabelModel.color_unit_correlation line 29
  7. instance OAI.PlaneFiveColor.LabelModel.continuous_complete line 44
  8. def OAI.PlaneFiveColor.LabelModel.projected line 46
  9. lemma OAI.PlaneFiveColor.LabelModel.projected_range line 47
  10. lemma OAI.PlaneFiveColor.LabelModel.projected_rotation_fixed line 54
  11. lemma OAI.PlaneFiveColor.LabelModel.projected_unit_correlation line 59
  12. def OAI.PlaneFiveColor.LabelModel.oneVector line 74
  13. lemma OAI.PlaneFiveColor.LabelModel.one_ae line 75
  14. lemma OAI.PlaneFiveColor.LabelModel.one_fixed line 76
  15. lemma OAI.PlaneFiveColor.LabelModel.one_continuous line 82
  16. lemma OAI.PlaneFiveColor.LabelModel.color_sum line 85
  17. lemma OAI.PlaneFiveColor.LabelModel.projected_sum line 91
  18. lemma OAI.PlaneFiveColor.Spectral.dense_E line 102
  19. lemma OAI.PlaneFiveColor.Spectral.algebraic_norm line 117
  20. lemma OAI.PlaneFiveColor.Spectral.orbit_uniformContinuous line 132
  21. def OAI.PlaneFiveColor.Spectral.orbitExtension line 147
  22. lemma OAI.PlaneFiveColor.Spectral.orbitExtension_continuous line 148
  23. lemma OAI.PlaneFiveColor.Spectral.orbitExtension_eq line 150
  24. lemma OAI.PlaneFiveColor.Spectral.orbitExtension_inner line 152
  25. lemma OAI.PlaneFiveColor.Spectral.normalized_algebraic line 170
  26. lemma OAI.PlaneFiveColor.Spectral.circle_closed_induction line 180
  27. lemma OAI.PlaneFiveColor.LabelModel.projected_continuous line 205
  28. def OAI.PlaneFiveColor.LabelModel.fieldVector line 207
  29. lemma OAI.PlaneFiveColor.LabelModel.fieldVector_continuous line 208
  30. lemma OAI.PlaneFiveColor.LabelModel.fieldVector_algebraic line 210
  31. lemma OAI.PlaneFiveColor.LabelModel.fieldVector_sum line 212
  32. lemma OAI.PlaneFiveColor.LabelModel.fieldVector_range line 216
  33. lemma OAI.PlaneFiveColor.LabelModel.fieldVector_unit_correlation line 234
  34. lemma OAI.EuclideanFiveColor.dense_approx line 256
  35. def OAI.EuclideanFiveColor.approxIndex line 262
  36. lemma OAI.EuclideanFiveColor.index_measurable line 263
  37. lemma OAI.EuclideanFiveColor.index_bound line 268
  38. def OAI.EuclideanFiveColor.approxField line 272
  39. lemma OAI.EuclideanFiveColor.approxField_measurable line 274
  40. lemma OAI.EuclideanFiveColor.approxField_tendsto line 279
  41. def OAI.EuclideanFiveColor.measurableField line 291
  42. lemma OAI.EuclideanFiveColor.measurableField_measurable line 294
  43. lemma OAI.EuclideanFiveColor.exists_measurable_field line 301
  44. lemma OAI.EuclideanFiveColor.positive_orthogonal line 317
  45. lemma OAI.PlaneFiveColor.LabelModel.exists_label_field line 341
  46. def OAI.EuclideanFiveColor.positiveSupport line 373
  47. lemma OAI.EuclideanFiveColor.positiveSupport_measurable line 375
  48. def OAI.EuclideanFiveColor.pickSupport line 380
  49. def OAI.EuclideanFiveColor.positiveSelect line 381
  50. lemma OAI.EuclideanFiveColor.positiveSelect_measurable line 382
  51. lemma OAI.EuclideanFiveColor.positiveSelect_pos line 385
  52. lemma OAI.EuclideanFiveColor.sample_field line 407
  53. lemma OAI.EuclideanFiveColor.proper_to_borel_weak line 436
  54. lemma OAI.EuclideanFiveColor.proper_to_weak line 444