AutoSamplingTheory.SALD.continuousForwardKlStatementContract

Data definition / provenance and workflow record

Meaning and type

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

def continuousForwardKlStatementContract : ForwardKlStatementContract

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.

theoremLabel : String (explicit)

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

thm:forward-KL

sourceStatement : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

sourceProof : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

movingTarget : String (explicit)

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

pi_t on t in [0,T], with transport velocity field v_t generating pi through the continuity equation.

saldLaw : String (explicit)

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

rho_s is the probability law of SALD eq:SALD for s in [0,S], with inverse time schedule s=s(t).

lsiAssumption : String (explicit)

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

For every t in [0,T], pi_t satisfies LSI with constant C_LSI(t) >= 0; C_LSI(t)=0 is allowed when no positive LSI is available.

alphaComplexityAssumption : String (explicit)

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

There exists alpha0 > 0 such that E_{alpha0}(pi_t,v_t) < +infty for every t in [0,T].

alphaRange : String (explicit)

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

For any alpha in (0, alpha0].

initialErrorFactor : String (explicit)

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

exp (-(int_0^T dot{s}(t) C_LSI(t) dt)) * exp (int_0^T (1/2) dot{s}(t)^(-1) alpha^(-1) dt) * KL(rho_0 || pi_0).

residualIntegral : String (explicit)

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

int_0^T exp (int_t^T (1/2) dot{s}(u)^(-1) alpha^(-1) du) * (1/2) dot{s}(t)^(-1) * E_alpha(pi_t,v_t) dt.

proofQuantity : String (explicit)

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

K(t) := KL(rho_{s(t)} || pi_t) = KL(rho_{s(t)} || tilde_pi_{s(t)}).

differentialInequality : String (explicit)

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

dK/dt <= -(dot{s}(t) C_LSI(t) - (1/2) dot{s}(t)^(-1) alpha^(-1)) * K(t) + (1/2) dot{s}(t)^(-1) * E_alpha(pi_t,v_t).

proofSteps : List String (explicit)

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

Ordered data items

1. appendix.tex:166-189 differentiates KL(rho_s || tilde_pi_s) and substitutes the SALD Fokker-Planck equation.
2. appendix.tex:190-225 changes from s to t and applies LSI to the Fisher information term.
3. appendix.tex:229-241 applies Donsker--Varadhan to bound ||v_t||_{L2(rho_{s(t)})}^2 by alpha^{-1}K(t)+E_alpha(pi_t,v_t).
4. appendix.tex:242-252 applies lem:gronwall with the exact exponent signs, then separates the LSI and alpha-complexity exponent terms.

dependencies : List String (explicit)

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

Ordered data items

1. eq:LSI-KL-FI
2. def:alpha-complexity
3. lem:dv_variation
4. lem:gronwall
5. sald.forward_kl.moving_target_dependency_chain
6. sald.forward_kl.gronwall_side_conditions
7. sald.forward_kl.kl_derivative
8. sald.forward_kl.dv_energy_bound
9. sald.forward_kl.gronwall_application

status : AutoSamplingTheory.ProofStatus (explicit)

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

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

def continuousForwardKlStatementContract : ForwardKlStatementContract where
  theoremLabel := "thm:forward-KL"
  sourceStatement := saldForwardKlSource
  sourceProof := saldForwardKlProofSource
  movingTarget := "pi_t on t in [0,T], with transport velocity field v_t generating pi through the continuity equation."
  saldLaw := "rho_s is the probability law of SALD eq:SALD for s in [0,S], with inverse time schedule s=s(t)."
  lsiAssumption := "For every t in [0,T], pi_t satisfies LSI with constant C_LSI(t) >= 0; C_LSI(t)=0 is allowed when no positive LSI is available."
  alphaComplexityAssumption := "There exists alpha0 > 0 such that E_{alpha0}(pi_t,v_t) < +infty for every t in [0,T]."
  alphaRange := "For any alpha in (0, alpha0]."
  initialErrorFactor := "exp (-(int_0^T dot{s}(t) C_LSI(t) dt)) * exp (int_0^T (1/2) dot{s}(t)^(-1) alpha^(-1) dt) * KL(rho_0 || pi_0)."
  residualIntegral := "int_0^T exp (int_t^T (1/2) dot{s}(u)^(-1) alpha^(-1) du) * (1/2) dot{s}(t)^(-1) * E_alpha(pi_t,v_t) dt."
  proofQuantity := "K(t) := KL(rho_{s(t)} || pi_t) = KL(rho_{s(t)} || tilde_pi_{s(t)})."
  differentialInequality := "dK/dt <= -(dot{s}(t) C_LSI(t) - (1/2) dot{s}(t)^(-1) alpha^(-1)) * K(t) + (1/2) dot{s}(t)^(-1) * E_alpha(pi_t,v_t)."
  proofSteps := [
    "appendix.tex:166-189 differentiates KL(rho_s || tilde_pi_s) and substitutes the SALD Fokker-Planck equation.",
    "appendix.tex:190-225 changes from s to t and applies LSI to the Fisher information term.",
    "appendix.tex:229-241 applies Donsker--Varadhan to bound ||v_t||_{L2(rho_{s(t)})}^2 by alpha^{-1}K(t)+E_alpha(pi_t,v_t).",
    "appendix.tex:242-252 applies lem:gronwall with the exact exponent signs, then separates the LSI and alpha-complexity exponent terms."
  ]
  dependencies := [
    "eq:LSI-KL-FI",
    "def:alpha-complexity",
    "lem:dv_variation",
    "lem:gronwall",
    "sald.forward_kl.moving_target_dependency_chain",
    "sald.forward_kl.gronwall_side_conditions",
    "sald.forward_kl.kl_derivative",
    "sald.forward_kl.dv_energy_bound",
    "sald.forward_kl.gronwall_application"
  ]
  status := ProofStatus.contractOnly