OAI/Probability/LogConcave/Sampling/AdjointCoordinateProductLeft.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.LogConcaveSampling.adjointCoordinate_product_leftline 13 - lemma
OAI.LogConcaveSampling.adjointCoordinate_product_rightline 29 - lemma
OAI.LogConcaveSampling.jointSkewEntry_LLline 47 - lemma
OAI.LogConcaveSampling.jointSkewEntry_RRline 50 - lemma
OAI.LogConcaveSampling.jointSkewEntry_LRline 53 - lemma
OAI.LogConcaveSampling.jointSkewEntry_RLline 58