OAI/Probability/LogConcave/Complexity/HarmonicCorrectionBudget.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.jointCorrectionArray_polySmooth line 16
2. def OAI.LogConcaveSampling.harmonicCorrectionBudget line 26
3. lemma OAI.LogConcaveSampling.harmonicCorrectionBudget_nonneg line 31
4. def OAI.LogConcaveSampling.harmonicMeanBudget line 34
5. lemma OAI.LogConcaveSampling.harmonicMeanBudget_nonneg line 39
6. theorem OAI.LogConcaveSampling.harmonic_correction_taylor_rms line 42
7. theorem OAI.LogConcaveSampling.harmonic_mean_taylor_uniform line 89