OAI/Probability/SKSupport/Diffusion/CompactDrift.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ZeroTemperatureSK.stripClamp line 16
  2. lemma OAI.ZeroTemperatureSK.stripClamp_mem line 18
  3. lemma OAI.ZeroTemperatureSK.stripClamp_eq line 21
  4. lemma OAI.ZeroTemperatureSK.continuous_stripClamp line 24
  5. def OAI.ZeroTemperatureSK.compactGradient line 29
  6. def OAI.ZeroTemperatureSK.compactCoeff line 32
  7. def OAI.ZeroTemperatureSK.compactDrift line 34
  8. lemma OAI.ZeroTemperatureSK.compactGradient_continuous line 37
  9. lemma OAI.ZeroTemperatureSK.compactGradient_bound line 46
  10. lemma OAI.ZeroTemperatureSK.compactCoeff_measurable line 51
  11. lemma OAI.ZeroTemperatureSK.compactCoeff_bounds line 54
  12. lemma OAI.ZeroTemperatureSK.compactDrift_measurable line 61
  13. lemma OAI.ZeroTemperatureSK.compactDrift_bound line 67
  14. lemma OAI.ZeroTemperatureSK.compactGradient_lipschitz line 74
  15. lemma OAI.ZeroTemperatureSK.compactDrift_lipschitz line 89
  16. lemma OAI.ZeroTemperatureSK.compactDrift_eq line 108
  17. def OAI.ZeroTemperatureSK.diffusionHorizon line 124
  18. lemma OAI.ZeroTemperatureSK.diffusionHorizon_mem line 126
  19. lemma OAI.ZeroTemperatureSK.diffusionHorizon_tendsto line 133
  20. lemma OAI.ZeroTemperatureSK.eventually_le_diffusionHorizon line 138
  21. def OAI.ZeroTemperatureSK.diffusionHorizonTime line 142
  22. def OAI.ZeroTemperatureSK.stripDrift line 146
  23. lemma OAI.ZeroTemperatureSK.stripDrift_eq line 154
  24. def OAI.ZeroTemperatureSK.localDiffusion line 158
  25. lemma OAI.ZeroTemperatureSK.localDiffusion_progressive line 161
  26. lemma OAI.ZeroTemperatureSK.localDiffusion_agree line 166
  27. def OAI.ZeroTemperatureSK.rawDiffusion line 176
  28. lemma OAI.ZeroTemperatureSK.rawDiffusion_progressive line 179
  29. lemma OAI.ZeroTemperatureSK.rawDiffusion_eq_local line 190
  30. lemma OAI.ZeroTemperatureSK.rawDiffusion_eq_integral line 198
  31. def OAI.ZeroTemperatureSK.beforeOneGradient line 217
  32. lemma OAI.ZeroTemperatureSK.beforeOneGradient_measurable line 220
  33. lemma OAI.ZeroTemperatureSK.beforeOneGradient_bound line 244
  34. def OAI.ZeroTemperatureSK.rawFeedback line 251
  35. lemma OAI.ZeroTemperatureSK.rawFeedback_progressive line 254
  36. lemma OAI.ZeroTemperatureSK.rawFeedback_bound line 261
  37. lemma OAI.ZeroTemperatureSK.rawFeedback_eq line 264
  38. lemma OAI.ZeroTemperatureSK.rawDrift_integrable line 269
  39. def OAI.ZeroTemperatureSK.diffusion line 275
  40. lemma OAI.ZeroTemperatureSK.diffusion_progressive line 278
  41. lemma OAI.ZeroTemperatureSK.diffusion_eq_raw line 289
  42. lemma OAI.ZeroTemperatureSK.diffusion_continuous line 301
  43. lemma OAI.ZeroTemperatureSK.diffusion_zero line 306
  44. theorem OAI.ZeroTemperatureSK.diffusion_isDiffusion line 309