OAI/Analysis/PlaneSpectrum/CircleOperator.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.EuclideanFiveColor.planeTranslate_continuous line 9
  2. lemma OAI.EuclideanFiveColor.circleTranslate_integrable line 12
  3. def OAI.EuclideanFiveColor.circleOperator line 15
  4. lemma OAI.EuclideanFiveColor.circleOperator_norm_le line 16
  5. lemma OAI.EuclideanFiveColor.circleOperator_ae line 20
  6. lemma OAI.EuclideanFiveColor.circleSymbol_stronglyMeasurable line 46
  7. def OAI.EuclideanFiveColor.circleMultiplier line 52
  8. lemma OAI.EuclideanFiveColor.circleMultiplier_ae line 55
  9. lemma OAI.EuclideanFiveColor.fourier_circleOperator line 57
  10. lemma OAI.EuclideanFiveColor.planePhase_sub_bound line 94
  11. lemma OAI.EuclideanFiveColor.planePhase_sub_bound_two line 105
  12. def OAI.EuclideanFiveColor.circleDifferenceRatio line 109
  13. lemma OAI.EuclideanFiveColor.circleDifferenceRatio_nonneg line 111
  14. lemma OAI.EuclideanFiveColor.circleDifferenceRatio_small line 114
  15. lemma OAI.EuclideanFiveColor.circleDifferenceRatio_bound line 129
  16. lemma OAI.EuclideanFiveColor.circleDifferenceRatio_tendsto line 156
  17. lemma OAI.EuclideanFiveColor.circleDifferenceRatio_measurable line 161
  18. lemma OAI.EuclideanFiveColor.planeL2_norm_sq line 176
  19. lemma OAI.EuclideanFiveColor.circleDifference_norm_sq line 179
  20. lemma OAI.EuclideanFiveColor.circle_smoothing_L2 line 198
  21. lemma OAI.EuclideanFiveColor.ae_circle_pullback line 222
  22. def OAI.EuclideanFiveColor.circleAverage line 230
  23. lemma OAI.EuclideanFiveColor.circleOperator_toLp_ae line 231
  24. lemma OAI.EuclideanFiveColor.circleOperator_difference_ae line 235
  25. def OAI.EuclideanFiveColor.colorMass line 249
  26. lemma OAI.EuclideanFiveColor.colorMass_measurable line 251
  27. lemma OAI.EuclideanFiveColor.colorMass_nonneg line 259
  28. lemma OAI.EuclideanFiveColor.colorMass_le_one line 261
  29. def OAI.EuclideanFiveColor.colorCutoff line 265
  30. lemma OAI.EuclideanFiveColor.colorCutoff_memLp line 267
  31. lemma OAI.EuclideanFiveColor.colorCutoff_sample line 277
  32. lemma OAI.EuclideanFiveColor.colorCutoff_circleDifference line 288