Samplinglib mathematical lesson

Construct a source-cited DV proof-obligation record

AutoSamplingTheory.dvVariationalObligation · def · Teaching coverage

Read this first

Mathematical statement

Given any source anchor, construct a ProofObligation with id probability.dv_variational_formula, the written KL variational-supremum statement, that source, sourceCited status, and a note that the result must be ported or kept as a cited analytic dependency. This creates metadata, not a proof of entropy duality.

\[\operatorname{id}=\texttt{probability.dv\_variational\_formula},\qquad \operatorname{status}=\texttt{sourceCited}.\]

Lean statement · dvVariationalObligation

The function accepts a provenance record and returns a workflow record, not an inequality or an equality of analytic quantities.

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)

def dvVariationalObligation (source : SourceAnchor) : ProofObligation

Exact module and namespace context

Proof roadmap

1Populate the obligation fields
Store the fixed id and variational statement alongside the caller's source anchor.
2Keep its unproved status explicit
Set sourceCited and attach the port-or-cite note. No term of a variational-identity proposition is returned.

Full assumptions and notation

All objects and hypotheses

source is any Core SourceAnchor; it is the sole function parameter.
The stored text describes KL(ν‖μ)=sup_Z{EνZ−log Eμexp Z} under the paper's integrability assumptions; those assumptions are text, not formal parameters.
ProofObligation's omitted dependsOn list is empty by default; the supplied note is descriptive.

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. Populate the obligation fields

Store the fixed id and variational statement alongside the caller's source anchor.

\[\text{source}\longmapsto(\text{id},\text{statement},\text{source}).\]

Corresponding Lean step

id, statement, source fields

2. Keep its unproved status explicit

Set sourceCited and attach the port-or-cite note. No term of a variational-identity proposition is returned.

\[\text{result type}=\texttt{ProofObligation}\ne\text{proof of KL duality}.\]

Corresponding Lean step

status := ProofStatus.sourceCited; note field

Lean verification

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

Lean construction · dvVariationalObligation

The body initializes named data fields. The word sourceCited preserves the intended cited-dependency status and supplies no proof certificate.

Download module (.lean)

def dvVariationalObligation (source : SourceAnchor) : ProofObligation where
  id := "probability.dv_variational_formula"
  statement := "KL(nu || mu) = sup_Z { E_nu[Z] - log E_mu[exp Z] } under the paper's integrability assumptions."
  source := source
  status := ProofStatus.sourceCited
  note := "Port from Mathlib/SLT or keep as cited analytic dependency until formalized."

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 Boucheron supremum equality has been proved by this constructor. The passed anchor is not validated here.

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.ProofObligation — Core workflow metadata type, not an analytic theorem.
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.