ASTIS mathematical exposition

Populate the paper-facing DV interface without claiming its proof

AutoSamplingTheory.dvVariationalFormulaInterface · def · Teaching coverage

Statement

Given a source anchor, populate the DvVariationalFormulaInterface with the existing paper-facing textual description: common probability measures, KL with source-specific side conditions, measurable real tests with finite log-mgf, the variational supremum expression, its one-sided consequence, descriptions of available scalar/tilting bridges, the Boucheron–Lugosi–Massart Corollary 4.15 citation, and sourceCited status. These are stored descriptions only.

\[\text{recorded target: }\mathrm{KL}(\nu\|\mu)=\sup_Z\left\{\mathbb E_\nu Z-\log\mathbb E_\mu e^Z\right\};\qquad \text{record status: sourceCited}.\]

All objects and hypotheses

source:SourceAnchor is the only parameter; no measures, test functions, absolute-continuity proofs or admissibility witnesses are passed.
All twelve data fields of DvVariationalFormulaInterface are populated. The reference to SALD appendix.tex:73–79 is an existing source comment, not a new independent reading or source-fidelity verdict.

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. Record the intended domain and functionals

Write the measure assumptions, real measurable test class, finite-log-mgf predicate and two functional expressions into their textual slots.

\[\text{recorded }V(Z)=\mathbb E_\nu Z-\log\mathbb E_\mu e^Z.\]

Corresponding Lean step

probabilityMeasures through variationalFunctional fields

2. Record target and bridge descriptions separately

The supremum identity remains source-cited. The one-sided consequence and names of existing scalar and tilted-backend bridges describe available narrower results, without converting the supremum identity into a proved theorem.

\[V(Z)\le\mathrm{KL}\Longrightarrow\mathbb E_\nu Z\le\mathrm{KL}+\log\mathbb E_\mu e^Z\quad\text{(recorded bridge shape)}.\]

Corresponding Lean step

supremumStatement, oneSidedConsequence, oneSidedScalarBridge

3. Attach provenance and the retained status

Store the caller's source, fixed citation text and sourceCited label.

\[\operatorname{status}=\texttt{sourceCited},\quad\operatorname{source}=\text{supplied anchor}.\]

Corresponding Lean step

source, citation, status fields

Lean statement · dvVariationalFormulaInterface

This lower-case function returns the upper-case interface record. None of its textual analytic clauses is a theorem hypothesis or conclusion.

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 dvVariationalFormulaInterface (source : SourceAnchor) :
    DvVariationalFormulaInterface

Exact module and namespace context

Lean construction · dvVariationalFormulaInterface

The body is a record literal containing descriptions and citations. Existing theorem names appear inside a string, so they are documentary references rather than Lean proof dependencies.

def dvVariationalFormulaInterface (source : SourceAnchor) :
    DvVariationalFormulaInterface where
  source := source
  probabilityMeasures := "mu and nu are probability distributions on the same measurable space."
  klFunctional := "KL(nu || mu), with the paper's absolute-continuity and finite-entropy side conditions supplied by each theorem block."
  testFunctionClass := "real-valued measurable random variables Z on the common space."
  finiteLogMgfPredicate := "log E_mu[exp(Z)] < +infty."
  logMgfFunctional := "Z |-> log E_mu[exp(Z)]."
  variationalFunctional := "Z |-> E_nu[Z] - log E_mu[exp(Z)]."
  supremumStatement := "KL(nu || mu) = sup_Z { E_nu[Z] - log E_mu[exp(Z)] }, where the supremum is over finite-log-mgf tests."
  oneSidedConsequence := "For every admissible Z, E_nu[Z] <= KL(nu || mu) + log E_mu[exp(Z)]."
  oneSidedScalarBridge := "AutoSamplingTheory.dvVariationalOneSidedConsequenceScalar proves the real-order rearrangement from E_nu[Z] - logMgf <= KL to E_nu[Z] <= KL + logMgf; AutoSamplingTheory.dvVariationalOneSidedFromSupremumScalar additionally proves the scalar step from admissible-test membership plus the source supremum identity to that one-sided bound; AutoSamplingTheory.dvVariationalTiltedRightOneSidedConsequence combines the Mathlib tilted backend with the scalar rearrangement under explicit selected-test hypotheses."
  citation := "Boucheron, Lugosi, and Massart, Concentration Inequalities, Corollary 4.15, cited by SALD appendix.tex:73."
  status := ProofStatus.sourceCited

/-- Pointwise square identity for the LSI density test `phi = sqrt(r)`.

In the SALD source step `main_body.tex:208-215`, this is the local scalar
part of replacing `phi^2` by the Radon-Nikodym density ratio `r = rho/pi`.
The measure-theoretic density and integral transport remain separate
obligations.
-/

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.
Names embedded in oneSidedScalarBridge are not formal theorem dependencies.
Do not present the stored test class or finite-log-mgf clause as a proved sufficient hypothesis for the full supremum equality.

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.
Existing source comment and stored citation — Locally recorded SALD appendix.tex:73–79 / Boucheron–Lugosi–Massart Corollary 4.15 citation only; primary text not independently inspected.
AutoSamplingTheory.DvVariationalFormulaInterface — Existing root ASTIS dependency; use its own adjacent teaching unit.
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.