OAI/Probability/LogConcave/Sampling/NumericalLayerCount.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.probabilityNormalizedTerm_rate line 12
2. lemma OAI.LogConcaveSampling.harmonicNormalizedTerm_rate line 17
3. lemma OAI.LogConcaveSampling.kernelNormalizedTerm_rate line 26
4. lemma OAI.LogConcaveSampling.kernelActionNormalizedBudget_rate line 36
5. lemma OAI.LogConcaveSampling.kernelAnalyticNormalizedBudget_rate line 65
6. lemma OAI.LogConcaveSampling.velocityNormalizedBudget_rate line 77
7. def OAI.LogConcaveSampling.numericalLayerCount line 100
8. lemma OAI.LogConcaveSampling.numericalLayerCount_bound line 102
9. lemma OAI.LogConcaveSampling.exists_numerical_order line 104
10. theorem OAI.LogConcaveSampling.numerical_exponent_margins line 118
11. lemma OAI.LogConcaveSampling.numerical_t_small line 139