OAI/Probability/LogConcave/Analysis/Law.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.EulerGeometry.measurable_iterate_map line 15
  2. def OAI.LogConcaveSampling.EulerGeometry.law line 26
  3. lemma OAI.LogConcaveSampling.EulerGeometry.law_probability line 29
  4. theorem OAI.LogConcaveSampling.EulerGeometry.laws_tendsto line 33
  5. lemma OAI.LogConcaveSampling.EulerGeometry.comparison_iterate line 62
  6. lemma OAI.LogConcaveSampling.EulerGeometry.laws_distanceCoupled line 72
  7. theorem OAI.LogConcaveSampling.gibbs_distanceCoupled_of_euler line 102
  8. lemma OAI.LogConcaveSampling.gradient_contDiff_one line 178
  9. lemma OAI.LogConcaveSampling.hessian_euler_contraction line 182
  10. def OAI.LogConcaveSampling.posteriorPotential line 221
  11. lemma OAI.LogConcaveSampling.posterior_smooth line 224
  12. lemma OAI.LogConcaveSampling.posterior_gradient line 228
  13. lemma OAI.LogConcaveSampling.posterior_hessian line 246
  14. lemma OAI.LogConcaveSampling.posterior_tail line 257
  15. lemma OAI.LogConcaveSampling.posterior_gradient_lipschitz line 265
  16. lemma OAI.LogConcaveSampling.norm_sq_growth_of_lipschitz line 278
  17. lemma OAI.LogConcaveSampling.posterior_gradient_integrable line 288
  18. lemma OAI.LogConcaveSampling.posterior_euler_lipschitz line 309
  19. theorem OAI.LogConcaveSampling.posterior_distanceCoupled line 325
  20. lemma OAI.LogConcaveSampling.posterior_squaredCoupled line 358
  21. lemma OAI.LogConcaveSampling.measurable_gibbs_family line 378
  22. def OAI.LogConcaveSampling.gibbsKernel line 390
  23. lemma OAI.LogConcaveSampling.bounded_integrable line 394
  24. lemma OAI.LogConcaveSampling.bounded_integral line 400
  25. lemma OAI.LogConcaveSampling.gibbs_family_integral_measurable line 407
  26. def OAI.LogConcaveSampling.posteriorKernel line 412
  27. lemma OAI.LogConcaveSampling.posteriorKernel_probability line 418
  28. def OAI.LogConcaveSampling.jointPosteriorLaw line 425
  29. def OAI.LogConcaveSampling.noisedLaw line 428
  30. lemma OAI.LogConcaveSampling.noisedLaw_probability line 431
  31. lemma OAI.LogConcaveSampling.jointPosteriorLaw_probability line 437
  32. lemma OAI.LogConcaveSampling.jointPosterior_fst line 443
  33. lemma OAI.LogConcaveSampling.jointPosterior_snd line 449