Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

Exact source context

import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator

namespace AutoSamplingTheory.Tests.GeneratorFunctionalInequalities

#check AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator.dirichletForm
#check AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator.SatisfiesPoincare
#check AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator.SatisfiesLogSobolev

end AutoSamplingTheory.Tests.GeneratorFunctionalInequalities