OAI/Probability/LogConcave/Analysis/Operator.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.EulerGeometry.gaussian_noise_product line 24
  2. lemma OAI.LogConcaveSampling.EulerGeometry.bounded_integrable line 35
  3. def OAI.LogConcaveSampling.EulerGeometry.operator line 40
  4. lemma OAI.LogConcaveSampling.EulerGeometry.measurable_operator line 43
  5. lemma OAI.LogConcaveSampling.EulerGeometry.operator_bound line 48
  6. lemma OAI.LogConcaveSampling.EulerGeometry.operator_zero line 56
  7. theorem OAI.LogConcaveSampling.EulerGeometry.iterated_defect line 60
  8. lemma OAI.LogConcaveSampling.EulerGeometry.measurable_iterate line 90
  9. lemma OAI.LogConcaveSampling.EulerGeometry.integral_iterate line 99
  10. lemma OAI.LogConcaveSampling.EulerGeometry.integral_iterate_gaussian line 121
  11. lemma OAI.LogConcaveSampling.EulerGeometry.iterate_operator_bound line 131
  12. lemma OAI.LogConcaveSampling.EulerGeometry.measurable_iterate_operator line 139
  13. lemma OAI.LogConcaveSampling.EulerGeometry.iterate_operator_modulus line 147
  14. theorem OAI.LogConcaveSampling.EulerGeometry.integral_collapse line 176
  15. theorem OAI.LogConcaveSampling.EulerGeometry.expectations_tendsto line 218
  16. lemma OAI.LogConcaveSampling.EulerGeometry.compact_test_lipschitz line 256
  17. theorem OAI.LogConcaveSampling.EulerGeometry.poincare_of_euler_approximation line 264
  18. theorem OAI.LogConcaveSampling.EulerGeometry.exists_consistent_schedule line 332
  19. lemma OAI.LogConcaveSampling.EulerGeometry.contraction_geometric_bound line 373
  20. lemma OAI.LogConcaveSampling.EulerGeometry.schedule_contraction_tendsto line 386
  21. lemma OAI.LogConcaveSampling.euler_noise_energy_bound line 402
  22. lemma OAI.LogConcaveSampling.euler_operator_gibbs_defect line 415
  23. theorem OAI.LogConcaveSampling.Primitive.poincare_compact line 431
  24. def OAI.LogConcaveSampling.PoincareCutoff.bump line 496
  25. def OAI.LogConcaveSampling.PoincareCutoff.cutoff line 497
  26. lemma OAI.LogConcaveSampling.PoincareCutoff.cutoff_smooth line 499
  27. lemma OAI.LogConcaveSampling.PoincareCutoff.cutoff_compact line 502
  28. lemma OAI.LogConcaveSampling.PoincareCutoff.cutoff_nonneg line 506
  29. lemma OAI.LogConcaveSampling.PoincareCutoff.cutoff_le_one line 507
  30. lemma OAI.LogConcaveSampling.PoincareCutoff.cutoff_abs line 508
  31. lemma OAI.LogConcaveSampling.PoincareCutoff.cutoff_tendsto line 512
  32. lemma OAI.LogConcaveSampling.PoincareCutoff.exists_derivative_bound line 521
  33. lemma OAI.LogConcaveSampling.PoincareCutoff.cutoff_derivative_tendsto line 536
  34. def OAI.LogConcaveSampling.PoincareCutoff.truncation line 544
  35. lemma OAI.LogConcaveSampling.PoincareCutoff.truncation_smooth line 546
  36. lemma OAI.LogConcaveSampling.PoincareCutoff.truncation_compact line 549
  37. lemma OAI.LogConcaveSampling.PoincareCutoff.truncation_tendsto line 552
  38. lemma OAI.LogConcaveSampling.PoincareCutoff.truncation_derivative line 556
  39. lemma OAI.LogConcaveSampling.PoincareCutoff.truncation_derivative_tendsto line 561
  40. lemma OAI.LogConcaveSampling.PoincareCutoff.truncation_abs line 569
  41. lemma OAI.LogConcaveSampling.PoincareCutoff.truncation_derivative_bound line 573
  42. theorem OAI.LogConcaveSampling.PoincareCutoff.extend line 591