AutoSamplingTheory.SALD.forwardKlDerivativeCandidateContract

Data definition / provenance and workflow record

Meaning and type

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

def forwardKlDerivativeCandidateContract : ForwardKlDerivativeCandidateContract

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.saldForwardKlDerivativeSource — audited data reference, not expanded and not a compiled dependency edge

densityAndLawInterface : String (explicit)

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

rho_s is Law(X_s) for SALD, tilde_pi_s = pi_{t(s)}, rho_s << tilde_pi_s, and KL/FI are finite along the proof interval.

scheduleInterface : String (explicit)

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

t=t(s) is smooth monotone increasing with inverse s=s(t), dot{s}(t)>0, and dot{t}(s(t)) = dot{s}(t)^(-1).

saldFokkerPlanck : String (explicit)

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

partial_s rho_s = div(rho_s * nabla log(rho_s / tilde_pi_s)), from eq:FP-eq.

targetVelocity : String (explicit)

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

v_t satisfies partial_t pi_t + div(v_t*pi_t)=0; tilde_v_s := dot{t}(s)*v_{t(s)} generates tilde_pi_s.

klDerivativeIdentity : String (explicit)

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

d/ds KL(rho_s || tilde_pi_s) = int partial_s rho_s * log(rho_s/tilde_pi_s) dx - int (rho_s/tilde_pi_s) * partial_s tilde_pi_s dx.

firstTermEvaluation : String (explicit)

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

The SALD Fokker--Planck equation and integration by parts give -FI(rho_s || tilde_pi_s).

secondTermBound : String (explicit)

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

The target-velocity term is bounded by sqrt(FI(rho_s||tilde_pi_s))*||tilde_v_s||_{L2(rho_s)} <= (1/2)*FI + (1/2)*||tilde_v_s||^2.

lsiStep : String (explicit)

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

Using LSI for pi_{t(s)}=tilde_pi_s gives FI(rho_s||tilde_pi_s) >= 2*C_LSI(t(s))*KL(rho_s||tilde_pi_s).

timeChangedInequality : String (explicit)

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

d/dt KL(rho_{s(t)} || pi_t) <= -dot{s}(t)*C_LSI(t)*KL(rho_{s(t)}||pi_t) + (1/2)*dot{s}(t)^(-1)*||v_t||_{L2(rho_{s(t)})}^2.

requiredRegularity : List String (explicit)

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

Ordered data items

1. differentiability in s and t of the density paths and KL quantity
2. smooth positive densities for rho_s, tilde_pi_s, and pi_t on the common state space
3. integration-by-parts hypotheses or boundary decay eliminating boundary terms
4. continuity/integrability of C_LSI(t), dot{s}(t), and the velocity L2 term

sourceGaps : List String (explicit)

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

Ordered data items

1. main_body.tex states the slowdown is smooth monotone but does not spell out the full inverse-function interface needed for dot{t}(s(t)) = dot{s}(t)^(-1)
2. appendix.tex uses differentiation under the integral and integration by parts without explicit dominated-convergence or boundary assumptions
3. the theorem statement does not explicitly state continuity of t -> C_LSI(t) or t -> E_alpha(pi_t,v_t), which Gronwall/integration later require

dependencies : List String (explicit)

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

Ordered data items

1. eq:SALD
2. eq:FP-eq
3. eq:LSI-KL-FI
4. TransportVelocityContract
5. KLContract
6. FIContract

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 forwardKlDerivativeCandidateContract : ForwardKlDerivativeCandidateContract where
  sourceBlock := saldForwardKlDerivativeSource
  densityAndLawInterface := "rho_s is Law(X_s) for SALD, tilde_pi_s = pi_{t(s)}, rho_s << tilde_pi_s, and KL/FI are finite along the proof interval."
  scheduleInterface := "t=t(s) is smooth monotone increasing with inverse s=s(t), dot{s}(t)>0, and dot{t}(s(t)) = dot{s}(t)^(-1)."
  saldFokkerPlanck := "partial_s rho_s = div(rho_s * nabla log(rho_s / tilde_pi_s)), from eq:FP-eq."
  targetVelocity := "v_t satisfies partial_t pi_t + div(v_t*pi_t)=0; tilde_v_s := dot{t}(s)*v_{t(s)} generates tilde_pi_s."
  klDerivativeIdentity := "d/ds KL(rho_s || tilde_pi_s) = int partial_s rho_s * log(rho_s/tilde_pi_s) dx - int (rho_s/tilde_pi_s) * partial_s tilde_pi_s dx."
  firstTermEvaluation := "The SALD Fokker--Planck equation and integration by parts give -FI(rho_s || tilde_pi_s)."
  secondTermBound := "The target-velocity term is bounded by sqrt(FI(rho_s||tilde_pi_s))*||tilde_v_s||_{L2(rho_s)} <= (1/2)*FI + (1/2)*||tilde_v_s||^2."
  lsiStep := "Using LSI for pi_{t(s)}=tilde_pi_s gives FI(rho_s||tilde_pi_s) >= 2*C_LSI(t(s))*KL(rho_s||tilde_pi_s)."
  timeChangedInequality := "d/dt KL(rho_{s(t)} || pi_t) <= -dot{s}(t)*C_LSI(t)*KL(rho_{s(t)}||pi_t) + (1/2)*dot{s}(t)^(-1)*||v_t||_{L2(rho_{s(t)})}^2."
  requiredRegularity := [
    "differentiability in s and t of the density paths and KL quantity",
    "smooth positive densities for rho_s, tilde_pi_s, and pi_t on the common state space",
    "integration-by-parts hypotheses or boundary decay eliminating boundary terms",
    "continuity/integrability of C_LSI(t), dot{s}(t), and the velocity L2 term"
  ]
  sourceGaps := [
    "main_body.tex states the slowdown is smooth monotone but does not spell out the full inverse-function interface needed for dot{t}(s(t)) = dot{s}(t)^(-1)",
    "appendix.tex uses differentiation under the integral and integration by parts without explicit dominated-convergence or boundary assumptions",
    "the theorem statement does not explicitly state continuity of t -> C_LSI(t) or t -> E_alpha(pi_t,v_t), which Gronwall/integration later require"
  ]
  dependencies := [
    "eq:SALD",
    "eq:FP-eq",
    "eq:LSI-KL-FI",
    "TransportVelocityContract",
    "KLContract",
    "FIContract"
  ]
  status := ProofStatus.obligation