OAI/Probability/LogConcave/Sampling/TimeBump.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.timeBump line 14
2. def OAI.LogConcaveSampling.smoothTimeClip line 16
3. lemma OAI.LogConcaveSampling.smoothTimeClip_contDiff line 18
4. lemma OAI.LogConcaveSampling.smoothTimeClip_eq line 21
5. lemma OAI.LogConcaveSampling.smoothTimeClip_sq_lt line 29
6. def OAI.LogConcaveSampling.smoothProbabilityVelocity line 44
7. lemma OAI.LogConcaveSampling.smoothProbabilityVelocity_contDiff line 48
8. def OAI.LogConcaveSampling.probabilityTransport line 61
9. lemma OAI.LogConcaveSampling.probabilityTransport_contDiff line 68
10. lemma OAI.LogConcaveSampling.conditionalFieldMean_neg_time line 103
11. lemma OAI.LogConcaveSampling.probabilityVelocity_neg_time line 109
12. lemma OAI.LogConcaveSampling.probabilityVelocity_lipschitz_signed line 113
13. lemma OAI.LogConcaveSampling.smoothProbabilityVelocity_lipschitz line 129
14. lemma OAI.LogConcaveSampling.smoothProbabilityVelocity_smooth line 136