AutoSamplingTheory.SALD.forwardKlDvAlphaMonotonicityContract

Data definition / provenance and workflow record

Meaning and type

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

def forwardKlDvAlphaMonotonicityContract :
    ForwardKlDvAlphaMonotonicityContract

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

sourceAssumption : 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, i.e. alpha0^(-1)*log E_{pi_t}[exp(alpha0*||v_t||^2)] is finite for every t.

alphaRange : String (explicit)

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

The theorem allows any alpha in (0,alpha0]; the proof must keep alpha>0 for division and alpha<=alpha0 for monotonicity.

nonnegativeEnergy : String (explicit)

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

The scalar q_t(x)=||v_t(x)||^2 is nonnegative, so alpha*q_t(x) <= alpha0*q_t(x) pointwise when alpha<=alpha0.

pointwiseDomination : String (explicit)

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

Use exp monotonicity to show exp(alpha*q_t(x)) <= exp(alpha0*q_t(x)) pointwise, with no change to the source test function Z_t.

expectationBridge : String (explicit)

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

Transfer the pointwise domination through the pi_t integral/expectation to obtain finite E_{pi_t}[exp(alpha*q_t)] from the finite alpha0 expectation.

logMgfBridge : String (explicit)

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

Show log E_{pi_t}[exp(alpha*q_t)] is finite and well-defined before applying lem:dv_variation with Z_t=alpha*q_t.

alphaComplexityRewrite : String (explicit)

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

Rewrite alpha^(-1)*log E_{pi_t}[exp(alpha*q_t)] as E_alpha(pi_t,v_t), matching the definition in main_body.tex:218-223.

downstreamCoefficientUse : String (explicit)

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

After multiplying the DV output by (1/2)*dot{s}(t)^(-1), preserve the source coefficient (1/2)*dot{s}(t)^(-1)*alpha^(-1) in appendix.tex:239-241.

dependencies : List String (explicit)

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

Ordered data items

1. def:alpha-complexity
2. SALD.saldDvFiniteLogMgfContract
3. sald.dv_variation.finite_log_mgf_interface

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 implicitly
2. the Lean backend still needs a measure-integral theorem turning pointwise exponential domination into finite expectation
3. no local theorem currently proves the log finiteness and alpha-complexity rewrite

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 forwardKlDvAlphaMonotonicityContract :
    ForwardKlDvAlphaMonotonicityContract where
  sourceBlock := saldForwardKlDvEnergySource
  theoremStatement := saldForwardKlSource
  sourceAssumption := "main_body.tex:240-241 assumes E_{alpha0}(pi_t,v_t)<+infty, i.e. alpha0^(-1)*log E_{pi_t}[exp(alpha0*||v_t||^2)] is finite for every t."
  alphaRange := "The theorem allows any alpha in (0,alpha0]; the proof must keep alpha>0 for division and alpha<=alpha0 for monotonicity."
  nonnegativeEnergy := "The scalar q_t(x)=||v_t(x)||^2 is nonnegative, so alpha*q_t(x) <= alpha0*q_t(x) pointwise when alpha<=alpha0."
  pointwiseDomination := "Use exp monotonicity to show exp(alpha*q_t(x)) <= exp(alpha0*q_t(x)) pointwise, with no change to the source test function Z_t."
  expectationBridge := "Transfer the pointwise domination through the pi_t integral/expectation to obtain finite E_{pi_t}[exp(alpha*q_t)] from the finite alpha0 expectation."
  logMgfBridge := "Show log E_{pi_t}[exp(alpha*q_t)] is finite and well-defined before applying lem:dv_variation with Z_t=alpha*q_t."
  alphaComplexityRewrite := "Rewrite alpha^(-1)*log E_{pi_t}[exp(alpha*q_t)] as E_alpha(pi_t,v_t), matching the definition in main_body.tex:218-223."
  downstreamCoefficientUse := "After multiplying the DV output by (1/2)*dot{s}(t)^(-1), preserve the source coefficient (1/2)*dot{s}(t)^(-1)*alpha^(-1) in appendix.tex:239-241."
  dependencies := [
    "def:alpha-complexity",
    "SALD.saldDvFiniteLogMgfContract",
    "sald.dv_variation.finite_log_mgf_interface"
  ]
  sourceGaps := [
    "the source invokes alpha0-to-alpha finite-log-mgf monotonicity implicitly",
    "the Lean backend still needs a measure-integral theorem turning pointwise exponential domination into finite expectation",
    "no local theorem currently proves the log finiteness and alpha-complexity rewrite"
  ]
  status := ProofStatus.obligation