OAI/Probability/LogConcave/JetEstimates/PolySmooth.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.LogConcaveSampling.PolySmooth line 22
2. lemma OAI.LogConcaveSampling.PolySmooth.jet_growth line 29
3. lemma OAI.LogConcaveSampling.PolySmooth.directional line 34
4. lemma OAI.LogConcaveSampling.PolySmooth.jet line 41
5. lemma OAI.LogConcaveSampling.PolySmooth.polyC1 line 47
6. lemma OAI.LogConcaveSampling.PolySmooth.add line 50
7. lemma OAI.LogConcaveSampling.PolySmooth.neg line 55
8. lemma OAI.LogConcaveSampling.PolySmooth.mul line 61
9. lemma OAI.LogConcaveSampling.PolySmooth.sum line 74
10. lemma OAI.LogConcaveSampling.PolySmooth.adjoint line 80
11. lemma OAI.LogConcaveSampling.PolySmooth.const line 84
12. lemma OAI.LogConcaveSampling.PolySmooth.prod line 89
13. lemma OAI.LogConcaveSampling.PolySmooth.integrable line 99
14. lemma OAI.LogConcaveSampling.PolySmooth.tensorAdjoint line 103