OAI/Probability/LogConcave/Analysis/GaussianProposalPotential.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.gaussianProposalPotential line 22
2. lemma OAI.LogConcaveSampling.gaussianProposalPotential_eq line 24
3. lemma OAI.LogConcaveSampling.gaussianProposalPotential_hasGradientAt line 28
4. lemma OAI.LogConcaveSampling.gaussianProposalPotential_gradient line 41
5. lemma OAI.LogConcaveSampling.gaussianProposalPotential_admissible line 45
6. lemma OAI.LogConcaveSampling.partition_comparison line 57
7. def OAI.LogConcaveSampling.gaussianAcceptance line 86
8. lemma OAI.LogConcaveSampling.gaussianAcceptance_bounds line 89
9. lemma OAI.LogConcaveSampling.measurable_gaussianAcceptance line 96
10. lemma OAI.LogConcaveSampling.gaussian_accepted_measure line 101