AutoSamplingTheory.SALD.discreteForwardKlDvFiniteLogMgfWitnessContract

Data definition / provenance and workflow record

Meaning and type

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

def discreteForwardKlDvFiniteLogMgfWitnessContract :
    DiscreteForwardKlDvFiniteLogMgfWitnessContract

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

theoremStatement : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

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

dvMeasures : String (explicit)

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

appendix.tex:496-507 applies lem:dv_variation with nu=hat rho_s and mu=tilde pi_s=pi_{t(s)} on the common Euclidean state space.

testFunction : String (explicit)

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

Z_s(x)=alpha*||v_{t(s)}(x)||^2, the same squared-velocity test as the continuous theorem but evaluated along the EM interpolation time.

finiteAlpha0Assumption : String (explicit)

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

The theorem assumes the same hypotheses as thm:forward-KL, including finite E_{alpha0}(pi_t,v_t) for every t in [0,T], and main_body.tex:306 takes alpha in (0,alpha0).

alphaMonotonicityBridge : String (explicit)

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

Reuse SALD.forwardKlDvAlphaMonotonicityContract to get finite log E_{pi_{t(s)}}[exp(alpha*||v_{t(s)}||^2)] for the smaller alpha before invoking DV.

interpolationLawInterface : String (explicit)

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

The EM interpolation supplies the law hat rho_s and the slowed target tilde pi_s on each interval [s_k,s_{k+1}], with endpoint laws tracked separately by SALD.discreteForwardKlEmInterpolationSideConditionContract.

commonSpaceAndAbsoluteContinuity : String (explicit)

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

The DV step requires hat rho_s and tilde pi_s on the same measurable space with the absolute-continuity/density interface needed for KL(hat rho_s||tilde pi_s).

measurabilityInterface : String (explicit)

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

v_{t(s)} and ||v_{t(s)}||^2 must be measurable under both hat rho_s and tilde pi_s; this is not supplied by the source as a standalone lemma.

scalingStep : String (explicit)

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

After DV bounds E_{hat rho_s}[alpha*||v_{t(s)}||^2], divide by alpha>0 and rewrite the log-mgf term as E_alpha(pi_{t(s)},v_{t(s)}).

dotTScalingStep : String (explicit)

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

Multiply the resulting bound by dot t(s)^2 because ||tilde v_s||^2=dot t(s)^2*||v_{t(s)}||^2 in appendix.tex:499-515.

outputBound : String (explicit)

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

||tilde v_s||_{L2(hat rho_s)}^2 <= dot t(s)^2*(alpha^(-1)*KL(hat rho_s||tilde pi_s)+E_alpha(pi_{t(s)},v_{t(s)})).

coefficientUse : String (explicit)

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

This supplies the dot t(s)^2*alpha^(-1)*K_s coefficient in appendix.tex:520-531 and, after time change, dot{s}(t)^(-1)*alpha^(-1) in appendix.tex:541-553.

dependencies : List String (explicit)

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

Ordered data items

1. lem:dv_variation
2. def:alpha-complexity
3. SALD.saldDvFiniteLogMgfContract
4. sald.dv_variation.finite_log_mgf_interface
5. sald.forward_kl.dv_alpha_mgf_monotonicity
6. sald.forward_kl.dv_finite_log_mgf_witness
7. sald.discrete_forward_kl.em_endpoint_laws
8. sald.discrete_forward_kl.em_interpolation_fp

sourceGaps : List String (explicit)

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

Ordered data items

1. the appendix directly applies DV under hat rho_s and tilde pi_s without isolating common-space or absolute-continuity hypotheses for the EM interpolation law
2. the source reuses the finite alpha0-complexity assumption from thm:forward-KL but does not restate the alpha0-to-alpha finite-log-mgf bridge for the discrete proof
3. measurability of v_{t(s)} and squared-norm integrability under the interpolated law are implicit in the paper's smoothness vocabulary

lowerPacket : List String (explicit)

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

Ordered data items

1. Formalize or refine the common-space and absolute-continuity side condition for hat rho_s and tilde pi_s before attempting the full DV velocity bound.
2. Reuse the continuous alpha0-to-alpha monotonicity obligation for the pi_t log-mgf; do not add a new theorem assumption.
3. Keep the dot t(s)^2 factor outside the DV bound so the later time-change coefficient remains dot{s}(t)^(-1).

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 discreteForwardKlDvFiniteLogMgfWitnessContract :
    DiscreteForwardKlDvFiniteLogMgfWitnessContract where
  sourceBlock := saldForwardKlDiscreteDvVelocitySource
  theoremStatement := saldForwardKlDiscreteSource
  dvMeasures := "appendix.tex:496-507 applies lem:dv_variation with nu=hat rho_s and mu=tilde pi_s=pi_{t(s)} on the common Euclidean state space."
  testFunction := "Z_s(x)=alpha*||v_{t(s)}(x)||^2, the same squared-velocity test as the continuous theorem but evaluated along the EM interpolation time."
  finiteAlpha0Assumption := "The theorem assumes the same hypotheses as thm:forward-KL, including finite E_{alpha0}(pi_t,v_t) for every t in [0,T], and main_body.tex:306 takes alpha in (0,alpha0)."
  alphaMonotonicityBridge := "Reuse SALD.forwardKlDvAlphaMonotonicityContract to get finite log E_{pi_{t(s)}}[exp(alpha*||v_{t(s)}||^2)] for the smaller alpha before invoking DV."
  interpolationLawInterface := "The EM interpolation supplies the law hat rho_s and the slowed target tilde pi_s on each interval [s_k,s_{k+1}], with endpoint laws tracked separately by SALD.discreteForwardKlEmInterpolationSideConditionContract."
  commonSpaceAndAbsoluteContinuity := "The DV step requires hat rho_s and tilde pi_s on the same measurable space with the absolute-continuity/density interface needed for KL(hat rho_s||tilde pi_s)."
  measurabilityInterface := "v_{t(s)} and ||v_{t(s)}||^2 must be measurable under both hat rho_s and tilde pi_s; this is not supplied by the source as a standalone lemma."
  scalingStep := "After DV bounds E_{hat rho_s}[alpha*||v_{t(s)}||^2], divide by alpha>0 and rewrite the log-mgf term as E_alpha(pi_{t(s)},v_{t(s)})."
  dotTScalingStep := "Multiply the resulting bound by dot t(s)^2 because ||tilde v_s||^2=dot t(s)^2*||v_{t(s)}||^2 in appendix.tex:499-515."
  outputBound := "||tilde v_s||_{L2(hat rho_s)}^2 <= dot t(s)^2*(alpha^(-1)*KL(hat rho_s||tilde pi_s)+E_alpha(pi_{t(s)},v_{t(s)}))."
  coefficientUse := "This supplies the dot t(s)^2*alpha^(-1)*K_s coefficient in appendix.tex:520-531 and, after time change, dot{s}(t)^(-1)*alpha^(-1) in appendix.tex:541-553."
  dependencies := [
    "lem:dv_variation",
    "def:alpha-complexity",
    "SALD.saldDvFiniteLogMgfContract",
    "sald.dv_variation.finite_log_mgf_interface",
    "sald.forward_kl.dv_alpha_mgf_monotonicity",
    "sald.forward_kl.dv_finite_log_mgf_witness",
    "sald.discrete_forward_kl.em_endpoint_laws",
    "sald.discrete_forward_kl.em_interpolation_fp"
  ]
  sourceGaps := [
    "the appendix directly applies DV under hat rho_s and tilde pi_s without isolating common-space or absolute-continuity hypotheses for the EM interpolation law",
    "the source reuses the finite alpha0-complexity assumption from thm:forward-KL but does not restate the alpha0-to-alpha finite-log-mgf bridge for the discrete proof",
    "measurability of v_{t(s)} and squared-norm integrability under the interpolated law are implicit in the paper's smoothness vocabulary"
  ]
  lowerPacket := [
    "Formalize or refine the common-space and absolute-continuity side condition for hat rho_s and tilde pi_s before attempting the full DV velocity bound.",
    "Reuse the continuous alpha0-to-alpha monotonicity obligation for the pi_t log-mgf; do not add a new theorem assumption.",
    "Keep the dot t(s)^2 factor outside the DV bound so the later time-change coefficient remains dot{s}(t)^(-1)."
  ]
  status := ProofStatus.obligation