OAI/Probability/LogConcave/Sampling/TerminalBackward.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.probabilityTransport_cocycle line 19
  2. lemma OAI.LogConcaveSampling.probabilityTransport_initial line 24
  3. lemma OAI.LogConcaveSampling.probabilityTransport_continuous line 26
  4. lemma OAI.LogConcaveSampling.interpolationLaw_zero line 31
  5. lemma OAI.LogConcaveSampling.probabilityTransport_from_zero line 39
  6. theorem OAI.LogConcaveSampling.probabilityTransport_pushforward line 66
  7. lemma OAI.LogConcaveSampling.smoothTimeClip_mem_extended line 91
  8. def OAI.LogConcaveSampling.terminalBackward line 96
  9. def OAI.LogConcaveSampling.terminalForward line 102
  10. lemma OAI.LogConcaveSampling.terminalBackward_smooth line 108
  11. lemma OAI.LogConcaveSampling.terminalForward_smooth line 119
  12. lemma OAI.LogConcaveSampling.probabilityTransport_eq_extended line 131
  13. lemma OAI.LogConcaveSampling.terminalBackward_eq line 149
  14. lemma OAI.LogConcaveSampling.terminalForward_eq line 154
  15. lemma OAI.LogConcaveSampling.terminalForward_backward line 161
  16. lemma OAI.LogConcaveSampling.terminalBackward_forward line 164