OAI/Analysis/PlaneSpectrum/CircleDecay.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.EuclideanFiveColor.oscillatory_integral_bound line 9
  2. def OAI.EuclideanFiveColor.circleOscillation line 56
  3. lemma OAI.EuclideanFiveColor.circleOscillation_norm line 57
  4. lemma OAI.EuclideanFiveColor.circleOscillation_continuous line 58
  5. lemma OAI.EuclideanFiveColor.circleOscillation_hasDeriv line 59
  6. lemma OAI.EuclideanFiveColor.circleOscillation_tail line 65
  7. lemma OAI.EuclideanFiveColor.circleOscillation_quarter line 101
  8. lemma OAI.EuclideanFiveColor.circleOscillation_pi_sub line 131
  9. lemma OAI.EuclideanFiveColor.circleOscillation_two_pi_sub line 138
  10. lemma OAI.EuclideanFiveColor.circleOscillation_full line 141
  11. def OAI.EuclideanFiveColor.circleSymbol line 177
  12. lemma OAI.EuclideanFiveColor.circleSymbol_norm_le_one line 178
  13. lemma OAI.EuclideanFiveColor.circlePhase_real line 183
  14. lemma OAI.EuclideanFiveColor.circleSymbol_integral line 199
  15. lemma OAI.EuclideanFiveColor.circleSymbol_sq_bound line 210