OAI/MeasureTheory/FalconerCompletion/Fourier/StationaryInverseUnit2.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Fourier kernels and oscillatory estimates.

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