AutoSamplingTheory.SALD.saldLsiKlFiBridgeContract

Data definition / provenance and workflow record

Meaning and type

The result has data type AutoSamplingTheory.SALD.LsiKlFiBridgeContract. A value of this type stores descriptions; it is not a proof of the statements in those descriptions.

def saldLsiKlFiBridgeContract : LsiKlFiBridgeContract

Construction and field-by-field explanation

Construct a data record from explicit fields and the audited defaults shown below.

This Lean definition constructs provenance or workflow data. It does not prove the mathematical statements stored as text. Status labels, named dependencies and citations are data, not compilation, proof or source certificates.

sourceBlock : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldKlFiLsiSource — audited data reference, not expanded and not a compiled dependency edge

absoluteContinuityInterface : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

rho << pi; write r=d rho/d pi, with r >= 0 pi-a.e. and integral r d pi = 1.

densityRatioInterface : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

The paper's rho/pi ratio is represented by r; KL(rho||pi)=integral log(r) r d pi and FI(rho||pi)=integral ||nabla log r||^2 r d pi when finite.

testFunctionInterface : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

Use phi=sqrt(r) as the LSI test function; Lean must either require phi is smooth/admissible or supply an approximation/closure lemma.

normalizationStep : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

integral phi^2 d pi = integral r d pi = 1, matching the LSI normalization hypothesis.

entropyIdentity : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

integral phi^2 log(phi^2) d pi = KL(rho||pi).

fisherChainRule : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

integral ||nabla phi||^2 d pi = (1/4)*FI(rho||pi), so the source LSI display gives KL(rho||pi) <= FI(rho||pi)/(2*C_LSI).

finiteQuantityInterfaces : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. finite KL(rho||pi)
2. finite FI(rho||pi)
3. measurable nonnegative density ratio r
4. integrability of log(r)*r and ||nabla log r||^2*r

sourceGaps : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. main_body.tex states the substitution phi=sqrt(rho/pi) but does not spell out density smoothness or approximation hypotheses
2. the source assumes the Fisher-information chain rule needed for the constant 1/(2*C_LSI)

dependencies : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. KLContract
2. FIContract
3. LSIContract
4. probability.lsi_to_kl_fi

status : AutoSamplingTheory.ProofStatus (explicit)

Stored workflow tag; honor the exact default but do not infer mathematical certification.

AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification

def saldLsiKlFiBridgeContract : LsiKlFiBridgeContract where
  sourceBlock := saldKlFiLsiSource
  absoluteContinuityInterface := "rho << pi; write r=d rho/d pi, with r >= 0 pi-a.e. and integral r d pi = 1."
  densityRatioInterface := "The paper's rho/pi ratio is represented by r; KL(rho||pi)=integral log(r) r d pi and FI(rho||pi)=integral ||nabla log r||^2 r d pi when finite."
  testFunctionInterface := "Use phi=sqrt(r) as the LSI test function; Lean must either require phi is smooth/admissible or supply an approximation/closure lemma."
  normalizationStep := "integral phi^2 d pi = integral r d pi = 1, matching the LSI normalization hypothesis."
  entropyIdentity := "integral phi^2 log(phi^2) d pi = KL(rho||pi)."
  fisherChainRule := "integral ||nabla phi||^2 d pi = (1/4)*FI(rho||pi), so the source LSI display gives KL(rho||pi) <= FI(rho||pi)/(2*C_LSI)."
  finiteQuantityInterfaces := [
    "finite KL(rho||pi)",
    "finite FI(rho||pi)",
    "measurable nonnegative density ratio r",
    "integrability of log(r)*r and ||nabla log r||^2*r"
  ]
  sourceGaps := [
    "main_body.tex states the substitution phi=sqrt(rho/pi) but does not spell out density smoothness or approximation hypotheses",
    "the source assumes the Fisher-information chain rule needed for the constant 1/(2*C_LSI)"
  ]
  dependencies := ["KLContract", "FIContract", "LSIContract", "probability.lsi_to_kl_fi"]
  status := ProofStatus.obligation