OAI/Analysis/FourierExtension/ConvexExtension.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Smooth cutoffs and convex continuation.

  1. lemma OAI.DiagonalExtension.CutoffHessian.iteratedFDeriv_section line 24
  2. lemma OAI.DiagonalExtension.CutoffHessian.continuous_section_derivative line 43
  3. lemma OAI.DiagonalExtension.CutoffHessian.uniform_derivative_small line 50
  4. def OAI.DiagonalExtension.CutoffHessian.profile line 68
  5. lemma OAI.DiagonalExtension.CutoffHessian.smooth_profile line 73
  6. lemma OAI.DiagonalExtension.CutoffHessian.profile_zero line 78
  7. theorem OAI.DiagonalExtension.CutoffHessian.profile_hessian_small line 82
  8. lemma OAI.DiagonalExtension.CutoffHessian.scaled_hessian_apply line 96
  9. lemma OAI.DiagonalExtension.CutoffHessian.hessian_add line 116
  10. def OAI.DiagonalExtension.CutoffHessian.patch line 128
  11. lemma OAI.DiagonalExtension.CutoffHessian.patch_scaled line 131
  12. lemma OAI.DiagonalExtension.CutoffHessian.patch_hessian_small line 142
  13. theorem OAI.DiagonalExtension.CutoffHessian.exists_small_patch line 159
  14. lemma OAI.DiagonalExtension.CutoffHessian.hessian_sub_map line 204
  15. theorem OAI.DiagonalExtension.CutoffHessian.glue_convex line 218
  16. theorem OAI.DiagonalExtension.SmoothExtension.extend_local line 261
  17. def OAI.DiagonalExtension.QuadraticTaylor.polynomial line 292
  18. lemma OAI.DiagonalExtension.QuadraticTaylor.smooth line 295
  19. lemma OAI.DiagonalExtension.QuadraticTaylor.derivative line 300
  20. lemma OAI.DiagonalExtension.QuadraticTaylor.fderiv_polynomial line 310
  21. lemma OAI.DiagonalExtension.QuadraticTaylor.hessian_polynomial line 316
  22. def OAI.DiagonalExtension.ConvexNeighborhood.taylor2 line 331
  23. theorem OAI.DiagonalExtension.ConvexNeighborhood.local_convex_extension line 334