OAI/Analysis/PlaneSpectrum/SpectralMeasure.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.EuclideanFiveColor.VectorMeasure.inner_toLp line 13
  2. def OAI.EuclideanFiveColor.VectorMeasure.vectorLinear line 29
  3. lemma OAI.EuclideanFiveColor.VectorMeasure.norm_toLp line 33
  4. def OAI.EuclideanFiveColor.VectorMeasure.cyclicMap line 40
  5. lemma OAI.EuclideanFiveColor.VectorMeasure.cyclicMap_toLp line 42
  6. lemma OAI.EuclideanFiveColor.VectorMeasure.norm_cyclicMap line 47
  7. def OAI.EuclideanFiveColor.VectorMeasure.cyclicIsometry line 53
  8. def OAI.EuclideanFiveColor.BoundedMeasurable.mulLp line 63
  9. lemma OAI.EuclideanFiveColor.BoundedMeasurable.mulLp_ae line 65
  10. def OAI.EuclideanFiveColor.BoundedMeasurable.mulLpLinear line 67
  11. lemma OAI.EuclideanFiveColor.BoundedMeasurable.mulLp_norm_le line 81
  12. def OAI.EuclideanFiveColor.BoundedMeasurable.mulLpCLM line 87
  13. lemma OAI.EuclideanFiveColor.BoundedMeasurable.mulLpCLM_ae line 89
  14. lemma OAI.EuclideanFiveColor.BoundedMeasurable.mulLp_l2 line 91
  15. abbrev OAI.EuclideanFiveColor.CommutingSpectral.algebra line 104
  16. instance OAI.EuclideanFiveColor.CommutingSpectral.algebra_closed line 106
  17. lemma OAI.EuclideanFiveColor.CommutingSpectral.adjoin_comm line 108
  18. instance OAI.EuclideanFiveColor.CommutingSpectral.algebra_commRing line 119
  19. instance OAI.EuclideanFiveColor.CommutingSpectral.algebra_commCStar line 122
  20. def OAI.EuclideanFiveColor.CommutingSpectral.generator line 124
  21. lemma OAI.EuclideanFiveColor.CommutingSpectral.generator_one line 126
  22. lemma OAI.EuclideanFiveColor.CommutingSpectral.generator_mul line 127
  23. lemma OAI.EuclideanFiveColor.CommutingSpectral.generator_unitary line 130
  24. abbrev OAI.EuclideanFiveColor.CommutingSpectral.Spectrum line 135
  25. def OAI.EuclideanFiveColor.CommutingSpectral.character line 136
  26. lemma OAI.EuclideanFiveColor.CommutingSpectral.character_apply line 150
  27. lemma OAI.EuclideanFiveColor.CommutingSpectral.character_continuous line 152
  28. def OAI.EuclideanFiveColor.CommutingSpectral.calculus line 156
  29. def OAI.EuclideanFiveColor.CommutingSpectral.evaluation line 159
  30. lemma OAI.EuclideanFiveColor.CommutingSpectral.calculus_evaluation line 161
  31. def OAI.EuclideanFiveColor.VectorMeasure.boundedCM line 178
  32. lemma OAI.EuclideanFiveColor.VectorMeasure.boundedCM_apply line 181
  33. lemma OAI.EuclideanFiveColor.VectorMeasure.boundedCM_toLp line 183
  34. lemma OAI.EuclideanFiveColor.VectorMeasure.mulCM_toLp line 187
  35. lemma OAI.EuclideanFiveColor.VectorMeasure.cyclicMap_mul line 192
  36. lemma OAI.EuclideanFiveColor.VectorMeasure.cyclicMap_one line 199
  37. lemma OAI.EuclideanFiveColor.VectorMeasure.cyclicMap_inner line 203
  38. lemma OAI.EuclideanFiveColor.VectorMeasure.cyclicMap_pair_one line 206
  39. def OAI.PlaneFiveColor.Spectral.ordinaryIndicator line 224
  40. lemma OAI.PlaneFiveColor.Spectral.ordinaryIndicator_apply line 227
  41. lemma OAI.PlaneFiveColor.Spectral.ordinary_eval_continuous line 228
  42. lemma OAI.PlaneFiveColor.Spectral.ordinary_difference_tendsto line 233
  43. def OAI.PlaneFiveColor.Spectral.ordinaryVector line 268
  44. lemma OAI.PlaneFiveColor.Spectral.ordinaryVector_continuous line 269
  45. lemma OAI.PlaneFiveColor.Spectral.measure_ordinary_zero_of_orthogonal line 287
  46. lemma OAI.EuclideanFiveColor.CommutingSpectral.evaluation_one line 306
  47. lemma OAI.EuclideanFiveColor.CommutingSpectral.evaluation_mul line 310
  48. lemma OAI.EuclideanFiveColor.CommutingSpectral.star_evaluation line 314
  49. def OAI.EuclideanFiveColor.CommutingSpectral.evaluationHom line 319
  50. lemma OAI.EuclideanFiveColor.CommutingSpectral.evaluation_span_dense line 323
  51. lemma OAI.EuclideanFiveColor.CompactIntegral.integrableCM line 358
  52. def OAI.EuclideanFiveColor.CompactIntegral.linear line 360
  53. lemma OAI.EuclideanFiveColor.CompactIntegral.norm_le line 364
  54. def OAI.EuclideanFiveColor.CompactIntegral.clm line 367
  55. lemma OAI.EuclideanFiveColor.CompactIntegral.apply_clm line 368
  56. lemma OAI.EuclideanFiveColor.CommutingSpectral.measure_eq_of_fourier line 373