production module

`AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.LogSobolev`

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

Imports

AutoSamplingTheory.Probability

Imported by

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalitiesAutoSamplingTheory.TechnicalLemmas.RegistryAutoSamplingTheory.TechnicalLemmas.Variational

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/LogSobolev.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.Probability

/-!
# Log-Sobolev / Fisher-information bookkeeping lemmas

Compiled algebraic and integral handoff lemmas for the LSI-to-KL/FI route.
Large analytic log-Sobolev theorems are still port targets; this file records
the locally proved reusable bookkeeping layer.
-/

namespace AutoSamplingTheory
namespace TechnicalLemmas
namespace FunctionalInequalities
namespace LogSobolev

export AutoSamplingTheory (
  lsiKlFiSqrtDensitySquareScalar
  lsiKlFiSqrtDensityEntropyIntegrandScalar
  lsiKlFiSqrtDensityNormalizationScalar
  lsiKlFiRnDerivLIntegralMassOne
  lsiKlFiRnDerivDensityMassOne
  lsiKlFiSqrtRnDerivTestMassOne
  lsiKlFiRnDerivEntropyIntegral
  lsiKlFiSqrtRnDerivEntropyIntegral
  lsiKlFiSqrtDensityFisherChainScalar
  lsiKlFiSqrtDensityFisherChainOfDerivativesScalar
  lsiKlFiSqrtDensityFisherChainFiniteSumScalar
  lsiKlFiSqrtDensityFisherChainFiniteSumHandoffScalar
  lsiKlFiSqrtDensityFisherChainIntegralFiniteSum
  lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar
)

end LogSobolev
end FunctionalInequalities
end TechnicalLemmas
end AutoSamplingTheory