AutoSamplingTheory.SALD.forwardKlDvFiniteLogMgfWitnessContract

Data definition / provenance and workflow record

Meaning and type

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

def forwardKlDvFiniteLogMgfWitnessContract :
    ForwardKlDvFiniteLogMgfWitnessContract

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

theoremStatement : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldForwardKlSource — 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.

Use nu=rho_{s(t)} and mu=pi_t in the common Euclidean state space of the SALD law and moving target.

testFunction : String (explicit)

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

Z_t(x)=alpha*||v_t(x)||^2, exactly the source choice in appendix.tex:230-235.

finiteAlpha0Assumption : String (explicit)

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

main_body.tex:240-241 assumes E_{alpha0}(pi_t,v_t)<+infty for every t in [0,T].

alphaMonotonicityBridge : String (explicit)

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

Use forwardKlDvAlphaMonotonicityContract to prove log E_{pi_t}[exp(alpha*||v_t||^2)]<+infty for 0<alpha<=alpha0 from the alpha0-complexity assumption before invoking DV.

commonSpaceAndAbsoluteContinuity : String (explicit)

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

The DV step requires rho_{s(t)} and pi_t on the same measurable space with rho_{s(t)} absolutely continuous with respect to pi_t wherever KL(rho_{s(t)}||pi_t) is used.

measurabilityInterface : String (explicit)

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

v_t must be measurable and ||v_t||^2 must be a valid real-valued DV test function under both rho_{s(t)} and pi_t.

scalingStep : String (explicit)

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

After DV gives E_rho[alpha*||v_t||^2] <= KL(rho||pi)+log E_pi[exp(alpha*||v_t||^2)], divide by alpha>0.

outputBound : String (explicit)

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

||v_t||_{L2(rho_{s(t)})}^2 <= alpha^(-1)*K(t)+E_alpha(pi_t,v_t).

coefficientUse : String (explicit)

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

Multiplying by (1/2)*dot{s}(t)^(-1) yields the scalar terms used in appendix.tex:239-241 without changing the factor 1/2.

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.cycle26ForwardKlMiddleContract
4. SALD.saldDvFiniteLogMgfContract
5. sald.dv_variation.finite_log_mgf_interface
6. sald.forward_kl.dv_alpha_mgf_monotonicity
7. SALD.forwardKlDvPositiveAlphaScalingScalar
8. SALD.forwardKlDvPositiveAlphaCoefficientScalar
9. sald.forward_kl.moving_target_dependency_chain

sourceGaps : List String (explicit)

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

Ordered data items

1. the source theorem states finite alpha0-complexity pointwise in t, but does not state the monotonicity lemma from alpha0 to alpha
2. the appendix does not isolate rho_{s(t)} << pi_t before using both KL and the DV formula
3. measurability of v_t and the squared-norm test function is implicit in the paper's vector-field vocabulary

lowerPacket : List String (explicit)

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

Ordered data items

1. Formalize only the alpha0-to-alpha finite-log-mgf monotonicity for Z=alpha*||v_t||^2, or keep it as a precise ProofObligation if no local exponential-moment API is ready.
2. Do not change the theorem's alpha range or add a new finite-mgf assumption to thm:forward-KL.
3. Use SALD.forwardKlDvPositiveAlphaScalingScalar and SALD.forwardKlDvPositiveAlphaCoefficientScalar for the pure real positive-alpha division, but keep the finite-log-mgf, common-space, and measurability backends as obligations.

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 forwardKlDvFiniteLogMgfWitnessContract :
    ForwardKlDvFiniteLogMgfWitnessContract where
  sourceBlock := saldForwardKlDvEnergySource
  theoremStatement := saldForwardKlSource
  dvMeasures := "Use nu=rho_{s(t)} and mu=pi_t in the common Euclidean state space of the SALD law and moving target."
  testFunction := "Z_t(x)=alpha*||v_t(x)||^2, exactly the source choice in appendix.tex:230-235."
  finiteAlpha0Assumption := "main_body.tex:240-241 assumes E_{alpha0}(pi_t,v_t)<+infty for every t in [0,T]."
  alphaMonotonicityBridge := "Use forwardKlDvAlphaMonotonicityContract to prove log E_{pi_t}[exp(alpha*||v_t||^2)]<+infty for 0<alpha<=alpha0 from the alpha0-complexity assumption before invoking DV."
  commonSpaceAndAbsoluteContinuity := "The DV step requires rho_{s(t)} and pi_t on the same measurable space with rho_{s(t)} absolutely continuous with respect to pi_t wherever KL(rho_{s(t)}||pi_t) is used."
  measurabilityInterface := "v_t must be measurable and ||v_t||^2 must be a valid real-valued DV test function under both rho_{s(t)} and pi_t."
  scalingStep := "After DV gives E_rho[alpha*||v_t||^2] <= KL(rho||pi)+log E_pi[exp(alpha*||v_t||^2)], divide by alpha>0."
  outputBound := "||v_t||_{L2(rho_{s(t)})}^2 <= alpha^(-1)*K(t)+E_alpha(pi_t,v_t)."
  coefficientUse := "Multiplying by (1/2)*dot{s}(t)^(-1) yields the scalar terms used in appendix.tex:239-241 without changing the factor 1/2."
  dependencies := [
    "lem:dv_variation",
    "def:alpha-complexity",
    "SALD.cycle26ForwardKlMiddleContract",
    "SALD.saldDvFiniteLogMgfContract",
    "sald.dv_variation.finite_log_mgf_interface",
    "sald.forward_kl.dv_alpha_mgf_monotonicity",
    "SALD.forwardKlDvPositiveAlphaScalingScalar",
    "SALD.forwardKlDvPositiveAlphaCoefficientScalar",
    "sald.forward_kl.moving_target_dependency_chain"
  ]
  sourceGaps := [
    "the source theorem states finite alpha0-complexity pointwise in t, but does not state the monotonicity lemma from alpha0 to alpha",
    "the appendix does not isolate rho_{s(t)} << pi_t before using both KL and the DV formula",
    "measurability of v_t and the squared-norm test function is implicit in the paper's vector-field vocabulary"
  ]
  lowerPacket := [
    "Formalize only the alpha0-to-alpha finite-log-mgf monotonicity for Z=alpha*||v_t||^2, or keep it as a precise ProofObligation if no local exponential-moment API is ready.",
    "Do not change the theorem's alpha range or add a new finite-mgf assumption to thm:forward-KL.",
    "Use SALD.forwardKlDvPositiveAlphaScalingScalar and SALD.forwardKlDvPositiveAlphaCoefficientScalar for the pure real positive-alpha division, but keep the finite-log-mgf, common-space, and measurability backends as obligations."
  ]
  status := ProofStatus.obligation