OAI/Probability/LogConcave/Analysis/InterpolationPotential.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.conditionalPotential_smooth line 20
  2. lemma OAI.LogConcaveSampling.conditionalPotential_gradient line 26
  3. lemma OAI.LogConcaveSampling.conditionalPotential_gradient_lipschitz line 49
  4. lemma OAI.LogConcaveSampling.conditional_identity_integrable line 70
  5. lemma OAI.LogConcaveSampling.integral_scaled_affine_add line 79
  6. theorem OAI.LogConcaveSampling.conditional_mean_identity line 88
  7. lemma OAI.LogConcaveSampling.hasGradientAt_log_tiltedIntegral line 117
  8. lemma OAI.LogConcaveSampling.quadraticTilt_eq_tilted line 143
  9. def OAI.LogConcaveSampling.interpolationPotential line 149
  10. lemma OAI.LogConcaveSampling.hasGradientAt_interpolationPotential line 154
  11. lemma OAI.LogConcaveSampling.interpolationPotential_gradient line 193
  12. lemma OAI.LogConcaveSampling.map_snd_withDensity line 205
  13. lemma OAI.LogConcaveSampling.probability_density_eq_gibbs line 221
  14. def OAI.LogConcaveSampling.interpolationLaw line 230
  15. lemma OAI.LogConcaveSampling.interpolation_exponent line 234
  16. lemma OAI.LogConcaveSampling.interpolation_density_integral line 246
  17. lemma OAI.LogConcaveSampling.interpolationLaw_probability line 281
  18. theorem OAI.LogConcaveSampling.interpolationLaw_eq_gibbs line 290