OAI/Dynamics/EntropyCounterexample/ReadoutCover.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.readoutCenter line 8
  2. def OAI.Problem340.readoutBump line 10
  3. def OAI.Problem340.readoutCoeff line 13
  4. def OAI.Problem340.readoutInterval line 15
  5. theorem OAI.Problem340.readoutCoeff_contDiff line 18
  6. theorem OAI.Problem340.readoutCoeff_nonneg line 21
  7. theorem OAI.Problem340.readoutCoeff_le_one line 24
  8. theorem OAI.Problem340.readoutCoeff_support line 27
  9. theorem OAI.Problem340.readoutInterval_length line 36
  10. theorem OAI.Problem340.readoutCenter_bounds line 39
  11. theorem OAI.Problem340.readoutInterval_subset line 47
  12. theorem OAI.Problem340.readoutCoeff_eq_one line 54
  13. theorem OAI.Problem340.readoutCoeff_cover line 59
  14. def OAI.Problem340.preparationBump line 74
  15. def OAI.Problem340.preparationCoeff line 77
  16. theorem OAI.Problem340.preparationCoeff_contDiff line 79
  17. theorem OAI.Problem340.preparationCoeff_nonneg line 82
  18. theorem OAI.Problem340.preparationCoeff_le_one line 85
  19. theorem OAI.Problem340.preparationCoeff_support line 88
  20. theorem OAI.Problem340.preparationCoeff_eq_one line 96
  21. theorem OAI.Problem340.readoutCoeff_hasCompactSupport line 102
  22. theorem OAI.Problem340.preparationCoeff_hasCompactSupport line 105
  23. theorem OAI.Problem340.readoutCoeff_tsupport_subset line 108
  24. theorem OAI.Problem340.readoutCoeff_closed_support_interval line 119
  25. theorem OAI.Problem340.exists_readoutCoeff_fderiv_bound line 127
  26. theorem OAI.Problem340.exists_preparationCoeff_fderiv_bound line 143