OAI/Probability/LogConcave/Analysis/CompactGibbsIbp.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.compact_gibbs_ibp line 14
2. lemma OAI.LogConcaveSampling.adjointCoordinate_compact_pairing line 41
3. lemma OAI.LogConcaveSampling.tensorAdjoint_compact_pairing line 64
4. lemma OAI.LogConcaveSampling.standardGaussian_eq_gibbs line 96
5. lemma OAI.LogConcaveSampling.compact_gaussian_ibp line 111