OAI/Probability/SKSupport/Diffusion/PicardDiffusion.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ZeroTemperatureSK.BoundedLipschitzDrift line 14
  2. lemma OAI.ZeroTemperatureSK.progressive_time_measurable line 24
  3. lemma OAI.ZeroTemperatureSK.progressive_bounded_integrable line 29
  4. def OAI.ZeroTemperatureSK.timePrimitive line 37
  5. lemma OAI.ZeroTemperatureSK.timePrimitive_continuous line 40
  6. lemma OAI.ZeroTemperatureSK.timePrimitive_progressive line 46
  7. lemma OAI.ZeroTemperatureSK.timePrimitive_bound line 56
  8. def OAI.ZeroTemperatureSK.BoundedLipschitzDrift.action line 72
  9. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.action_progressive line 74
  10. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.action_bound line 81
  11. def OAI.ZeroTemperatureSK.BoundedLipschitzDrift.correctionIter line 84
  12. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.correctionIter_progressive line 88
  13. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.correctionIter_continuous line 94
  14. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.correctionIter_bound line 102
  15. def OAI.ZeroTemperatureSK.BoundedLipschitzDrift.rate line 111
  16. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.rate_pos line 113
  17. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.one_le_rate line 114
  18. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.integral_exp_rate line 116
  19. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.integral_exp_contraction line 126
  20. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.timePrimitive_action_sub_estimate line 139
  21. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.correctionIter_diff_bound line 163
  22. def OAI.ZeroTemperatureSK.BoundedLipschitzDrift.correction line 182
  23. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.correctionIter_tendsto line 185
  24. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.correction_progressive line 195
  25. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.correction_bound line 204
  26. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.correction_eq_integral line 210
  27. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.correction_continuous line 235
  28. def OAI.ZeroTemperatureSK.BoundedLipschitzDrift.solution line 244
  29. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.solution_progressive line 246
  30. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.solution_eq line 249
  31. lemma OAI.ZeroTemperatureSK.BoundedLipschitzDrift.solution_continuous line 257