OAI/Probability/LogConcave/Complexity/CenteringStateBudget.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.centeringSkew_inv_scaled line 14
2. lemma OAI.LogConcaveSampling.identityArray_polySmooth line 27
3. lemma OAI.LogConcaveSampling.identityArray_inv_energy line 32
4. def OAI.LogConcaveSampling.centeringStateBudget line 43
5. def OAI.LogConcaveSampling.centeringMeanBudget line 47
6. theorem OAI.LogConcaveSampling.centering_state_taylor_uniform line 52
7. theorem OAI.LogConcaveSampling.centering_mean_taylor_uniform line 98