OAI/MeasureTheory/FalconerCompletion/Fourier/StationaryInverseUnit3.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Fourier kernels and oscillatory estimates.

  1. def OAI.GraphLiteralSupport.Attempt4PrefixShell.stationaryInverseUnitND line 18
  2. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.stationaryInverseUnitND_val line 21
  3. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.stationaryInverseUnitND_inv line 24
  4. def OAI.GraphLiteralSupport.Attempt4PrefixShell.stationaryInversePolynomialND line 27
  5. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.stationaryInversePolynomialND_zero line 31
  6. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.stationaryInversePolynomialND_convolution line 36
  7. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.stationaryInversePolynomialND_succ line 46
  8. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.stationaryInversePolynomialND_degree line 58
  9. def OAI.GraphLiteralSupport.Attempt4PrefixShell.stationaryFactorPolynomialND line 77
  10. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.stationaryFactorPolynomialND_degree line 81
  11. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.stationaryFactorPolynomialND_product line 91
  12. def OAI.GraphLiteralSupport.Attempt4PrefixShell.smoothFunctionSpaceND line 99
  13. abbrev OAI.GraphLiteralSupport.Attempt4PrefixShell.SmoothFunctionND line 113
  14. def OAI.GraphLiteralSupport.Attempt4PrefixShell.casimirOperatorND line 116
  15. def OAI.GraphLiteralSupport.Attempt4PrefixShell.differentialPolynomialND line 121
  16. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.differentialPolynomialND_add line 124
  17. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.differentialPolynomialND_mul line 128
  18. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.differentialPolynomialND_C line 132
  19. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.differentialPolynomialND_X line 136
  20. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.differentialPolynomialND_factor line 139
  21. def OAI.GraphLiteralSupport.Attempt4PrefixShell.stationaryLPolynomialND line 153
  22. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.stationaryLPolynomialND_zero line 156
  23. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.stationaryLPolynomialND_degree line 159
  24. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.differentialPolynomialND_L line 164
  25. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.differentialPolynomialND_inverse_convolution line 173