OAI/Probability/LogConcave/Sampling/Directional.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.directional line 22
2. lemma OAI.LogConcaveSampling.directional_smooth line 25
3. lemma OAI.LogConcaveSampling.directional_mul line 29
4. lemma OAI.LogConcaveSampling.directional_add line 39
5. lemma OAI.LogConcaveSampling.directional_neg line 45
6. lemma OAI.LogConcaveSampling.directional_sum line 50
7. lemma OAI.LogConcaveSampling.directional_directional line 58
8. lemma OAI.LogConcaveSampling.directional_commute line 65
9. lemma OAI.LogConcaveSampling.directional_gradient line 73