OAI/Probability/LogConcave/Sampling/UnitUniform.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.measurable_fin_snoc line 19
  2. lemma OAI.LogConcaveSampling.pi_snoc_law line 28
  3. def OAI.LogConcaveSampling.unitUniform line 44
  4. instance OAI.LogConcaveSampling.(instance at line 46) line 46
  5. lemma OAI.LogConcaveSampling.unitUniform_Iic line 50
  6. def OAI.LogConcaveSampling.acceptanceEvent line 63
  7. lemma OAI.LogConcaveSampling.measurable_acceptanceEvent line 65
  8. theorem OAI.LogConcaveSampling.accepted_measure line 68
  9. def OAI.LogConcaveSampling.rejectionPick line 92
  10. lemma OAI.LogConcaveSampling.measurable_rejectionPick line 98
  11. lemma OAI.LogConcaveSampling.rejectionPick_snoc line 110
  12. theorem OAI.LogConcaveSampling.rejection_law_succ line 115
  13. lemma OAI.LogConcaveSampling.rejection_failure_mass line 142
  14. theorem OAI.LogConcaveSampling.capped_rejection_tv line 154