AutoSamplingTheory.SALD.generalMovingTargetDiscreteStatementContract

Data definition / provenance and workflow record

Meaning and type

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

def generalMovingTargetDiscreteStatementContract :
    GeneralMovingTargetDiscreteStatementContract

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:general-moving-target-SALD-discrete

sourceStatement : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

sourceProof : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

emUpdate : String (explicit)

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

Discrete-time general VA-SALD eq:SALD_general_EM with drift dot{t}_k*c_{t_k}+(sigma_{t_k}^2/2)*nabla log pi_{t_k} and noise sigma_{t_k}*sqrt(eta)*xi_k.

interpolation : String (explicit)

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

Continuous frozen interpolation eq:general_moving_target_SALD_frozen_interp with hat rho_{s_k}=rho_k^eta and hat rho_{s_{k+1}}=rho_{k+1}^eta.

frozenError : String (explicit)

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

General VA frozen-field error delta_pi^VA from eq:general_discrete_delta_def, bounded by lem:frozen_delta_cross_lip.

constantSchedule : String (explicit)

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

The theorem assumes dot{t}(s)=dot{s}(t)^(-1) is constant, matching the discrete-time linear-slowdown discussion.

assumptions : String (explicit)

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

Same conditions as thm:general-moving-target-SALD plus the space/time Lipschitz, exponential-complexity, and step-size assumptions of lem:frozen_delta_cross_lip.

alphaRange : String (explicit)

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

For any alpha in (0,alpha0] and alpha' in (0,alpha0'].

terminalBound : String (explicit)

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

KL(rho_K^eta||pi_T) is bounded by the Gronwall expression with a(t)=(sigma_eta(t)^2/2)*dot{s}(t)*C_LSI(t)-2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*alpha^(-1)-2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t) and b(t)=2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t)+2*dot{s}(t)*eta*Delta(t).

proofQuantity : 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 K(T)=KL(rho_K^eta||pi_T) by endpoint law matching.

differentialInequality : String (explicit)

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

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

proofSteps : List String (explicit)

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

Ordered data items

1. appendix.tex:953-1024 defines the EM update, frozen interpolation, sigma_eta, phi_t, and delta_pi^VA.
2. appendix.tex:1026-1307 proves lem:frozen_delta_cross_lip for the general VA frozen-field error.
3. appendix.tex:1354-1488 differentiates KL(hat rho_s||tilde pi_s), inserts the interpolation Fokker--Planck equation, and decomposes the cross term into delta_pi^VA plus dot{t}*m_t.
4. appendix.tex:1493-1542 applies Young to the m_t term, applies the frozen-delta lemma, and uses LSI.
5. appendix.tex:1544-1598 applies DV to m_t and changes from s to t.
6. appendix.tex:1600 applies lem:gronwall to obtain eq:general_moving_target_KL_bound_discrete.

dependencies : List String (explicit)

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

Ordered data items

1. thm:general-moving-target-SALD
2. eq:SALD_general_EM
3. eq:general_moving_target_SALD_frozen_interp
4. eq:general_discrete_delta_def
5. lem:frozen_delta_cross_lip
6. lem:dv_variation
7. lem:gronwall
8. sald.general_moving_target_discrete.em_interpolation_fp
9. sald.general_moving_target_discrete.frozen_delta_cross_lip
10. sald.general_moving_target_discrete.kl_derivative
11. sald.general_moving_target_discrete.dv_m_energy
12. sald.general_moving_target_discrete.gronwall_application
13. sald.general_moving_target_discrete.gronwall_side_conditions

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 generalMovingTargetDiscreteStatementContract :
    GeneralMovingTargetDiscreteStatementContract where
  theoremLabel := "thm:general-moving-target-SALD-discrete"
  sourceStatement := saldGeneralMovingTargetDiscreteSource
  sourceProof := saldGeneralMovingTargetDiscreteSource
  emUpdate := "Discrete-time general VA-SALD eq:SALD_general_EM with drift dot{t}_k*c_{t_k}+(sigma_{t_k}^2/2)*nabla log pi_{t_k} and noise sigma_{t_k}*sqrt(eta)*xi_k."
  interpolation := "Continuous frozen interpolation eq:general_moving_target_SALD_frozen_interp with hat rho_{s_k}=rho_k^eta and hat rho_{s_{k+1}}=rho_{k+1}^eta."
  frozenError := "General VA frozen-field error delta_pi^VA from eq:general_discrete_delta_def, bounded by lem:frozen_delta_cross_lip."
  constantSchedule := "The theorem assumes dot{t}(s)=dot{s}(t)^(-1) is constant, matching the discrete-time linear-slowdown discussion."
  assumptions := "Same conditions as thm:general-moving-target-SALD plus the space/time Lipschitz, exponential-complexity, and step-size assumptions of lem:frozen_delta_cross_lip."
  alphaRange := "For any alpha in (0,alpha0] and alpha' in (0,alpha0']."
  terminalBound := "KL(rho_K^eta||pi_T) is bounded by the Gronwall expression with a(t)=(sigma_eta(t)^2/2)*dot{s}(t)*C_LSI(t)-2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*alpha^(-1)-2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t) and b(t)=2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t)+2*dot{s}(t)*eta*Delta(t)."
  proofQuantity := "K(t)=KL(hat rho_{s(t)}||pi_t), with K(T)=KL(rho_K^eta||pi_T) by endpoint law matching."
  differentialInequality := "dK/dt <= -((sigma_eta(t)^2/2)*dot{s}(t)*C_LSI(t)-2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*alpha^(-1)-2*dot{s}(t)*eta^2*alpha'^(-1)*Gamma(t))*K(t)+2*sigma_eta(t)^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t)+2*dot{s}(t)*eta*Delta(t)."
  proofSteps := [
    "appendix.tex:953-1024 defines the EM update, frozen interpolation, sigma_eta, phi_t, and delta_pi^VA.",
    "appendix.tex:1026-1307 proves lem:frozen_delta_cross_lip for the general VA frozen-field error.",
    "appendix.tex:1354-1488 differentiates KL(hat rho_s||tilde pi_s), inserts the interpolation Fokker--Planck equation, and decomposes the cross term into delta_pi^VA plus dot{t}*m_t.",
    "appendix.tex:1493-1542 applies Young to the m_t term, applies the frozen-delta lemma, and uses LSI.",
    "appendix.tex:1544-1598 applies DV to m_t and changes from s to t.",
    "appendix.tex:1600 applies lem:gronwall to obtain eq:general_moving_target_KL_bound_discrete."
  ]
  dependencies := [
    "thm:general-moving-target-SALD",
    "eq:SALD_general_EM",
    "eq:general_moving_target_SALD_frozen_interp",
    "eq:general_discrete_delta_def",
    "lem:frozen_delta_cross_lip",
    "lem:dv_variation",
    "lem:gronwall",
    "sald.general_moving_target_discrete.em_interpolation_fp",
    "sald.general_moving_target_discrete.frozen_delta_cross_lip",
    "sald.general_moving_target_discrete.kl_derivative",
    "sald.general_moving_target_discrete.dv_m_energy",
    "sald.general_moving_target_discrete.gronwall_application",
    "sald.general_moving_target_discrete.gronwall_side_conditions"
  ]
  status := ProofStatus.contractOnly