OAI/Analysis/FourierExtension/SmoothCharts.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Smooth regular levels and positively curved charts.

  1. theorem OAI.DiagonalExtension.SmoothLevel.exists_height line 18
  2. lemma OAI.DiagonalExtension.SmoothLevel.second_level_equation line 73
  3. lemma OAI.DiagonalExtension.SmoothLevel.height_hessian line 99
  4. lemma OAI.DiagonalExtension.SmoothLevel.eventually_contDiffAt_implicit line 148
  5. lemma OAI.DiagonalExtension.SmoothLevel.positive_quadratic_lower line 189
  6. lemma OAI.DiagonalExtension.SmoothLevel.eventually_quadratic_lower line 211
  7. theorem OAI.DiagonalExtension.SmoothLevel.exists_convex_height line 240
  8. def OAI.DiagonalExtension.SmoothLevel.kernelNormalEquiv line 320
  9. lemma OAI.DiagonalExtension.SmoothLevel.kernelNormalEquiv_apply line 335
  10. lemma OAI.DiagonalExtension.SmoothLevel.kernelNormalEquiv_symm_snd line 338
  11. lemma OAI.DiagonalExtension.SmoothLevel.kernelNormalEquiv_symm_fst line 341
  12. theorem OAI.DiagonalExtension.IsSurface.exists_convex_chart line 349