OAI/Probability/LogConcave/Sampling/ProbabilityVelocity.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.probabilityVelocity line 23
  2. lemma OAI.LogConcaveSampling.probabilityVelocity_joint_smooth line 26
  3. lemma OAI.LogConcaveSampling.probabilityVelocity_lipschitz line 33
  4. theorem OAI.LogConcaveSampling.exists_probability_trajectory line 48
  5. def OAI.LogConcaveSampling.clampedProbabilityVelocity line 85
  6. def OAI.LogConcaveSampling.clampedProbabilityDerivative line 89
  7. lemma OAI.LogConcaveSampling.clampedProbabilityVelocity_continuous line 94
  8. lemma OAI.LogConcaveSampling.clampedProbabilityDerivative_continuous line 108
  9. lemma OAI.LogConcaveSampling.clampedProbabilityVelocity_hasFDerivAt line 123
  10. lemma OAI.LogConcaveSampling.clampedProbabilityVelocity_lipschitz line 137
  11. lemma OAI.LogConcaveSampling.clampedProbabilityVelocity_eq line 144
  12. def OAI.LogConcaveSampling.interpolationPath line 153
  13. def OAI.LogConcaveSampling.interpolationPathDerivative line 156
  14. lemma OAI.LogConcaveSampling.interpolationPath_continuous line 159
  15. lemma OAI.LogConcaveSampling.interpolationPath_measurable line 162
  16. lemma OAI.LogConcaveSampling.interpolationPathDerivative_measurable line 165
  17. lemma OAI.LogConcaveSampling.interpolationPath_hasDerivAt line 168
  18. lemma OAI.LogConcaveSampling.interpolationPath_norm_le line 181
  19. lemma OAI.LogConcaveSampling.interpolationPathDerivative_norm_le line 194
  20. lemma OAI.LogConcaveSampling.interpolationPath_residual line 209
  21. lemma OAI.LogConcaveSampling.interpolationPath_defect line 225
  22. lemma OAI.LogConcaveSampling.interpolationPath_flux line 232
  23. lemma OAI.LogConcaveSampling.interpolationPath_defect_bound line 254
  24. def OAI.LogConcaveSampling.probabilityFlow line 289
  25. lemma OAI.LogConcaveSampling.probabilityFlow_continuous line 295