OAI/Dynamics/EntropyCounterexample/SkewProduct.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem340.RawState line 11
  2. def OAI.Problem340.rawQuadratic line 13
  3. theorem OAI.Problem340.continuous_rawQuadratic line 16
  4. def OAI.Problem340.rawUpdate line 19
  5. def OAI.Problem340.rawUpdateAtTime line 24
  6. def OAI.Problem340.rawNormalForm line 29
  7. theorem OAI.Problem340.rawUpdateAtTime_zero line 33
  8. theorem OAI.Problem340.rawUpdateAtTime_one line 38
  9. theorem OAI.Problem340.continuous_rawUpdate line 43
  10. theorem OAI.Problem340.continuous_rawUpdateAtTime line 54
  11. theorem OAI.Problem340.continuous_rawNormalForm line 71
  12. def OAI.Problem340.rawUpdateHomotopy line 78
  13. theorem OAI.Problem340.rawUpdate_not_surjective line 90
  14. theorem OAI.Problem340.rawUpdate_not_bijective line 98