ASTIS mathematical exposition

Construct a source-cited DV proof-obligation record

AutoSamplingTheory.dvVariationalObligation · def · Teaching coverage

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}.\]

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 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.

def dvVariationalObligation (source : SourceAnchor) : ProofObligation

Exact module and namespace context

Lean construction · dvVariationalObligation

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

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."

/-- Precise source-cited DV interface matching `appendix.tex:73-79`.

Downstream proof obligations may depend on this interface only as a cited
analytic result until an actual Lean proof or imported theorem replaces it.
-/

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.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the ASTIS 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.

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