OAI/Geometry/SmoothYau/Smoothness/FlowParameters.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.YauCounterexamples.continuousMapApply line 33
  2. lemma OAI.YauCounterexamples.continuousMapApply_apply line 43
  3. lemma OAI.YauCounterexamples.continuousMapApply_norm_le line 46
  4. def OAI.YauCounterexamples.continuousMapApplyCLM line 53
  5. def OAI.YauCounterexamples.superposition line 64
  6. lemma OAI.YauCounterexamples.superposition_apply line 68
  7. lemma OAI.YauCounterexamples.hasFDerivAt_superposition line 73
  8. lemma OAI.YauCounterexamples.contDiff_nat_superposition line 112
  9. theorem OAI.YauCounterexamples.contDiff_superposition line 130
  10. theorem OAI.YauCounterexamples.smooth_inverse_on line 157
  11. abbrev OAI.YauCounterexamples.FlowParameters line 213
  12. def OAI.YauCounterexamples.flowIntegralMap line 215
  13. lemma OAI.YauCounterexamples.flowIntegralMap_smooth line 218
  14. def OAI.YauCounterexamples.flowIntegralDerivative line 224
  15. lemma OAI.YauCounterexamples.flowIntegralMap_derivative line 234
  16. theorem OAI.YauCounterexamples.smooth_integral_paths line 251