OAI/Analysis/FourierExtension/Surface.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Positively curved surfaces and their extension operators.

  1. abbrev OAI.DiagonalExtension.E3 line 16
  2. def OAI.DiagonalExtension.IsSurface line 18
  3. def OAI.DiagonalExtension.surfaceMeasure line 28
  4. def OAI.DiagonalExtension.fourierCharacter line 31
  5. def OAI.DiagonalExtension.extension line 34
  6. def OAI.DiagonalExtension.MainStatement line 37
  7. theorem OAI.DiagonalExtension.regular_level_finiteAt line 48
  8. theorem OAI.DiagonalExtension.IsSurface.hausdorffMeasure_lt_top line 88
  9. theorem OAI.DiagonalExtension.IsSurface.isFiniteMeasure line 104
  10. theorem OAI.DiagonalExtension.IsSurface.integrable_of_memLp line 110
  11. theorem OAI.DiagonalExtension.norm_fourierCharacter line 119
  12. theorem OAI.DiagonalExtension.continuous_fourierCharacter line 122
  13. theorem OAI.DiagonalExtension.extension_integrand_integrable line 126
  14. theorem OAI.DiagonalExtension.norm_extension_le line 133
  15. theorem OAI.DiagonalExtension.continuous_extension line 139