AutoSamplingTheory.SALD.saldDvFiniteLogMgfContract

Data definition / provenance and workflow record

Meaning and type

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

def saldDvFiniteLogMgfContract : DvFiniteLogMgfContract

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

formula : String (explicit)

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

KL(nu||mu)=sup_Z {E_nu[Z]-log E_mu[exp Z]}, with the supremum over random variables satisfying log E_mu[exp Z] < +infty.

commonSpaceInterface : String (explicit)

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

mu and nu are probability distributions on the same measurable space; later SALD uses nu=rho_{s(t)} or hat rho_s and mu=pi_t or tilde pi_s.

testFunctionClass : String (explicit)

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

Z is a measurable real random variable; theorem blocks instantiate Z with alpha*||v_t||^2, alpha*||m_t||^2, and frozen-defect squared norms.

finiteLogMgfCondition : String (explicit)

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

Each instantiation must provide log E_mu[exp Z] < +infty before the cited formula can be applied.

saldInstantiations : List String (explicit)

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

Ordered data items

1. forward-KL: Z=alpha*||v_t||^2 under mu=pi_t.
2. discrete forward-KL: Z=alpha*||v_{t(s)}||^2 under mu=pi_{t(s)}.
3. general moving-target VA-SALD: Z=alpha*||m_t||^2 under mu=pi_t.
4. general discrete VA-SALD and frozen-delta bounds: residual or frozen squared-norm tests under the source alpha/alpha' complexity assumptions.

alphaComplexityWitness : String (explicit)

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

The finite alpha0-complexity assumptions in the theorem statements are the intended source witness for finite log-mgf when 0 < alpha <= alpha0; Lean still needs the monotonicity/measurability bridge.

dependencies : List String (explicit)

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

Ordered data items

1. probability.dv_variational_formula
2. dvVariationalFormulaInterface
3. KLContract
4. def:alpha-complexity

sourceGaps : List String (explicit)

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

Ordered data items

1. appendix.tex cites the DV formula but does not state the measurable-space or random-variable class in Lean terms
2. finite log-mgf monotonicity from alpha0 to smaller alpha is used later but is not proved in the source

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 saldDvFiniteLogMgfContract : DvFiniteLogMgfContract where
  sourceBlock := saldDvVariationSource
  formula := "KL(nu||mu)=sup_Z {E_nu[Z]-log E_mu[exp Z]}, with the supremum over random variables satisfying log E_mu[exp Z] < +infty."
  commonSpaceInterface := "mu and nu are probability distributions on the same measurable space; later SALD uses nu=rho_{s(t)} or hat rho_s and mu=pi_t or tilde pi_s."
  testFunctionClass := "Z is a measurable real random variable; theorem blocks instantiate Z with alpha*||v_t||^2, alpha*||m_t||^2, and frozen-defect squared norms."
  finiteLogMgfCondition := "Each instantiation must provide log E_mu[exp Z] < +infty before the cited formula can be applied."
  saldInstantiations := [
    "forward-KL: Z=alpha*||v_t||^2 under mu=pi_t.",
    "discrete forward-KL: Z=alpha*||v_{t(s)}||^2 under mu=pi_{t(s)}.",
    "general moving-target VA-SALD: Z=alpha*||m_t||^2 under mu=pi_t.",
    "general discrete VA-SALD and frozen-delta bounds: residual or frozen squared-norm tests under the source alpha/alpha' complexity assumptions."
  ]
  alphaComplexityWitness := "The finite alpha0-complexity assumptions in the theorem statements are the intended source witness for finite log-mgf when 0 < alpha <= alpha0; Lean still needs the monotonicity/measurability bridge."
  dependencies := ["probability.dv_variational_formula", "dvVariationalFormulaInterface", "KLContract", "def:alpha-complexity"]
  sourceGaps := [
    "appendix.tex cites the DV formula but does not state the measurable-space or random-variable class in Lean terms",
    "finite log-mgf monotonicity from alpha0 to smaller alpha is used later but is not proved in the source"
  ]
  status := ProofStatus.obligation