OAI/Probability/SKSupport/Regularity/PositiveRegularity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ZeroTemperatureSK.positiveValue line 13
  2. def OAI.ZeroTemperatureSK.positiveError line 16
  3. lemma OAI.ZeroTemperatureSK.positiveError_limit line 19
  4. lemma OAI.ZeroTemperatureSK.positiveValue_error line 31
  5. lemma OAI.ZeroTemperatureSK.positiveValue_uniform line 41
  6. lemma OAI.ZeroTemperatureSK.positiveValue_uniform_spatial line 50
  7. lemma OAI.ZeroTemperatureSK.positiveValue_regular line 59
  8. lemma OAI.ZeroTemperatureSK.positiveValue_uniform_derivative_bounds line 64
  9. theorem OAI.ZeroTemperatureSK.positive_limit_contDiff line 85
  10. lemma OAI.ZeroTemperatureSK.positiveValue_derivative_uniform_spatial line 94
  11. theorem OAI.ZeroTemperatureSK.positive_limit_derivative_bounds line 105
  12. lemma OAI.ZeroTemperatureSK.positiveValue_derivative_uniform line 115