AutoSamplingTheory.SALD.generalMovingTargetDvFiniteLogMgfWitnessContract

Data definition / provenance and workflow record

Meaning and type

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

def generalMovingTargetDvFiniteLogMgfWitnessContract :
    GeneralMovingTargetDvFiniteLogMgfWitnessContract

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

theoremStatement : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldGeneralMovingTargetSource — 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 general VA-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*||m_t(x)||^2, with m_t=v_t-c_t exactly as in appendix.tex:724-726 and 885-895.

finiteAlpha0Assumption : String (explicit)

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

appendix.tex:724-727 assumes E_{alpha0}(pi_t,m_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.

From 0<alpha<=alpha0 and finite E_{alpha0}(pi_t,m_t), prove finite log E_{pi_t}[exp(alpha*||m_t||^2)] 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 the absolute-continuity/density interface needed for KL(rho_{s(t)}||pi_t).

measurabilityInterface : String (explicit)

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

m_t=v_t-c_t and ||m_t||^2 must be measurable under rho_{s(t)} and pi_t; the source treats this as part of the vector-field smoothness vocabulary.

scalingStep : String (explicit)

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

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

outputBound : String (explicit)

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

||m_t||_{L2(rho_{s(t)})}^2 <= alpha^(-1)*K(t)+E_alpha(pi_t,m_t), matching appendix.tex:887-895.

coefficientUse : String (explicit)

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

Multiplying by sigma_t^(-2)*dot{s}(t)^(-1) yields the scalar terms in appendix.tex:899-907 without changing the sigma-weighted coefficient.

unifiedSpecializationUse : String (explicit)

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

For thm:unified-forward-KL, the source specialization c_t<-u_t identifies m_t=w_t, so this same witness becomes the finite-log-mgf bridge for E_alpha(pi_t,w_t).

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.generalMovingTargetDvPositiveAlphaScalingContract
6. KLContract
7. SALD.generalMovingTargetDvEnergyCandidateContract

sourceGaps : List String (explicit)

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

Ordered data items

1. the source invokes alpha0-to-alpha finite-log-mgf monotonicity for m_t implicitly
2. rho_{s(t)} << pi_t and the common measurable space for the DV instantiation are not isolated as a separate lemma
3. the division by alpha>0 and the rewrite to E_alpha(pi_t,m_t) are displayed in one equality but require separate Lean order and scalar algebra
4. the unified theorem inherits the residual log-mgf witness after m_t=w_t but the appendix proof only states the specialization in one line

lowerPacket : List String (explicit)

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

Ordered data items

1. Target this contract or sald.general_moving_target.dv_finite_log_mgf_witness only.
2. Refine one backend: alpha0-to-alpha monotonicity for m_t, common-space/absolute-continuity, measurability of ||m_t||^2, or positive-alpha scaling.
3. Keep lem:dv_variation source-cited and do not add a new finite-mgf assumption to thm:general-moving-target-SALD or thm:unified-forward-KL.
4. Preserve the downstream sigma_t^(-2)*dot{s}(t)^(-1)*alpha^(-1) coefficient.

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 generalMovingTargetDvFiniteLogMgfWitnessContract :
    GeneralMovingTargetDvFiniteLogMgfWitnessContract where
  sourceBlock := saldGeneralMovingTargetResidualDvSource
  theoremStatement := saldGeneralMovingTargetSource
  dvMeasures := "Use nu=rho_{s(t)} and mu=pi_t in the common Euclidean state space of the general VA-SALD law and moving target."
  testFunction := "Z_t(x)=alpha*||m_t(x)||^2, with m_t=v_t-c_t exactly as in appendix.tex:724-726 and 885-895."
  finiteAlpha0Assumption := "appendix.tex:724-727 assumes E_{alpha0}(pi_t,m_t)<+infty for every t in [0,T]."
  alphaMonotonicityBridge := "From 0<alpha<=alpha0 and finite E_{alpha0}(pi_t,m_t), prove finite log E_{pi_t}[exp(alpha*||m_t||^2)] before invoking DV."
  commonSpaceAndAbsoluteContinuity := "The DV step requires rho_{s(t)} and pi_t on the same measurable space with the absolute-continuity/density interface needed for KL(rho_{s(t)}||pi_t)."
  measurabilityInterface := "m_t=v_t-c_t and ||m_t||^2 must be measurable under rho_{s(t)} and pi_t; the source treats this as part of the vector-field smoothness vocabulary."
  scalingStep := "After DV bounds E_{rho_{s(t)}}[alpha*||m_t||^2], divide by alpha>0 and rewrite the log-mgf term as E_alpha(pi_t,m_t)."
  outputBound := "||m_t||_{L2(rho_{s(t)})}^2 <= alpha^(-1)*K(t)+E_alpha(pi_t,m_t), matching appendix.tex:887-895."
  coefficientUse := "Multiplying by sigma_t^(-2)*dot{s}(t)^(-1) yields the scalar terms in appendix.tex:899-907 without changing the sigma-weighted coefficient."
  unifiedSpecializationUse := "For thm:unified-forward-KL, the source specialization c_t<-u_t identifies m_t=w_t, so this same witness becomes the finite-log-mgf bridge for E_alpha(pi_t,w_t)."
  dependencies := [
    "lem:dv_variation",
    "def:alpha-complexity",
    "SALD.saldDvFiniteLogMgfContract",
    "sald.dv_variation.finite_log_mgf_interface",
    "SALD.generalMovingTargetDvPositiveAlphaScalingContract",
    "KLContract",
    "SALD.generalMovingTargetDvEnergyCandidateContract"
  ]
  sourceGaps := [
    "the source invokes alpha0-to-alpha finite-log-mgf monotonicity for m_t implicitly",
    "rho_{s(t)} << pi_t and the common measurable space for the DV instantiation are not isolated as a separate lemma",
    "the division by alpha>0 and the rewrite to E_alpha(pi_t,m_t) are displayed in one equality but require separate Lean order and scalar algebra",
    "the unified theorem inherits the residual log-mgf witness after m_t=w_t but the appendix proof only states the specialization in one line"
  ]
  lowerPacket := [
    "Target this contract or sald.general_moving_target.dv_finite_log_mgf_witness only.",
    "Refine one backend: alpha0-to-alpha monotonicity for m_t, common-space/absolute-continuity, measurability of ||m_t||^2, or positive-alpha scaling.",
    "Keep lem:dv_variation source-cited and do not add a new finite-mgf assumption to thm:general-moving-target-SALD or thm:unified-forward-KL.",
    "Preserve the downstream sigma_t^(-2)*dot{s}(t)^(-1)*alpha^(-1) coefficient."
  ]
  status := ProofStatus.obligation