Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
production module

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities

0 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities.lean.

Imports
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GeneratorAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.LogSobolevAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.PoincareAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecayAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedBochnerAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradientAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradientWeakAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradientDistributionAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedResolventAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedLocalL2AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ClosedGraphResolvent
Imported by
AutoSamplingTheory.TechnicalLemmas
Placeholder scan
0 declaration(s) flagged
Gate status
Partial

Declarations

This aggregator contains no named declarations.