OAI/Analysis/RotationWeights/FunctionalCalculus.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ContinuousCircleWeight.lp_diagonal_stronglyMeasurable line 22
  2. def OAI.ContinuousCircleWeight.boundedPiField line 47
  3. lemma OAI.ContinuousCircleWeight.boundedPiField_apply line 49
  4. lemma OAI.ContinuousCircleWeight.boundedPiField_bound line 51
  5. lemma OAI.ContinuousCircleWeight.boundedPiField_measurable line 53
  6. def OAI.ContinuousCircleWeight.boundedPi line 58
  7. lemma OAI.ContinuousCircleWeight.boundedPi_coe line 63
  8. lemma OAI.ContinuousCircleWeight.boundedPi_norm_le line 67
  9. lemma OAI.ContinuousCircleWeight.norm_tendsto_zero_of_sq line 71
  10. lemma OAI.ContinuousCircleWeight.lpDiagonal_tendsto line 75
  11. lemma OAI.ContinuousCircleWeight.L2_tendsto_of_dominated line 103
  12. lemma OAI.ContinuousCircleWeight.boundedPi_tendsto line 125
  13. def OAI.ContinuousCircleWeight.complexCircleMap line 162
  14. lemma OAI.ContinuousCircleWeight.circleFunction_circle line 165
  15. lemma OAI.ContinuousCircleWeight.circleFunction_fourier_one line 170
  16. lemma OAI.ContinuousCircleWeight.circleFunction_continuousOn line 177
  17. lemma OAI.ContinuousCircleWeight.circleFunction_continuousOn_spectrum line 184
  18. lemma OAI.ContinuousCircleWeight.circle_cfc line 192
  19. lemma OAI.ContinuousCircleWeight.circle_cfc_hom line 206
  20. lemma OAI.ContinuousCircleWeight.bounded_real_continuous_approx line 220
  21. lemma OAI.ContinuousCircleWeight.boundedPi_eq_continuousPi line 247
  22. lemma OAI.ContinuousCircleWeight.boundedPi_congr line 257
  23. lemma OAI.ContinuousCircleWeight.commute_boundedPi_real line 273