OAI/Geometry/SmoothYau/Smoothness/LinearPowerDirectional.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.stereoAux_directional line 23
  2. theorem OAI.YauCounterexamples.stereoAux_second_jet line 41
  3. def OAI.YauCounterexamples.roundChart line 69
  4. lemma OAI.YauCounterexamples.roundChart_smooth line 71
  5. lemma OAI.YauCounterexamples.roundChart_zero line 74
  6. lemma OAI.YauCounterexamples.roundChart_first line 77
  7. lemma OAI.YauCounterexamples.roundChart_directional line 86
  8. lemma OAI.YauCounterexamples.roundChart_second line 94
  9. theorem OAI.YauCounterexamples.roundChart_metric_first line 107
  10. lemma OAI.YauCounterexamples.linearPower_directional line 150
  11. lemma OAI.YauCounterexamples.roundLinearPower_directional line 155
  12. lemma OAI.YauCounterexamples.roundLinearPower_second line 164
  13. lemma OAI.YauCounterexamples.roundLinearPower_second_of_two_le line 185
  14. lemma OAI.YauCounterexamples.fderiv_real_part line 196
  15. lemma OAI.YauCounterexamples.second_real_part line 201
  16. lemma OAI.YauCounterexamples.roundLinearPower_real_second line 208