OAI/Probability/LogConcave/JetEstimates/PolyC1.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.LogConcaveSampling.PolyC1 line 23
2. lemma OAI.LogConcaveSampling.integrable_polynomial_gibbs line 28
3. lemma OAI.LogConcaveSampling.PolyC1.continuous line 36
4. lemma OAI.LogConcaveSampling.PolyC1.differentiable line 37
5. lemma OAI.LogConcaveSampling.PolyC1.directional_continuous line 38
6. lemma OAI.LogConcaveSampling.PolyC1.add line 40
7. lemma OAI.LogConcaveSampling.PolyC1.neg line 44
8. lemma OAI.LogConcaveSampling.PolyC1.mul line 49
9. lemma OAI.LogConcaveSampling.PolyC1.sum line 54
10. def OAI.LogConcaveSampling.adjointCoordinate line 62
11. lemma OAI.LogConcaveSampling.adjointCoordinate_pairing line 65
12. def OAI.LogConcaveSampling.tensorAdjoint line 91
13. lemma OAI.LogConcaveSampling.tensorAdjoint_pairing line 95