OAI/Dynamics/EntropyCounterexample/Map.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem340.Construction.Sphere line 15
  2. abbrev OAI.Problem340.Construction.RawManifold line 16
  3. structure OAI.Problem340.Construction.SphereData line 18
  4. def OAI.Problem340.Construction.phase line 25
  5. theorem OAI.Problem340.Construction.phase_infty line 27
  6. theorem OAI.Problem340.Construction.phase_coe line 28
  7. theorem OAI.Problem340.Construction.phase_zero line 29
  8. def OAI.Problem340.Construction.prediction line 31
  9. def OAI.Problem340.Construction.predictedClock line 34
  10. def OAI.Problem340.Construction.inputTerm line 37
  11. def OAI.Problem340.Construction.baseInput line 41
  12. def OAI.Problem340.Construction.input line 44
  13. def OAI.Problem340.Construction.periodicReadout line 47
  14. def OAI.Problem340.Construction.periodicGain line 50
  15. def OAI.Problem340.Construction.clockIncrement line 53
  16. def OAI.Problem340.Construction.readout line 56
  17. def OAI.Problem340.Construction.rawMap line 59
  18. theorem OAI.Problem340.Construction.rawMap_main_infty line 65
  19. theorem OAI.Problem340.Construction.rawMap_register_ne_infty line 69
  20. theorem OAI.Problem340.Construction.rawMap_not_surjective line 72
  21. theorem OAI.Problem340.Construction.rawMap_not_bijective line 78
  22. theorem OAI.Problem340.Construction.inputTerm_infty line 81
  23. theorem OAI.Problem340.Construction.inputTerm_zero line 84
  24. theorem OAI.Problem340.Construction.baseInput_infty line 87
  25. theorem OAI.Problem340.Construction.baseInput_zero line 90
  26. theorem OAI.Problem340.Construction.input_infty line 93
  27. theorem OAI.Problem340.Construction.input_zero line 96
  28. theorem OAI.Problem340.Construction.norm_phase_le_one line 99
  29. theorem OAI.Problem340.Construction.norm_inputTerm_le line 107
  30. theorem OAI.Problem340.Construction.summable_norm_inputTerm line 135
  31. theorem OAI.Problem340.Construction.summable_inputTerm line 145
  32. theorem OAI.Problem340.Construction.norm_baseInput_le line 150