OAI/Probability/LogConcave/Analysis/EulerDrift.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LogConcaveSampling.Primitive.contDiff_potential line 19
  2. theorem OAI.LogConcaveSampling.Primitive.gradient_potential line 24
  3. theorem OAI.LogConcaveSampling.Primitive.gradient_potential_lipschitz line 45
  4. theorem OAI.LogConcaveSampling.Primitive.gaussianLowerTail line 53
  5. lemma OAI.LogConcaveSampling.partition_pos_of_continuous line 73
  6. lemma OAI.LogConcaveSampling.partition_ne_top_of_integrable line 83
  7. lemma OAI.LogConcaveSampling.probability_gibbs_of_partition line 88
  8. lemma OAI.LogConcaveSampling.lipschitz_sq_norm_growth line 94
  9. theorem OAI.LogConcaveSampling.Primitive.gradient_sq_integrable line 105
  10. def OAI.LogConcaveSampling.eulerDrift line 122
  11. lemma OAI.LogConcaveSampling.Primitive.eulerDrift_eq line 125
  12. lemma OAI.LogConcaveSampling.Primitive.eulerDrift_lipschitz line 133
  13. lemma OAI.LogConcaveSampling.Primitive.contDiff_eulerDrift line 151
  14. def OAI.LogConcaveSampling.GaussianPoincare.rotation line 174
  15. lemma OAI.LogConcaveSampling.GaussianPoincare.rotation_apply line 181
  16. lemma OAI.LogConcaveSampling.GaussianPoincare.rotation_energy line 186
  17. theorem OAI.LogConcaveSampling.GaussianPoincare.rotation_gaussian line 193
  18. lemma OAI.LogConcaveSampling.GaussianPoincare.integral_dual_sq line 232
  19. lemma OAI.LogConcaveSampling.GaussianPoincare.interval_integral_sq_le line 240
  20. lemma OAI.LogConcaveSampling.GaussianPoincare.rotation_first_deriv line 261
  21. lemma OAI.LogConcaveSampling.GaussianPoincare.along_rotation_deriv line 267
  22. lemma OAI.LogConcaveSampling.GaussianPoincare.rotation_difference_bound line 274
  23. lemma OAI.LogConcaveSampling.GaussianPoincare.memLp_lipschitz line 289
  24. lemma OAI.LogConcaveSampling.GaussianPoincare.independent_difference_variance line 298
  25. lemma OAI.LogConcaveSampling.GaussianPoincare.tangent_sq_bound line 319
  26. lemma OAI.LogConcaveSampling.GaussianPoincare.unrotated_integrable line 340
  27. lemma OAI.LogConcaveSampling.GaussianPoincare.integral_tangent_sq line 357
  28. lemma OAI.LogConcaveSampling.GaussianPoincare.tangent_time_integrable line 368
  29. theorem OAI.LogConcaveSampling.GaussianPoincare.variance_le_gradient line 398
  30. def OAI.LogConcaveSampling.EulerGeometry.iterate line 444
  31. def OAI.LogConcaveSampling.EulerGeometry.energy line 448
  32. lemma OAI.LogConcaveSampling.EulerGeometry.energy_nonneg line 452
  33. lemma OAI.LogConcaveSampling.EulerGeometry.energy_eq_sum line 457
  34. lemma OAI.LogConcaveSampling.EulerGeometry.energy_le line 465
  35. lemma OAI.LogConcaveSampling.EulerGeometry.initial_contraction line 478
  36. lemma OAI.LogConcaveSampling.EulerGeometry.noise_sensitivity line 492
  37. lemma OAI.LogConcaveSampling.EulerGeometry.noise_lipschitz line 534
  38. lemma OAI.LogConcaveSampling.EulerGeometry.contDiff_iterate line 544
  39. lemma OAI.LogConcaveSampling.EulerGeometry.contDiff_noise line 553
  40. theorem OAI.LogConcaveSampling.GaussianPoincare.variance_lipschitz_image line 571