OAI/Probability/LogConcave/Sampling/TerminalJacobianInverse.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LogConcaveSampling.terminalJacobian_inverse line 18
2. lemma OAI.LogConcaveSampling.terminalJacobian_final line 51
3. theorem OAI.LogConcaveSampling.terminalJacobian_deriv line 77
4. theorem OAI.LogConcaveSampling.terminalJacobian_deriv_closed line 145
5. lemma OAI.LogConcaveSampling.terminalJacobian_initial_deriv line 171
6. lemma OAI.LogConcaveSampling.terminalJacobian_action_initial_deriv line 178
7. theorem OAI.LogConcaveSampling.terminalJacobian_action_deriv line 203
8. theorem OAI.LogConcaveSampling.terminalJacobian_action_quotient line 212
9. theorem OAI.LogConcaveSampling.terminalJacobian_action_quotient_limit line 222