OAI/Probability/LogConcave/Dynamics/TriangularEquiv.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.GlobalODE.triangularEquiv line 26
2. lemma OAI.LogConcaveSampling.GlobalODE.spaceTimeForward_time_deriv line 46
3. theorem OAI.LogConcaveSampling.GlobalODE.spaceTimeForward_hasFDerivAt line 59
4. theorem OAI.LogConcaveSampling.GlobalODE.spaceTimeBackward_differentiableAt line 80
5. def OAI.LogConcaveSampling.GlobalODE.backwardTest line 95
6. lemma OAI.LogConcaveSampling.GlobalODE.backwardTest_eq line 98
7. lemma OAI.LogConcaveSampling.GlobalODE.backwardTest_continuous line 103
8. lemma OAI.LogConcaveSampling.GlobalODE.backwardTest_lipschitz line 108
9. lemma OAI.LogConcaveSampling.GlobalODE.backwardTest_differentiableAt line 125
10. theorem OAI.LogConcaveSampling.GlobalODE.backwardTest_material_zero line 133
11. theorem OAI.LogConcaveSampling.GlobalODE.backwardTest_chain line 170
12. lemma OAI.LogConcaveSampling.GlobalODE.backwardTest_spatial_derivative_bound line 190
13. theorem OAI.LogConcaveSampling.GlobalODE.transport_expectation_of_flux line 202