OAI/Geometry/SmoothYau/Smoothness/HessianJet.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.deriv_radial_line line 40
  2. lemma OAI.YauCounterexamples.second_deriv_radial_line line 45
  3. lemma OAI.YauCounterexamples.second_order_line_taylor line 56
  4. lemma OAI.YauCounterexamples.gaussian_of_hessian line 73
  5. lemma OAI.YauCounterexamples.compact_uniform_value_radius line 95
  6. lemma OAI.YauCounterexamples.compact_uniform_hessian_radius line 115
  7. theorem OAI.YauCounterexamples.compact_gaussian_localization line 123
  8. def OAI.YauCounterexamples.hessianFromJet line 183
  9. lemma OAI.YauCounterexamples.hessianFromJet_iterated line 187
  10. lemma OAI.YauCounterexamples.continuous_hessian_of_iterated line 193
  11. lemma OAI.YauCounterexamples.second_fderiv_eval_const line 199
  12. lemma OAI.YauCounterexamples.second_fderiv_realPolyEval line 209
  13. lemma OAI.YauCounterexamples.polynomial_prescribed_two_jet line 224
  14. lemma OAI.YauCounterexamples.continuous_iterated_re_precomp line 248
  15. lemma OAI.YauCounterexamples.first_fderiv_re_precomp line 266
  16. lemma OAI.YauCounterexamples.second_fderiv_re_precomp line 273
  17. lemma OAI.YauCounterexamples.second_fderiv_sub line 291
  18. theorem OAI.YauCounterexamples.compact_polynomial_gaussian line 298