OAI/Probability/SKSupport/Regularity/ClosedTime.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ZeroTemperatureSK.ClosedTime line 12
  2. def OAI.ZeroTemperatureSK.closedFiltration line 16
  3. def OAI.ZeroTemperatureSK.terminalGradient line 22
  4. abbrev OAI.ZeroTemperatureSK.GaussianSample line 26
  5. def OAI.ZeroTemperatureSK.gaussianLaw line 28
  6. def OAI.ZeroTemperatureSK.gaussianCoordinate line 31
  7. def OAI.ZeroTemperatureSK.meshStep line 34
  8. def OAI.ZeroTemperatureSK.meshTime line 36
  9. def OAI.ZeroTemperatureSK.eulerState line 38
  10. def OAI.ZeroTemperatureSK.eulerCurvatureMoment line 45
  11. def OAI.ZeroTemperatureSK.eulerNormalizer line 49
  12. def OAI.ZeroTemperatureSK.normalizedIncrement line 52
  13. def OAI.ZeroTemperatureSK.randomizedSign line 58
  14. def OAI.ZeroTemperatureSK.gaussianCoeffA line 63
  15. def OAI.ZeroTemperatureSK.gaussianCoeffB line 68
  16. def OAI.ZeroTemperatureSK.gaussianValueSum line 72