Samplinglib mathematical lesson

Record the cited entropy-duality interface

AutoSamplingTheory.DvVariationalFormulaInterface · structure · Teaching coverage

Read this first

Mathematical statement

This record packages text describing the Donsker–Varadhan variational formula, its intended hypotheses, selected tests, scalar bridges and citation. Status defaults to sourceCited. Every analytic slot is text, not a Lean hypothesis or proved equality.

\[\operatorname{fields}(\texttt{DvVariationalFormulaInterface})=\{\texttt{source},\texttt{probabilityMeasures},\texttt{klFunctional},\texttt{testFunctionClass},\texttt{finiteLogMgfPredicate},\texttt{logMgfFunctional},\texttt{variationalFunctional},\texttt{supremumStatement},\texttt{oneSidedConsequence},\texttt{oneSidedScalarBridge},\texttt{citation},\texttt{status}\}.\]

Lean statement · DvVariationalFormulaInterface

This declaration introduces a record type. Its 12 fields are descriptions, provenance and a status label, not mathematical objects satisfying the written claim.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

structure DvVariationalFormulaInterface where
  source : SourceAnchor
  probabilityMeasures : String
  klFunctional : String
  testFunctionClass : String
  finiteLogMgfPredicate : String
  logMgfFunctional : String
  variationalFunctional : String
  supremumStatement : String
  oneSidedConsequence : String
  oneSidedScalarBridge : String
  citation : String
  status : ProofStatus := ProofStatus.sourceCited
deriving Repr, DecidableEq

Exact module and namespace context

Proof roadmap

1Specify the record's data slots
The structure declares exactly the listed fields and their data types. A source anchor is itself provenance data from Core, not a proof of the described statement.
2Provide defaults and routine data operations
Any listed defaults are filled when omitted. Derived representation and decidable equality let the program display and compare records; they compare data and do not decide analytic truth.

Full assumptions and notation

All objects and hypotheses

source has type SourceAnchor: provenance.
probabilityMeasures has type String: described measure assumptions.
klFunctional has type String: KL expression.
testFunctionClass has type String: described test class.
finiteLogMgfPredicate has type String: described admissibility predicate.
logMgfFunctional has type String: log moment-generating-functional description.
variationalFunctional has type String: variational-test value description.
supremumStatement has type String: written supremum identity.
oneSidedConsequence has type String: written test-wise consequence.
oneSidedScalarBridge has type String: description of available bridge declarations.
citation has type String: citation text.
status has type ProofStatus: default sourceCited.
No ambient measurable space, measure, analytic hypothesis or proof witness is a parameter of this metadata structure. Default fields may be overridden when constructing a record.

Notation and interpretation

Analytic values versus metadata: Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.
\[\texttt{ProofObligation}\ne\text{proof of its statement string}\]

Construction and meaning

1. Specify the record's data slots

The structure declares exactly the listed fields and their data types. A source anchor is itself provenance data from Core, not a proof of the described statement.

\[\text{descriptive fields}+\text{provenance}\longmapsto\text{one record}.\]

Corresponding Lean step

structure DvVariationalFormulaInterface where; listed fields

2. Provide defaults and routine data operations

Any listed defaults are filled when omitted. Derived representation and decidable equality let the program display and compare records; they compare data and do not decide analytic truth.

\[\operatorname{DecidableEq}(\text{records})\ne\text{decision procedure for the recorded mathematics}.\]

Corresponding Lean step

field defaults; deriving Repr, DecidableEq

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean construction · DvVariationalFormulaInterface

There is no theorem proof here. The body declares the fields and their defaults; derived display and equality support are ordinary operations on that data.

Download module (.lean)

structure DvVariationalFormulaInterface where
  source : SourceAnchor
  probabilityMeasures : String
  klFunctional : String
  testFunctionClass : String
  finiteLogMgfPredicate : String
  logMgfFunctional : String
  variationalFunctional : String
  supremumStatement : String
  oneSidedConsequence : String
  oneSidedScalarBridge : String
  citation : String
  status : ProofStatus := ProofStatus.sourceCited
deriving Repr, DecidableEq

Exact module and namespace context

Scope and omitted-condition boundaries

Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.
No admissibility predicate, supremum functional or theorem is enforced by this data schema; even sourceCited is a metadata label, not certification.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
AutoSamplingTheory.SourceAnchor — Core workflow metadata type, not an analytic theorem.
AutoSamplingTheory.ProofStatus — Core workflow metadata type, not an analytic theorem.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.