AutoSamplingTheory.SALD.saldLsiKlFiDensityTestContract

Data definition / provenance and workflow record

Meaning and type

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

def saldLsiKlFiDensityTestContract : LsiKlFiDensityTestContract

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

densityObject : String (explicit)

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

r = rho/pi is the Radon-Nikodym density d rho / d pi for rho << pi.

absoluteContinuity : String (explicit)

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

rho << pi is required before the paper's ratio rho/pi, KL integral, and FI integral are meaningful.

normalization : String (explicit)

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

integral r d pi = 1, hence phi=sqrt(r) satisfies integral phi^2 d pi = 1; cycle 43 formalizes this for Mathlib Radon-Nikodym densities via AutoSamplingTheory.lsiKlFiRnDerivDensityMassOne and AutoSamplingTheory.lsiKlFiSqrtRnDerivTestMassOne.

positivityDomain : String (explicit)

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

r >= 0 pi-a.e.; any log(r) and nabla log(r) interface must handle the zero-density set or work under a positive smooth approximation.

finiteKlInterface : String (explicit)

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

finite integral log(r) * r d pi is needed to identify the entropy side with KL(rho||pi).

finiteFiInterface : String (explicit)

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

finite integral ||nabla log r||^2 * r d pi is needed before the Fisher-information chain rule can be used.

sqrtTestFunction : String (explicit)

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

phi = sqrt(r), exactly as stated after the LSI definition in main_body.tex.

testAdmissibility : String (explicit)

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

phi must be an admissible smooth LSI test function, or the proof must pass through an approximation/closure theorem.

entropyRewrite : 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 = integral r * log(r) d pi = KL(rho||pi); cycle 43 formalizes the Mathlib log-likelihood transport step through AutoSamplingTheory.lsiKlFiRnDerivEntropyIntegral and AutoSamplingTheory.lsiKlFiSqrtRnDerivEntropyIntegral.

fisherChainRule : String (explicit)

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

nabla sqrt(r) = (1/2) sqrt(r) * nabla log(r), giving integral ||nabla phi||^2 d pi = (1/4) FI(rho||pi); cycle 43 lower formalizes the finite-coordinate a.e. integral handoff once coordinate derivative identities are supplied.

coefficientAudit : String (explicit)

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

Combining the source LSI factor 2/C_LSI with the 1/4 Fisher chain-rule factor gives FI(rho||pi)/(2*C_LSI), matching eq:LSI-KL-FI; SALD.lsiKlFiCoefficientAuditScalar formalizes the coefficient algebra, SALD.lsiKlFiDensityTestBridgeScalar formalizes the normalized-test scalar handoff after the analytic inputs are supplied, cycle 38 adds the pointwise positive-density scalar Fisher coefficient plus the downstream half-Fisher coefficient bridge, and cycle 43 adds Mathlib-backed density normalization, entropy transport, and a finite-coordinate integral Fisher-chain handoff for the sqrt Radon-Nikodym test.

approximationFallback : String (explicit)

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

If sqrt(r) is not smooth or positive, record a closure/approximation lemma as a separate obligation rather than adding hidden assumptions to forward-KL theorems.

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. AutoSamplingTheory.lsiKlFiRnDerivLIntegralMassOne
5. AutoSamplingTheory.lsiKlFiRnDerivDensityMassOne
6. AutoSamplingTheory.lsiKlFiSqrtRnDerivTestMassOne
7. AutoSamplingTheory.lsiKlFiRnDerivEntropyIntegral
8. AutoSamplingTheory.lsiKlFiSqrtRnDerivEntropyIntegral
9. AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainScalar
10. AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainOfDerivativesScalar
11. AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainIntegralFiniteSum
12. AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar
13. SALD.lsiKlFiCoefficientAuditScalar
14. SALD.lsiKlFiDensityTestBridgeScalar
15. SALD.lsiKlFiHalfFisherScalar
16. SALD.lsiKlFiDensityTestHalfFisherScalar
17. probability.lsi_to_kl_fi

sourceGaps : List String (explicit)

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

Ordered data items

1. main_body.tex:208 states rho << pi but not the Radon-Nikodym backend or zero-density convention
2. main_body.tex:208-215 does not state smoothness/admissibility hypotheses for sqrt(rho/pi)
3. the Fisher-information chain rule and approximation/closure argument are used but not proved in the source

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 saldLsiKlFiDensityTestContract : LsiKlFiDensityTestContract where
  sourceBlock := saldKlFiLsiSource
  densityObject := "r = rho/pi is the Radon-Nikodym density d rho / d pi for rho << pi."
  absoluteContinuity := "rho << pi is required before the paper's ratio rho/pi, KL integral, and FI integral are meaningful."
  normalization := "integral r d pi = 1, hence phi=sqrt(r) satisfies integral phi^2 d pi = 1; cycle 43 formalizes this for Mathlib Radon-Nikodym densities via AutoSamplingTheory.lsiKlFiRnDerivDensityMassOne and AutoSamplingTheory.lsiKlFiSqrtRnDerivTestMassOne."
  positivityDomain := "r >= 0 pi-a.e.; any log(r) and nabla log(r) interface must handle the zero-density set or work under a positive smooth approximation."
  finiteKlInterface := "finite integral log(r) * r d pi is needed to identify the entropy side with KL(rho||pi)."
  finiteFiInterface := "finite integral ||nabla log r||^2 * r d pi is needed before the Fisher-information chain rule can be used."
  sqrtTestFunction := "phi = sqrt(r), exactly as stated after the LSI definition in main_body.tex."
  testAdmissibility := "phi must be an admissible smooth LSI test function, or the proof must pass through an approximation/closure theorem."
  entropyRewrite := "integral phi^2 * log(phi^2) d pi = integral r * log(r) d pi = KL(rho||pi); cycle 43 formalizes the Mathlib log-likelihood transport step through AutoSamplingTheory.lsiKlFiRnDerivEntropyIntegral and AutoSamplingTheory.lsiKlFiSqrtRnDerivEntropyIntegral."
  fisherChainRule := "nabla sqrt(r) = (1/2) sqrt(r) * nabla log(r), giving integral ||nabla phi||^2 d pi = (1/4) FI(rho||pi); cycle 43 lower formalizes the finite-coordinate a.e. integral handoff once coordinate derivative identities are supplied."
  coefficientAudit := "Combining the source LSI factor 2/C_LSI with the 1/4 Fisher chain-rule factor gives FI(rho||pi)/(2*C_LSI), matching eq:LSI-KL-FI; SALD.lsiKlFiCoefficientAuditScalar formalizes the coefficient algebra, SALD.lsiKlFiDensityTestBridgeScalar formalizes the normalized-test scalar handoff after the analytic inputs are supplied, cycle 38 adds the pointwise positive-density scalar Fisher coefficient plus the downstream half-Fisher coefficient bridge, and cycle 43 adds Mathlib-backed density normalization, entropy transport, and a finite-coordinate integral Fisher-chain handoff for the sqrt Radon-Nikodym test."
  approximationFallback := "If sqrt(r) is not smooth or positive, record a closure/approximation lemma as a separate obligation rather than adding hidden assumptions to forward-KL theorems."
  dependencies := [
    "KLContract",
    "FIContract",
    "LSIContract",
    "AutoSamplingTheory.lsiKlFiRnDerivLIntegralMassOne",
    "AutoSamplingTheory.lsiKlFiRnDerivDensityMassOne",
    "AutoSamplingTheory.lsiKlFiSqrtRnDerivTestMassOne",
    "AutoSamplingTheory.lsiKlFiRnDerivEntropyIntegral",
    "AutoSamplingTheory.lsiKlFiSqrtRnDerivEntropyIntegral",
    "AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainScalar",
    "AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainOfDerivativesScalar",
    "AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainIntegralFiniteSum",
    "AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar",
    "SALD.lsiKlFiCoefficientAuditScalar",
    "SALD.lsiKlFiDensityTestBridgeScalar",
    "SALD.lsiKlFiHalfFisherScalar",
    "SALD.lsiKlFiDensityTestHalfFisherScalar",
    "probability.lsi_to_kl_fi"
  ]
  sourceGaps := [
    "main_body.tex:208 states rho << pi but not the Radon-Nikodym backend or zero-density convention",
    "main_body.tex:208-215 does not state smoothness/admissibility hypotheses for sqrt(rho/pi)",
    "the Fisher-information chain rule and approximation/closure argument are used but not proved in the source"
  ]
  status := ProofStatus.obligation