production module

`AutoSamplingTheory.TechnicalLemmas.InformationTheory.DonskerVaradhan`

0 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/InformationTheory/DonskerVaradhan.lean.

Imports

AutoSamplingTheory.Probability

Imported by

AutoSamplingTheory.TechnicalLemmas.InformationTheoryAutoSamplingTheory.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/InformationTheory/DonskerVaradhan.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.Probability

/-!
# Donsker--Varadhan technical lemmas

Small compiled one-sided consequences and scaled-test energy bounds around
the Donsker--Varadhan variational principle.

The full analytic DV theorem remains a cited-result/port target.  This module
contains only ASTIS-owned Lean declarations that already compile locally.
-/

namespace AutoSamplingTheory
namespace TechnicalLemmas
namespace InformationTheory
namespace DonskerVaradhan

export AutoSamplingTheory (
  dvVariationalOneSidedConsequenceScalar
  dvVariationalOneSidedFromSupremumScalar
  dvFiniteLogMgfOfLeAlpha
  dvVariationalOneSidedOfTiltedRight
  dvVariationalOneSidedOfScaledTest
  dvVariationalScaledTestEnergyBound
  dvVariationalScaledTestEnergyBoundWithCoeff
  dvVariationalTiltedRightOneSidedConsequence
)

end DonskerVaradhan
end InformationTheory
end TechnicalLemmas
end AutoSamplingTheory