ASTIS mathematical exposition

Record the remaining LSI-to-KL/Fisher proof target

AutoSamplingTheory.lsiToKlFiObligation · def · Teaching coverage

Statement

Given any source anchor, construct the proof-obligation record named probability.lsi_to_kl_fi with the text that an LSI constant c_LSI should imply KL(ρ‖π)≤FI(ρ‖π)/(2c_LSI). The record has obligation status. It does not prove the inequality or supply its missing analytic hypotheses.

\[\text{recorded target: }\mathrm{KL}(\rho\|\pi)\le\frac{\mathrm{FI}(\rho\|\pi)}{2c_{\mathrm{LSI}}},\qquad\operatorname{status}=\texttt{obligation}.\]

All objects and hypotheses

source:SourceAnchor is the sole input. No positive constant, measures, LSI witness, density regularity or admissible-test proof is passed.
The returned ProofObligation uses its default empty dependency list and empty note.

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. Write the requested target and provenance

Populate the fixed id, written inequality, supplied source and explicit obligation label.

\[\text{source}\mapsto(\texttt{probability.lsi\_to\_kl\_fi},\text{target text},\text{source},\texttt{obligation}).\]

Corresponding Lean step

record fields id, statement, source, status

2. Interpret the result only as a workflow object

The constructor returns data that can track unfinished work. It provides no witness of the stored functional inequality.

\[\texttt{ProofObligation}\not\Rightarrow\mathrm{KL}\le\mathrm{FI}/(2c_{\mathrm{LSI}}).\]

Corresponding Lean step

return type ProofObligation

Lean statement · lsiToKlFiObligation

The displayed inequality occurs inside a string field. The return type is a record for unproved work, not the inequality proposition.

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 lsiToKlFiObligation (source : SourceAnchor) : ProofObligation

Exact module and namespace context

Lean construction · lsiToKlFiObligation

No proof tactics or analytic theorem are used. The function constructs the stated data record with an obligation status.

def lsiToKlFiObligation (source : SourceAnchor) : ProofObligation where
  id := "probability.lsi_to_kl_fi"
  statement := "If pi satisfies LSI with constant c_LSI, then KL(rho || pi) <= FI(rho || pi)/(2*c_LSI)."
  source := source
  status := ProofStatus.obligation

end AutoSamplingTheory

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 LSI-to-KL/FI conclusion may be inferred from compiling or displaying this record.

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