AutoSamplingTheory.SALD.generalMovingTargetStatementContract

Data definition / provenance and workflow record

Meaning and type

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

def generalMovingTargetStatementContract : GeneralMovingTargetStatementContract

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

sourceStatement : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

sourceProof : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

dynamics : String (explicit)

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

dX_s=(dot{t}(s)*c_{t(s)}(X_s)+(sigma_{t(s)}^2/2)*nabla log pi_{t(s)}(X_s)) ds + sigma_{t(s)} dW_s.

residualField : String (explicit)

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

v_t is a transport velocity for pi_t and m_t(x)=v_t(x)-c_t(x).

lsiAssumption : String (explicit)

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

pi_t satisfies LSI with constant C_LSI(t)>=0 for every t in [0,T].

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,m_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].

terminalBound : String (explicit)

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

KL(rho_S||pi_T) is bounded by the product of exp(-int_0^T (sigma_t^2/2)*dot{s}(t)*C_LSI(t)dt), exp(int_0^T sigma_t^(-2)*dot{s}(t)^(-1)*alpha^(-1)dt), and KL(rho_0||pi_0), plus the residual integral with sigma_t^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t).

pureContractionCase : String (explicit)

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

If c_t=v_t for all t,x, then m_t=0, E_alpha(pi_t,m_t)=0, and the residual integral vanishes.

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).

differentialInequality : String (explicit)

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

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

proofSteps : List String (explicit)

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

Ordered data items

1. appendix.tex:765-835 differentiates KL(rho_s||pi_{t(s)}) and inserts the general VA-SALD Fokker--Planck equation.
2. appendix.tex:835-864 combines the c_t drift with the target transport velocity v_t, exposing the residual m_t=v_t-c_t and applying Young's inequality with epsilon=2*dot{t}(s)/sigma_{t(s)}^2.
3. appendix.tex:866-884 changes from s to t and applies LSI to convert FI into KL contraction.
4. appendix.tex:886-907 applies Donsker--Varadhan with Z=alpha*||m_t||^2.
5. appendix.tex:908-934 applies lem:gronwall and obtains the displayed theorem bound.
6. appendix.tex:936-945 specializes c_t=v_t to obtain the pure contraction estimate.

dependencies : List String (explicit)

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

Ordered data items

1. eq:general_moving_target_SALD
2. eq:general_moving_target_FP
3. eq:LSI-KL-FI
4. def:alpha-complexity
5. lem:dv_variation
6. lem:gronwall
7. sald.general_moving_target.kl_derivative
8. sald.general_moving_target.dv_m_energy
9. sald.general_moving_target.gronwall_application
10. sald.general_moving_target.gronwall_side_conditions
11. sald.general_moving_target.pure_contraction

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 generalMovingTargetStatementContract : GeneralMovingTargetStatementContract where
  theoremLabel := "thm:general-moving-target-SALD"
  sourceStatement := saldGeneralMovingTargetSource
  sourceProof := saldGeneralMovingTargetSource
  dynamics := "dX_s=(dot{t}(s)*c_{t(s)}(X_s)+(sigma_{t(s)}^2/2)*nabla log pi_{t(s)}(X_s)) ds + sigma_{t(s)} dW_s."
  residualField := "v_t is a transport velocity for pi_t and m_t(x)=v_t(x)-c_t(x)."
  lsiAssumption := "pi_t satisfies LSI with constant C_LSI(t)>=0 for every t in [0,T]."
  alphaComplexityAssumption := "There exists alpha0>0 such that E_{alpha0}(pi_t,m_t)<+infty for every t in [0,T]."
  alphaRange := "For any alpha in (0,alpha0]."
  terminalBound := "KL(rho_S||pi_T) is bounded by the product of exp(-int_0^T (sigma_t^2/2)*dot{s}(t)*C_LSI(t)dt), exp(int_0^T sigma_t^(-2)*dot{s}(t)^(-1)*alpha^(-1)dt), and KL(rho_0||pi_0), plus the residual integral with sigma_t^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t)."
  pureContractionCase := "If c_t=v_t for all t,x, then m_t=0, E_alpha(pi_t,m_t)=0, and the residual integral vanishes."
  proofQuantity := "K(t)=KL(rho_{s(t)}||pi_t)."
  differentialInequality := "dK/dt <= -((sigma_t^2/2)*dot{s}(t)*C_LSI(t)-sigma_t^(-2)*dot{s}(t)^(-1)*alpha^(-1))*K(t)+sigma_t^(-2)*dot{s}(t)^(-1)*E_alpha(pi_t,m_t)."
  proofSteps := [
    "appendix.tex:765-835 differentiates KL(rho_s||pi_{t(s)}) and inserts the general VA-SALD Fokker--Planck equation.",
    "appendix.tex:835-864 combines the c_t drift with the target transport velocity v_t, exposing the residual m_t=v_t-c_t and applying Young's inequality with epsilon=2*dot{t}(s)/sigma_{t(s)}^2.",
    "appendix.tex:866-884 changes from s to t and applies LSI to convert FI into KL contraction.",
    "appendix.tex:886-907 applies Donsker--Varadhan with Z=alpha*||m_t||^2.",
    "appendix.tex:908-934 applies lem:gronwall and obtains the displayed theorem bound.",
    "appendix.tex:936-945 specializes c_t=v_t to obtain the pure contraction estimate."
  ]
  dependencies := [
    "eq:general_moving_target_SALD",
    "eq:general_moving_target_FP",
    "eq:LSI-KL-FI",
    "def:alpha-complexity",
    "lem:dv_variation",
    "lem:gronwall",
    "sald.general_moving_target.kl_derivative",
    "sald.general_moving_target.dv_m_energy",
    "sald.general_moving_target.gronwall_application",
    "sald.general_moving_target.gronwall_side_conditions",
    "sald.general_moving_target.pure_contraction"
  ]
  status := ProofStatus.contractOnly