OAI/Probability/LogConcave/Sampling/LogMeshCountRate.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.LogConcaveSampling.logMeshCount_rateline 12 - lemma
OAI.LogConcaveSampling.probabilityNode_card_rateline 24 - theorem
OAI.LogConcaveSampling.meanWork_rateline 31 - lemma
OAI.LogConcaveSampling.sampleWork_rateline 43 - lemma
OAI.LogConcaveSampling.routineBudget_rateline 57 - lemma
OAI.LogConcaveSampling.sampleCorrelation_antitoneline 76 - lemma
OAI.LogConcaveSampling.logMeshCount_monoline 83 - lemma
OAI.LogConcaveSampling.sampleCorrelation_radius_lowerline 91 - lemma
OAI.LogConcaveSampling.logMeshLength_sample_rateline 101