OAI/Dynamics/EntropyCounterexample/Saturation.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.saturationDerivative line 12
  2. def OAI.Problem340.saturationPrimitive line 15
  3. theorem OAI.Problem340.saturationPrimitive_hasDerivAt line 18
  4. theorem OAI.Problem340.saturationPrimitive_contDiff line 25
  5. theorem OAI.Problem340.saturationPrimitive_nonneg line 33
  6. theorem OAI.Problem340.saturationPrimitive_eq_self line 37
  7. theorem OAI.Problem340.saturationPrimitive_monotone line 50
  8. theorem OAI.Problem340.saturationPrimitive_eq_at_two line 55
  9. theorem OAI.Problem340.saturationPrimitive_le_two line 74
  10. def OAI.Problem340.saturationCutoff line 90
  11. def OAI.Problem340.saturationProfile line 93
  12. theorem OAI.Problem340.saturationProfile_contDiff line 96
  13. theorem OAI.Problem340.saturationProfile_nonneg line 100
  14. theorem OAI.Problem340.saturationProfile_le_two line 104
  15. theorem OAI.Problem340.saturationProfile_eq_primitive line 111
  16. theorem OAI.Problem340.saturationProfile_eq_self line 117
  17. theorem OAI.Problem340.saturationProfile_eq_zero line 121
  18. theorem OAI.Problem340.saturationProfile_monotoneOn line 128
  19. def OAI.Problem340.saturation line 135
  20. theorem OAI.Problem340.saturation_zero line 138
  21. theorem OAI.Problem340.saturation_eq_self line 142
  22. theorem OAI.Problem340.saturation_eq_zero line 151
  23. theorem OAI.Problem340.norm_saturation line 155
  24. theorem OAI.Problem340.norm_saturation_le_two line 164
  25. theorem OAI.Problem340.saturation_contDiff line 169
  26. theorem OAI.Problem340.saturation_hasCompactSupport line 183
  27. def OAI.Problem340.sphereSaturation line 194
  28. theorem OAI.Problem340.sphereSaturation_infty line 197
  29. theorem OAI.Problem340.sphereSaturation_coe line 200
  30. theorem OAI.Problem340.sphereSaturation_continuous line 203
  31. theorem OAI.Problem340.norm_sphereSaturation_le_two line 210
  32. theorem OAI.Problem340.saturation_inv_eventually_zero line 216
  33. theorem OAI.Problem340.saturation_inv_contDiff line 230