OAI/Geometry/SmoothYau/Smoothness/NormalJetMapFirstPhase.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.exists_metric_orthonormal_frame line 51
  2. def OAI.YauCounterexamples.normalJetMap line 71
  3. lemma OAI.YauCounterexamples.contDiff_normalJetMap line 75
  4. lemma OAI.YauCounterexamples.normalJetMap_zero line 80
  5. lemma OAI.YauCounterexamples.hasFDerivAt_normalJetMap line 84
  6. lemma OAI.YauCounterexamples.fderiv_normalJetMap line 99
  7. lemma OAI.YauCounterexamples.normalJetMap_local_diffeomorphism line 104
  8. def OAI.YauCounterexamples.normalMetricTensor line 118
  9. lemma OAI.YauCounterexamples.normalMetricTensor_is_pullback line 123
  10. lemma OAI.YauCounterexamples.normalMetricTensor_at_zero line 132
  11. lemma OAI.YauCounterexamples.contDiff_normalMetricTensor_apply line 137
  12. lemma OAI.YauCounterexamples.normalMetricTensor_normal_jet line 146
  13. theorem OAI.YauCounterexamples.exists_smooth_normal_coordinate_jet line 181
  14. lemma OAI.YauCounterexamples.normalJetMap_remainder line 236
  15. lemma OAI.YauCounterexamples.normalJetMap_approximates line 244
  16. lemma OAI.YauCounterexamples.normalJetMap_derivative_invertible line 268
  17. lemma OAI.YauCounterexamples.normalJetMap_uniform_inverse line 292
  18. lemma OAI.YauCounterexamples.normalJetMap_first_phase_jet line 354
  19. lemma OAI.YauCounterexamples.normalJetMap_second_phase_jet line 363
  20. lemma OAI.YauCounterexamples.metricNormal_second_phase_jet line 385