OAI/Probability/LogConcave/Analysis/ProposalLog.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.EulerDefect.proposalLog line 21
  2. def OAI.LogConcaveSampling.EulerDefect.proposal line 24
  3. lemma OAI.LogConcaveSampling.EulerDefect.log_ratio line 27
  4. lemma OAI.LogConcaveSampling.EulerDefect.proposal_displacement line 36
  5. lemma OAI.LogConcaveSampling.EulerDefect.proposal_zero line 42
  6. lemma OAI.LogConcaveSampling.EulerDefect.differentiable_proposal line 44
  7. lemma OAI.LogConcaveSampling.EulerDefect.continuous_proposal line 48
  8. lemma OAI.LogConcaveSampling.EulerDefect.remainder_scaled_tendsto line 51
  9. lemma OAI.LogConcaveSampling.EulerDefect.scaled_log_ratio line 60
  10. theorem OAI.LogConcaveSampling.EulerDefect.scaled_log_ratio_tendsto line 70
  11. lemma OAI.LogConcaveSampling.EulerDefect.displacement_bound line 83
  12. lemma OAI.LogConcaveSampling.EulerDefect.gradient_norm_sq_difference_bound line 93
  13. lemma OAI.LogConcaveSampling.EulerDefect.scaled_log_ratio_bound line 106
  14. lemma OAI.LogConcaveSampling.EulerDefect.quadratic_dominator_bound line 144
  15. theorem OAI.LogConcaveSampling.EulerDefect.expected_scaled_log_ratio_tendsto line 165
  16. lemma OAI.LogConcaveSampling.MetropolisBalance.exp_gap line 209
  17. def OAI.LogConcaveSampling.MetropolisBalance.defectWeight line 222
  18. lemma OAI.LogConcaveSampling.MetropolisBalance.reverse_defect_integrable line 225
  19. lemma OAI.LogConcaveSampling.MetropolisBalance.integral_reverse_defect line 232
  20. lemma OAI.LogConcaveSampling.MetropolisBalance.density_gap_integrable line 241
  21. lemma OAI.LogConcaveSampling.MetropolisBalance.density_gap_bound line 251
  22. lemma OAI.LogConcaveSampling.MetropolisBalance.weighted_bounded_integrable line 266
  23. theorem OAI.LogConcaveSampling.MetropolisBalance.one_step_defect line 276
  24. def OAI.LogConcaveSampling.MetropolisBalance.densityLaw line 320
  25. lemma OAI.LogConcaveSampling.MetropolisBalance.densityLaw_integral line 324
  26. lemma OAI.LogConcaveSampling.MetropolisBalance.densityLaw_integrable line 332
  27. theorem OAI.LogConcaveSampling.MetropolisBalance.probability_one_step_defect line 340
  28. def OAI.LogConcaveSampling.EulerDefect.joint line 365
  29. def OAI.LogConcaveSampling.EulerDefect.jointCoefficient line 368
  30. lemma OAI.LogConcaveSampling.EulerDefect.joint_density line 371
  31. lemma OAI.LogConcaveSampling.EulerDefect.measurable_joint_map line 389
  32. lemma OAI.LogConcaveSampling.EulerDefect.jointCoefficient_ne_zero line 395
  33. lemma OAI.LogConcaveSampling.EulerDefect.jointCoefficient_ne_top line 401
  34. lemma OAI.LogConcaveSampling.EulerDefect.scaled_log_ratio_integrable line 405
  35. def OAI.LogConcaveSampling.EulerDefect.rate line 437
  36. lemma OAI.LogConcaveSampling.EulerDefect.rate_nonneg line 443
  37. lemma OAI.LogConcaveSampling.EulerDefect.rate_tendsto line 446
  38. lemma OAI.LogConcaveSampling.EulerDefect.joint_log_ratio_integrable line 452
  39. lemma OAI.LogConcaveSampling.EulerDefect.joint_log_ratio_integral line 471
  40. theorem OAI.LogConcaveSampling.EulerDefect.one_step_gibbs_defect line 486