AutoSamplingTheory.SALD.discreteForwardKlDerivativeCandidateContract

Data definition / provenance and workflow record

Meaning and type

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

def discreteForwardKlDerivativeCandidateContract : DiscreteForwardKlDerivativeCandidateContract

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

interpolationLaw : String (explicit)

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

For s in [s_k,s_{k+1}], hat rho_{s_k}=rho_k^eta and hat rho_{s_{k+1}}=rho_{k+1}^eta.

frozenConditionalDrift : String (explicit)

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

bar b_{k,s}(x)=E[nabla log pi_{t_k}(X_k^eta) | hat X_s=x].

fokkerPlanck : String (explicit)

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

partial_s hat rho_s = -div(hat rho_s*bar b_{k,s}) + Delta hat rho_s, then Delta hat rho_s is split using A_s=nabla log(hat rho_s/tilde pi_s).

klDerivativeIdentity : String (explicit)

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

d/ds KL(hat rho_s||tilde pi_s)=int partial_s hat rho_s*log(hat rho_s/tilde pi_s) - int (hat rho_s/tilde pi_s)*partial_s tilde pi_s.

firstTermEvaluation : String (explicit)

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

Integration by parts yields -FI(hat rho_s||tilde pi_s) minus the frozen drift cross term involving nabla log tilde pi_s - bar b_{k,s}.

targetVelocityTerm : String (explicit)

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

The same tilde v_s=dot{t}(s)*v_{t(s)} transport identity as the continuous proof yields the moving-target cross term.

frozenDefectBound : String (explicit)

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

Apply lem:frozen_delta_cross_lip_sald to bound the frozen score-defect cross term by (1/4)*FI + 2*eta^2*alpha'^(-1)*Gamma*K + 2*eta*Delta.

movingVelocityDvBound : String (explicit)

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

Young gives another (1/4)*FI plus ||tilde v_s||^2; DV with Z=alpha*||v_{t(s)}||^2 and the discrete finite-log-mgf witness bounds this by dot{t}(s)^2*(alpha^(-1)*K + E_alpha(pi_{t(s)},v_{t(s)})).

outputSInequality : String (explicit)

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

d/ds K_s <= -(C_LSI(t(s)) - dot{t}(s)^2*alpha^(-1) - 2*eta^2*alpha'^(-1)*Gamma(t(s)))*K_s + dot{t}(s)^2*E_alpha(pi_{t(s)},v_{t(s)}) + 2*eta*Delta(t(s)).

timeChangedInequality : String (explicit)

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

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

requiredRegularity : List String (explicit)

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

Ordered data items

1. piecewise differentiability of the EM interpolation law hat rho_s on each interval [s_k,s_{k+1}]
2. existence of the conditional drift bar b_{k,s} and Fokker--Planck equation for the interpolation
3. density positivity, finite KL/FI, differentiation-under-integral, and integration-by-parts conditions for hat rho_s and tilde pi_s
4. endpoint law matching and continuity of the stitched KL path at s_k and s_{k+1}
5. inverse-schedule identities dot{t}(s(t))=dot{s}(t)^(-1) and dot{s}(t)>0

sourceGaps : List String (explicit)

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

Ordered data items

1. appendix.tex uses the interpolation Fokker--Planck equation and conditional drift without a standalone theorem
2. the differentiability and boundary conditions are inherited from the continuous proof but not restated for the EM interpolation
3. the Gronwall argument is applied across the stitched interpolation intervals without separately spelling out endpoint continuity of K

dependencies : List String (explicit)

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

Ordered data items

1. eq:frozen_interp_terminal_disc_prop_additive_final
2. lem:frozen_delta_cross_lip_sald
3. eq:LSI-KL-FI
4. lem:dv_variation
5. SALD.discreteForwardKlPostLsiDerivativeBoundScalar
6. SALD.discreteForwardKlPostLsiDerivativeBoundOfKlFiScalar
7. sald.discrete_forward_kl.dv_finite_log_mgf_witness
8. sald.forward_kl.density_boundary_regular
9. sald.forward_kl.schedule_time_change
10. sald.discrete_forward_kl.em_endpoint_laws
11. sald.discrete_forward_kl.em_conditional_fokker_planck

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 discreteForwardKlDerivativeCandidateContract : DiscreteForwardKlDerivativeCandidateContract where
  sourceBlock := saldForwardKlDiscreteDerivativeSource
  interpolationLaw := "For s in [s_k,s_{k+1}], hat rho_{s_k}=rho_k^eta and hat rho_{s_{k+1}}=rho_{k+1}^eta."
  frozenConditionalDrift := "bar b_{k,s}(x)=E[nabla log pi_{t_k}(X_k^eta) | hat X_s=x]."
  fokkerPlanck := "partial_s hat rho_s = -div(hat rho_s*bar b_{k,s}) + Delta hat rho_s, then Delta hat rho_s is split using A_s=nabla log(hat rho_s/tilde pi_s)."
  klDerivativeIdentity := "d/ds KL(hat rho_s||tilde pi_s)=int partial_s hat rho_s*log(hat rho_s/tilde pi_s) - int (hat rho_s/tilde pi_s)*partial_s tilde pi_s."
  firstTermEvaluation := "Integration by parts yields -FI(hat rho_s||tilde pi_s) minus the frozen drift cross term involving nabla log tilde pi_s - bar b_{k,s}."
  targetVelocityTerm := "The same tilde v_s=dot{t}(s)*v_{t(s)} transport identity as the continuous proof yields the moving-target cross term."
  frozenDefectBound := "Apply lem:frozen_delta_cross_lip_sald to bound the frozen score-defect cross term by (1/4)*FI + 2*eta^2*alpha'^(-1)*Gamma*K + 2*eta*Delta."
  movingVelocityDvBound := "Young gives another (1/4)*FI plus ||tilde v_s||^2; DV with Z=alpha*||v_{t(s)}||^2 and the discrete finite-log-mgf witness bounds this by dot{t}(s)^2*(alpha^(-1)*K + E_alpha(pi_{t(s)},v_{t(s)}))."
  outputSInequality := "d/ds K_s <= -(C_LSI(t(s)) - dot{t}(s)^2*alpha^(-1) - 2*eta^2*alpha'^(-1)*Gamma(t(s)))*K_s + dot{t}(s)^2*E_alpha(pi_{t(s)},v_{t(s)}) + 2*eta*Delta(t(s))."
  timeChangedInequality := "d/dt K(t) <= -(dot{s}(t)*C_LSI(t) - dot{s}(t)^(-1)*alpha^(-1) - 2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t))*K(t) + dot{s}(t)^(-1)*E_alpha(pi_t,v_t) + 2*dot{s}(t)*eta*Delta(t)."
  requiredRegularity := [
    "piecewise differentiability of the EM interpolation law hat rho_s on each interval [s_k,s_{k+1}]",
    "existence of the conditional drift bar b_{k,s} and Fokker--Planck equation for the interpolation",
    "density positivity, finite KL/FI, differentiation-under-integral, and integration-by-parts conditions for hat rho_s and tilde pi_s",
    "endpoint law matching and continuity of the stitched KL path at s_k and s_{k+1}",
    "inverse-schedule identities dot{t}(s(t))=dot{s}(t)^(-1) and dot{s}(t)>0"
  ]
  sourceGaps := [
    "appendix.tex uses the interpolation Fokker--Planck equation and conditional drift without a standalone theorem",
    "the differentiability and boundary conditions are inherited from the continuous proof but not restated for the EM interpolation",
    "the Gronwall argument is applied across the stitched interpolation intervals without separately spelling out endpoint continuity of K"
  ]
  dependencies := [
    "eq:frozen_interp_terminal_disc_prop_additive_final",
    "lem:frozen_delta_cross_lip_sald",
    "eq:LSI-KL-FI",
    "lem:dv_variation",
    "SALD.discreteForwardKlPostLsiDerivativeBoundScalar",
    "SALD.discreteForwardKlPostLsiDerivativeBoundOfKlFiScalar",
    "sald.discrete_forward_kl.dv_finite_log_mgf_witness",
    "sald.forward_kl.density_boundary_regular",
    "sald.forward_kl.schedule_time_change",
    "sald.discrete_forward_kl.em_endpoint_laws",
    "sald.discrete_forward_kl.em_conditional_fokker_planck"
  ]
  status := ProofStatus.obligation