OAI/Probability/SKSupport/Parabolic/ForwardGeometry.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ZeroTemperatureSK.Heat.forwardTime line 12
  2. def OAI.ZeroTemperatureSK.Heat.forwardScale line 13
  3. def OAI.ZeroTemperatureSK.Heat.forwardVariance line 14
  4. def OAI.ZeroTemperatureSK.Heat.forwardCorrection line 16
  5. def OAI.ZeroTemperatureSK.Heat.forwardScore line 20
  6. lemma OAI.ZeroTemperatureSK.Heat.forwardTime_pos line 23
  7. lemma OAI.ZeroTemperatureSK.Heat.forwardScale_pos line 26
  8. lemma OAI.ZeroTemperatureSK.Heat.forwardScale_le_one line 29
  9. lemma OAI.ZeroTemperatureSK.Heat.forwardVariance_nonneg line 33
  10. lemma OAI.ZeroTemperatureSK.Heat.forwardVariance_le line 36
  11. lemma OAI.ZeroTemperatureSK.Heat.continuous_forwardTime line 41
  12. lemma OAI.ZeroTemperatureSK.Heat.continuous_forwardScale line 43
  13. lemma OAI.ZeroTemperatureSK.Heat.continuous_forwardVariance line 45
  14. lemma OAI.ZeroTemperatureSK.Heat.hasDerivAt_forwardTime line 49
  15. lemma OAI.ZeroTemperatureSK.Heat.hasDerivAt_forwardScale line 54
  16. lemma OAI.ZeroTemperatureSK.Heat.hasDerivAt_forwardVariance line 59
  17. lemma OAI.ZeroTemperatureSK.Heat.forwardVariance_pos line 72
  18. lemma OAI.ZeroTemperatureSK.Heat.forwardCorrection_terminal line 75