OAI/Probability/LogConcave/Numerics/VelocityWorkCoefficient.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.MeanTree.flowWork_bound line 11
2. lemma OAI.LogConcaveSampling.MeanTree.kernelWork_bound line 22
3. def OAI.LogConcaveSampling.MeanTree.velocityWorkCoefficient line 47
4. lemma OAI.LogConcaveSampling.MeanTree.velocityWork_bound line 49
5. lemma OAI.LogConcaveSampling.MeanTree.vectorPicard_zero_bound line 65
6. lemma OAI.LogConcaveSampling.MeanTree.meanWork_polynomial line 81