OAI/Probability/LogConcave/Sampling/ContinuousFirstOrderReply.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LogConcaveSampling.Admissible.continuous_firstOrderReply line 15
  2. theorem OAI.LogConcaveSampling.OracleAlgorithm.measurable_history line 22
  3. theorem OAI.LogConcaveSampling.OracleAlgorithm.measurable_run line 41
  4. theorem OAI.LogConcaveSampling.queryComplexity_le_of_canSample line 46
  5. theorem OAI.LogConcaveSampling.quadratic_lower_bound_of_hasDerivAt line 55
  6. theorem OAI.LogConcaveSampling.quadratic_bounds_of_hasDerivAt line 89
  7. theorem OAI.LogConcaveSampling.Admissible.contDiff_gradient line 100
  8. theorem OAI.LogConcaveSampling.Admissible.quadratic_bounds line 105
  9. theorem OAI.LogConcaveSampling.integrable_gaussian_envelope line 132
  10. theorem OAI.LogConcaveSampling.Admissible.integrable_exp_neg line 140
  11. theorem OAI.LogConcaveSampling.Admissible.partition_ne_top line 151
  12. theorem OAI.LogConcaveSampling.Admissible.partition_pos line 158
  13. theorem OAI.LogConcaveSampling.Admissible.isProbabilityMeasure_gibbs line 169