OAI/Probability/LogConcave/Sampling/ProbabilityEndpoint.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.centering_transport_joint_law line 14
2. lemma OAI.LogConcaveSampling.kernelTransportAction_terminal line 29
3. lemma OAI.LogConcaveSampling.rms_bound_pushforward line 40
4. def OAI.LogConcaveSampling.probabilityEndpoint line 62
5. lemma OAI.LogConcaveSampling.probabilityEndpoint_time line 66