OAI/MeasureTheory/FalconerCompletion/Fourier/StationaryInverseUnit.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Fourier kernels and oscillatory estimates.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.stationaryInverseUnitND line 17
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.stationaryInverseUnitND_val line 20
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.stationaryInverseUnitND_inv line 23
  4. def OAI.GraphLiteralSupport.CurrentFalconer.stationaryInversePolynomialND line 26
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.stationaryInversePolynomialND_zero line 30
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.stationaryInversePolynomialND_convolution line 35
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.stationaryInversePolynomialND_succ line 45
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.stationaryInversePolynomialND_degree line 57
  9. def OAI.GraphLiteralSupport.CurrentFalconer.stationaryFactorPolynomialND line 76
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.stationaryFactorPolynomialND_degree line 80
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.stationaryFactorPolynomialND_product line 90
  12. def OAI.GraphLiteralSupport.CurrentFalconer.smoothFunctionSpaceND line 98
  13. abbrev OAI.GraphLiteralSupport.CurrentFalconer.SmoothFunctionND line 112
  14. def OAI.GraphLiteralSupport.CurrentFalconer.casimirOperatorND line 115
  15. def OAI.GraphLiteralSupport.CurrentFalconer.differentialPolynomialND line 120
  16. lemma OAI.GraphLiteralSupport.CurrentFalconer.differentialPolynomialND_add line 123
  17. lemma OAI.GraphLiteralSupport.CurrentFalconer.differentialPolynomialND_mul line 127
  18. lemma OAI.GraphLiteralSupport.CurrentFalconer.differentialPolynomialND_C line 131
  19. lemma OAI.GraphLiteralSupport.CurrentFalconer.differentialPolynomialND_X line 135
  20. lemma OAI.GraphLiteralSupport.CurrentFalconer.differentialPolynomialND_factor line 138
  21. def OAI.GraphLiteralSupport.CurrentFalconer.stationaryLPolynomialND line 152
  22. lemma OAI.GraphLiteralSupport.CurrentFalconer.stationaryLPolynomialND_zero line 155
  23. lemma OAI.GraphLiteralSupport.CurrentFalconer.stationaryLPolynomialND_degree line 158
  24. lemma OAI.GraphLiteralSupport.CurrentFalconer.differentialPolynomialND_L line 163
  25. lemma OAI.GraphLiteralSupport.CurrentFalconer.differentialPolynomialND_inverse_convolution line 172