OAI/Probability/LogConcave/Analysis/PrimitivePotentialModeBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LogConcaveSampling.primitivePotential_mode_bounds line 17
  2. theorem OAI.LogConcaveSampling.Primitive.exists_unique_mode line 37
  3. theorem OAI.LogConcaveSampling.Primitive.continuous_potential line 67
  4. theorem OAI.LogConcaveSampling.Primitive.integrable_exp_neg_potential line 73
  5. lemma OAI.LogConcaveSampling.polynomial_gaussian_absorb line 97
  6. lemma OAI.LogConcaveSampling.integrable_sq_norm_gaussian line 112
  7. theorem OAI.LogConcaveSampling.radial_integration_by_parts line 122
  8. lemma OAI.LogConcaveSampling.partition_toReal line 223
  9. lemma OAI.LogConcaveSampling.integral_gibbs line 230
  10. lemma OAI.LogConcaveSampling.integrable_gibbs_of_weighted line 241
  11. theorem OAI.LogConcaveSampling.Admissible.radial_gradient_lower line 263
  12. theorem OAI.LogConcaveSampling.Admissible.second_moment_bound line 284