AutoSamplingTheory.SALD.discreteForwardKlGronwallInstantiationContract

Data definition / provenance and workflow record

Meaning and type

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

def discreteForwardKlGronwallInstantiationContract : DiscreteForwardKlGronwallInstantiationContract

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

statementBlock : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

quantityK : String (explicit)

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

K(t)=KL(hat rho_{s(t)}||pi_t), with endpoint K(T)=KL(rho_K^eta||pi_T).

gronwallA : String (explicit)

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

a(t)=dot{s}(t)*C_LSI(t) - dot{s}(t)^(-1)*alpha^(-1) - 2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t).

gronwallB : String (explicit)

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

b(t)=dot{s}(t)^(-1)*E_alpha(pi_t,v_t) + 2*dot{s}(t)*eta*Delta(t).

preSpecializationBound : String (explicit)

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

K(T) <= exp(-int_0^T a(t)dt)*K(0) + int_0^T exp(-int_t^T a(u)du)*b(t)dt.

linearSlowdownSpecialization : String (explicit)

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

For t(s)=s/r, dot{s}(t)=r and dot{s}(t)^(-1)=1/r; substituting in the appendix Gronwall bound gives the main-body exponent terms -r*int_0^T C_LSI(t)dt, T/(r*alpha), and 2*r*eta^2*alpha'^(-1)*barGamma.

accumulatedError : String (explicit)

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

The residual integral is bounded by the common positive exponential factor times ((1/r)*A_alpha(pi,v)+2*r*eta*barDelta_{alpha'}), after dropping nonpositive LSI contributions.

requiredRegularity : List String (explicit)

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

Ordered data items

1. integrability of C_LSI, Gamma, Delta, and E_alpha(pi_t,v_t) on [0,T]
2. piecewise differentiability or endpoint-safe absolute continuity of K(t) after stitching EM intervals
3. nonnegativity of C_LSI to discard the LSI part from the residual exponential

sourceGaps : List String (explicit)

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

Ordered data items

1. the source does not state a separate stitched-interval Gronwall lemma for the EM interpolation
2. continuity/integrability of Gamma and Delta is asserted informally as controlled by smoothness and complexities
3. appendix.tex stops at the general-schedule Gronwall bound; the final linear-slowdown algebra is required to match main_body.tex lines 309-323

dependencies : List String (explicit)

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

Ordered data items

1. lem:gronwall
2. sald.discrete_forward_kl.kl_derivative
3. sald.gronwall.integrating_factor
4. sald.discrete_forward_kl.stitched_interval_regularity
5. sald.discrete_forward_kl.linear_slowdown_specialization

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 discreteForwardKlGronwallInstantiationContract : DiscreteForwardKlGronwallInstantiationContract where
  sourceBlock := saldForwardKlDiscreteGronwallSource
  statementBlock := saldForwardKlDiscreteSource
  quantityK := "K(t)=KL(hat rho_{s(t)}||pi_t), with endpoint K(T)=KL(rho_K^eta||pi_T)."
  gronwallA := "a(t)=dot{s}(t)*C_LSI(t) - dot{s}(t)^(-1)*alpha^(-1) - 2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t)."
  gronwallB := "b(t)=dot{s}(t)^(-1)*E_alpha(pi_t,v_t) + 2*dot{s}(t)*eta*Delta(t)."
  preSpecializationBound := "K(T) <= exp(-int_0^T a(t)dt)*K(0) + int_0^T exp(-int_t^T a(u)du)*b(t)dt."
  linearSlowdownSpecialization := "For t(s)=s/r, dot{s}(t)=r and dot{s}(t)^(-1)=1/r; substituting in the appendix Gronwall bound gives the main-body exponent terms -r*int_0^T C_LSI(t)dt, T/(r*alpha), and 2*r*eta^2*alpha'^(-1)*barGamma."
  accumulatedError := "The residual integral is bounded by the common positive exponential factor times ((1/r)*A_alpha(pi,v)+2*r*eta*barDelta_{alpha'}), after dropping nonpositive LSI contributions."
  requiredRegularity := [
    "integrability of C_LSI, Gamma, Delta, and E_alpha(pi_t,v_t) on [0,T]",
    "piecewise differentiability or endpoint-safe absolute continuity of K(t) after stitching EM intervals",
    "nonnegativity of C_LSI to discard the LSI part from the residual exponential"
  ]
  sourceGaps := [
    "the source does not state a separate stitched-interval Gronwall lemma for the EM interpolation",
    "continuity/integrability of Gamma and Delta is asserted informally as controlled by smoothness and complexities",
    "appendix.tex stops at the general-schedule Gronwall bound; the final linear-slowdown algebra is required to match main_body.tex lines 309-323"
  ]
  dependencies := [
    "lem:gronwall",
    "sald.discrete_forward_kl.kl_derivative",
    "sald.gronwall.integrating_factor",
    "sald.discrete_forward_kl.stitched_interval_regularity",
    "sald.discrete_forward_kl.linear_slowdown_specialization"
  ]
  status := ProofStatus.obligation