OAI/Analysis/PlaneSpectrum/Representations.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlaneFiveColor.Spectral.Rot line 11

    Source documentation

    Discrete additive notation for the actual multiplicative algebraic rotation group.

    def Rot := Additive K deriving AddCommGroup

    Mentions: OAI.PlaneFiveColor.Spectral.K

  2. instance OAI.PlaneFiveColor.Spectral.(instance at line 12) line 12
  3. instance OAI.PlaneFiveColor.Spectral.(instance at line 13) line 13
  4. def OAI.PlaneFiveColor.Spectral.rotMul line 14
  5. def OAI.PlaneFiveColor.Spectral.mulRot line 15
  6. lemma OAI.PlaneFiveColor.Spectral.rotMul_mulRot line 16
  7. lemma OAI.PlaneFiveColor.Spectral.mulRot_rotMul line 17
  8. instance OAI.PlaneFiveColor.Spectral.rotAction line 18
  9. lemma OAI.PlaneFiveColor.Spectral.rot_vadd line 22
  10. instance OAI.PlaneFiveColor.Spectral.rotMeasurable line 24
  11. instance OAI.PlaneFiveColor.Spectral.rotInvariant line 27
  12. instance OAI.PlaneFiveColor.Spectral.rotErgodic line 30
  13. lemma OAI.PlaneFiveColor.Spectral.rot_zsmul_surjective line 34
  14. def OAI.PlaneFiveColor.LabelModel.Proper line 55
  15. abbrev OAI.PlaneFiveColor.LabelModel.Space line 56
  16. lemma OAI.PlaneFiveColor.LabelModel.closed_proper line 57
  17. instance OAI.PlaneFiveColor.LabelModel.(instance at line 63) line 63
  18. def OAI.PlaneFiveColor.LabelModel.trans line 64
  19. def OAI.PlaneFiveColor.LabelModel.rotate line 69
  20. lemma OAI.PlaneFiveColor.LabelModel.trans_apply line 74
  21. lemma OAI.PlaneFiveColor.LabelModel.rotate_apply line 75
  22. lemma OAI.PlaneFiveColor.LabelModel.trans_continuous line 76
  23. lemma OAI.PlaneFiveColor.LabelModel.rotate_continuous line 79
  24. lemma OAI.PlaneFiveColor.LabelModel.trans_zero line 82
  25. lemma OAI.PlaneFiveColor.LabelModel.trans_add line 83
  26. lemma OAI.PlaneFiveColor.LabelModel.rotate_one line 84
  27. lemma OAI.PlaneFiveColor.LabelModel.rotate_mul line 89
  28. lemma OAI.PlaneFiveColor.LabelModel.covariance line 95
  29. def OAI.PlaneFiveColor.LabelModel.transHomeo line 99
  30. def OAI.PlaneFiveColor.LabelModel.rotateHomeo line 106
  31. abbrev OAI.PlaneFiveColor.LabelModel.Trans line 113
  32. def OAI.PlaneFiveColor.LabelModel.tr line 114
  33. def OAI.PlaneFiveColor.LabelModel.ro line 115
  34. def OAI.PlaneFiveColor.LabelModel.measure line 116
  35. instance OAI.PlaneFiveColor.LabelModel.(instance at line 117) line 117
  36. lemma OAI.PlaneFiveColor.LabelModel.trans_preserving line 118
  37. lemma OAI.PlaneFiveColor.LabelModel.rotate_preserving line 124
  38. def OAI.EuclideanFiveColor.Koopman.isometry line 137
  39. def OAI.EuclideanFiveColor.Koopman.unitary line 150
  40. lemma OAI.EuclideanFiveColor.Koopman.unitary_apply line 152
  41. lemma OAI.EuclideanFiveColor.Koopman.nonlinear_commute line 154
  42. def OAI.EuclideanFiveColor.ContinuousVectors.op line 171
  43. lemma OAI.EuclideanFiveColor.ContinuousVectors.op_zero line 172
  44. lemma OAI.EuclideanFiveColor.ContinuousVectors.op_add line 173
  45. lemma OAI.EuclideanFiveColor.ContinuousVectors.op_comm line 176
  46. lemma OAI.EuclideanFiveColor.ContinuousVectors.norm_op line 178
  47. lemma OAI.EuclideanFiveColor.ContinuousVectors.dist_op line 179
  48. def OAI.EuclideanFiveColor.ContinuousVectors.space line 182
  49. lemma OAI.EuclideanFiveColor.ContinuousVectors.mem_space line 193
  50. lemma OAI.EuclideanFiveColor.ContinuousVectors.isClosed_space line 194
  51. instance OAI.EuclideanFiveColor.ContinuousVectors.(instance at line 209) line 209
  52. lemma OAI.EuclideanFiveColor.ContinuousVectors.op_mem line 210
  53. lemma OAI.EuclideanFiveColor.ContinuousVectors.orbit_continuous line 215
  54. abbrev OAI.PlaneFiveColor.LabelModel.Hilbert line 238
  55. def OAI.PlaneFiveColor.LabelModel.translation line 239
  56. def OAI.PlaneFiveColor.LabelModel.rotation line 241
  57. lemma OAI.PlaneFiveColor.LabelModel.translation_apply line 243
  58. lemma OAI.PlaneFiveColor.LabelModel.rotation_apply line 246
  59. def OAI.PlaneFiveColor.LabelModel.representation line 249
  60. lemma OAI.PlaneFiveColor.LabelModel.op_apply line 268
  61. lemma OAI.PlaneFiveColor.LabelModel.rotation_covariance line 270
  62. lemma OAI.EuclideanFiveColor.projection_fixed_of_contraction line 284
  63. lemma OAI.EuclideanFiveColor.ContinuousVectors.nonlinear_mem line 308
  64. def OAI.EuclideanFiveColor.ContinuousVectors.clamp line 316
  65. lemma OAI.EuclideanFiveColor.ContinuousVectors.clamp_lipschitz line 317
  66. lemma OAI.EuclideanFiveColor.ContinuousVectors.clamp_zero line 324
  67. lemma OAI.EuclideanFiveColor.ContinuousVectors.clamp_range line 325
  68. lemma OAI.EuclideanFiveColor.ContinuousVectors.clamp_eq line 328
  69. lemma OAI.EuclideanFiveColor.ContinuousVectors.projection_range line 332
  70. lemma OAI.EuclideanFiveColor.ContinuousVectors.covariance_mem line 357
  71. lemma OAI.EuclideanFiveColor.ContinuousVectors.projection_covariance_fixed line 366
  72. lemma OAI.EuclideanFiveColor.ContinuousVectors.op_orthogonal line 372
  73. lemma OAI.EuclideanFiveColor.ContinuousVectors.projection_coefficient line 380
  74. def OAI.EuclideanFiveColor.VectorMeasure.realCM line 404
  75. lemma OAI.EuclideanFiveColor.VectorMeasure.realCM_apply line 405
  76. lemma OAI.EuclideanFiveColor.VectorMeasure.realCM_add line 406
  77. lemma OAI.EuclideanFiveColor.VectorMeasure.realCM_sub line 407
  78. lemma OAI.EuclideanFiveColor.VectorMeasure.realCM_smul line 408
  79. lemma OAI.EuclideanFiveColor.VectorMeasure.realCM_one line 409
  80. lemma OAI.EuclideanFiveColor.VectorMeasure.real_nonneg line 412
  81. def OAI.EuclideanFiveColor.VectorMeasure.functional line 424
  82. def OAI.EuclideanFiveColor.VectorMeasure.measure line 437
  83. instance OAI.EuclideanFiveColor.VectorMeasure.(instance at line 438) line 438
  84. instance OAI.EuclideanFiveColor.VectorMeasure.(instance at line 439) line 439
  85. lemma OAI.EuclideanFiveColor.VectorMeasure.integral_real line 440
  86. lemma OAI.EuclideanFiveColor.VectorMeasure.integral_complex line 442
  87. lemma OAI.EuclideanFiveColor.VectorMeasure.measure_univ line 470