OAI/Probability/LogConcave/Sampling/NormalizedScoreMajorant.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.LogConcaveSampling.normalizedTensorMajorant_order_budgetline 13 - def
OAI.LogConcaveSampling.normalizedScoreMajorantline 31 - lemma
OAI.LogConcaveSampling.normalizedScoreMajorant_nonnegline 34 - lemma
OAI.LogConcaveSampling.normalizedScoreMajorant_budgetline 38 - def
OAI.LogConcaveSampling.physicalTameScoreline 57