OAI/MeasureTheory/FalconerCompletion/Fourier/SphereConeToLp.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Fourier kernels and oscillatory estimates.

  1. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereConeND_toLp line 19
  2. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereConeND_norm line 22
  3. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereConeND_injOn line 26
  4. def OAI.GraphLiteralSupport.Attempt4FullFar.coneBasisND line 42
  5. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereConeDerivND_toMatrix line 46
  6. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereConeDerivND_det line 71
  7. lemma OAI.GraphLiteralSupport.Attempt4FullFar.lintegral_unitInterval_powND line 82
  8. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartWeightND line 95
  9. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartWeightND_measurable line 98
  10. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartWeightND_pos line 103
  11. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereConeND_volume line 108
  12. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereConeND_measurableSet_image line 142
  13. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereConeND_preimage_image line 151
  14. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartND_surface_measure line 163
  15. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartND_continuous line 196
  16. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereAreaND line 202
  17. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereAreaND_chart line 205
  18. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereAreaND_restrict_chart line 212
  19. lemma OAI.GraphLiteralSupport.Attempt4FullFar.integral_sphereAreaND_chart line 231
  20. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartWeightND_eq_source line 245
  21. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartND_exponential line 255
  22. lemma OAI.GraphLiteralSupport.Attempt4FullFar.integral_sphereAreaND_quadratic line 263
  23. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartAmplitudeND line 279
  24. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartWeightND_zero line 284
  25. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartWeightND_contDiffOn line 289
  26. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartAmplitudeND_zero line 296
  27. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartAmplitudeND_tsupport line 309
  28. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartAmplitudeND_hasCompactSupport line 319
  29. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartAmplitudeND_contDiff line 327
  30. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartSchwartzND line 345