OAI/Probability/LogConcave/Analysis/CenteringPotential.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.gradient_gaussianPotential line 18
  2. lemma OAI.LogConcaveSampling.gaussianPotential_gradient_lipschitz line 24
  3. def OAI.LogConcaveSampling.centeringPotential line 30
  4. def OAI.LogConcaveSampling.centeringMeanArray line 33
  5. def OAI.LogConcaveSampling.centeringGradientBound line 38
  6. lemma OAI.LogConcaveSampling.centeringPotential_gradient_lipschitz line 41
  7. lemma OAI.LogConcaveSampling.centeringMeanArray_polySmooth line 52
  8. lemma OAI.LogConcaveSampling.centeringMeanArray_energy line 58
  9. lemma OAI.LogConcaveSampling.centeringSkew_polySmooth line 72
  10. lemma OAI.LogConcaveSampling.centeringSkew_scaled_bound line 81
  11. lemma OAI.LogConcaveSampling.centeringScore_scaled_bound line 94
  12. lemma OAI.LogConcaveSampling.centeringMean_scaled_energy line 104
  13. theorem OAI.LogConcaveSampling.centering_mean_taylor_rms line 113
  14. theorem OAI.LogConcaveSampling.exists_centering_mean_taylor_rms line 169