OAI/Probability/SKSupport/Regularity/Regularity.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ZeroTemperatureSK.approxValue line 15
  2. def OAI.ZeroTemperatureSK.approxError line 18
  3. lemma OAI.ZeroTemperatureSK.approxError_limit line 21
  4. lemma OAI.ZeroTemperatureSK.approxValue_error line 33
  5. lemma OAI.ZeroTemperatureSK.approxValue_uniform line 43
  6. lemma OAI.ZeroTemperatureSK.approxValue_uniform_spatial line 52
  7. lemma OAI.ZeroTemperatureSK.approxValue_regular line 61
  8. lemma OAI.ZeroTemperatureSK.approxValue_uniform_derivative_bounds line 66
  9. theorem OAI.ZeroTemperatureSK.value_contDiff line 86
  10. lemma OAI.ZeroTemperatureSK.approxValue_derivative_uniform_spatial line 95
  11. theorem OAI.ZeroTemperatureSK.value_uniform_derivative_bounds line 106
  12. lemma OAI.ZeroTemperatureSK.cascade_even line 127
  13. lemma OAI.ZeroTemperatureSK.finiteValue_even line 136
  14. theorem OAI.ZeroTemperatureSK.value_even line 155
  15. lemma OAI.ZeroTemperatureSK.gradient_odd line 164
  16. lemma OAI.ZeroTemperatureSK.gradient_zero line 177
  17. lemma OAI.ZeroTemperatureSK.gradient_monotone line 183
  18. lemma OAI.ZeroTemperatureSK.curvature_nonneg line 190