OAI/Analysis/PlaneSpectrum/Fourier.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanFiveColor.Multiplier.apply line 10
  2. lemma OAI.EuclideanFiveColor.Multiplier.apply_ae line 13
  3. def OAI.EuclideanFiveColor.Multiplier.linear line 15
  4. lemma OAI.EuclideanFiveColor.Multiplier.apply_norm_le line 29
  5. def OAI.EuclideanFiveColor.Multiplier.clm line 35
  6. lemma OAI.EuclideanFiveColor.Multiplier.clm_ae line 38
  7. abbrev OAI.EuclideanFiveColor.ComplexPlaneL2 line 41
  8. def OAI.EuclideanFiveColor.planeTranslate line 42
  9. lemma OAI.EuclideanFiveColor.planeTranslate_ae line 44
  10. def OAI.EuclideanFiveColor.planePhase line 47
  11. lemma OAI.EuclideanFiveColor.planePhase_norm line 48
  12. lemma OAI.EuclideanFiveColor.planePhase_continuous line 49
  13. def OAI.EuclideanFiveColor.phaseMultiplier line 53
  14. lemma OAI.EuclideanFiveColor.phaseMultiplier_ae line 56
  15. def OAI.EuclideanFiveColor.schwartzTranslate line 58
  16. lemma OAI.EuclideanFiveColor.schwartzTranslate_apply line 61
  17. lemma OAI.EuclideanFiveColor.schwartzTranslate_toLp line 63
  18. lemma OAI.EuclideanFiveColor.fourier_schwartzTranslate line 69
  19. lemma OAI.EuclideanFiveColor.fourier_planeTranslate line 75
  20. lemma OAI.EuclideanFiveColor.ProbabilityL2.norm_integral_sq line 96
  21. def OAI.EuclideanFiveColor.ProbabilityL2.average line 116
  22. lemma OAI.EuclideanFiveColor.ProbabilityL2.average_measurable line 117
  23. lemma OAI.EuclideanFiveColor.ProbabilityL2.fiber_memLp line 119
  24. lemma OAI.EuclideanFiveColor.ProbabilityL2.average_memLp line 125
  25. lemma OAI.EuclideanFiveColor.ProbabilityL2.average_toLp_integral line 132