OAI/Probability/LogConcave/JetEstimates/CompLinear.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.LogConcaveSampling.Appell.HasGrowth.comp_linearline 12 - lemma
OAI.LogConcaveSampling.PolySmooth.comp_linearline 24 - lemma
OAI.LogConcaveSampling.productPotential_polySmoothline 34 - lemma
OAI.LogConcaveSampling.gaussianPotential_polySmoothline 41 - lemma
OAI.LogConcaveSampling.productPotential_lowerTailline 53 - lemma
OAI.LogConcaveSampling.gaussianPotential_lowerTailline 67