OAI/Probability/LogConcave/Complexity/TerminalDerivativeBudget.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.terminalDerivativeBudget line 15
2. lemma OAI.LogConcaveSampling.terminalDerivativeBudget_nonneg line 19
3. lemma OAI.LogConcaveSampling.terminalActionChain_sq_uniform line 30
4. lemma OAI.LogConcaveSampling.terminal_cell_budget_cancel line 47
5. theorem OAI.LogConcaveSampling.terminal_derivative_cell_rms line 66
6. theorem OAI.LogConcaveSampling.terminal_hermite_cell_rms line 96