AutoSamplingTheory.SALD.generalMovingTargetDiscreteConditionalDriftContract

Data definition / provenance and workflow record

Meaning and type

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

def generalMovingTargetDiscreteConditionalDriftContract :
    GeneralMovingTargetDiscreteConditionalDriftContract

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

parentInterface : String (explicit)

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

sald.general_moving_target_discrete.em_interpolation_fp / appendix.tex:1358-1387

randomVariables : String (explicit)

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

On a fixed interval [s_k,s_{k+1}], use the common probability space carrying X_k^eta, the frozen EM interpolation hat X_s, c_{t_k}(X_k^eta), and nabla log pi_{t_k}(X_k^eta).

conditioningMap : String (explicit)

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

Condition on hat X_s=x, with x in the Euclidean state space supporting hat rho_s=Law(hat X_s).

conditionalLawKernel : String (explicit)

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

Provide a regular conditional law of X_k^eta given hat X_s=x, or an equivalent kernel supporting conditional expectations of both drift summands.

driftSummands : String (explicit)

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

dot t_k*c_{t_k}(X_k^eta) and (sigma_eta^2/2)*nabla log pi_{t_k}(X_k^eta), matching appendix.tex:1368-1377.

conditionalExpectationLinearity : String (explicit)

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

The selected conditional expectation must be linear for integrable vector-valued summands; SALD.generalMovingTargetDiscreteConditionalDriftLinearCombination compiles only this algebra after linearity is supplied.

selectedDriftField : String (explicit)

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

bar b_{k,s}(x)=E[dot t_k*c_{t_k}(X_k^eta)+(sigma_eta^2/2)*nabla log pi_{t_k}(X_k^eta) | hat X_s=x], defined pointwise or hat-rho_s-a.e. and usable as the drift field in divergence form.

measurabilityInterface : String (explicit)

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

x |-> bar b_{k,s}(x), and the two selected conditional-expectation summands, must be measurable with respect to the state-space sigma algebra; SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityOfComponents derives bar b_{k,s} regularity from supplied component regularity and closure rules, while SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityHandoff transfers any already-supplied combo predicate by equality.

integrabilityInterface : String (explicit)

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

Both summands must be conditionally integrable; hat rho_s*bar b_{k,s} must have enough local integrability for the weak divergence term; cycle 70 records this as a conditional-law/measurability obligation, not as a proved disintegration theorem.

fokkerPlanckInput : String (explicit)

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

This interface supplies only the regular conditional drift input to partial_s hat rho_s = -div(hat rho_s*bar b_{k,s}) + (sigma_eta^2/2)*Delta hat rho_s; it does not prove the weak Fokker--Planck equation.

exclusions : List String (explicit)

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

Ordered data items

1. Do not prove or mark the regular conditional law itself as formalized in this contract.
2. Do not prove density/absolute-continuity for hat rho_s or tilde pi_s here.
3. Do not prove the weak Fokker-Planck equation, KL differentiation, boundary integration by parts, Laplacian split, LSI, DV, or Gronwall here.
4. Do not add these requirements as hidden hypotheses to thm:general-moving-target-SALD-discrete.

dependencies : List String (explicit)

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

Ordered data items

1. eq:general_moving_target_SALD_frozen_interp
2. SALD.generalVaSaldEulerMaruyamaContract
3. SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation
4. SALD.generalMovingTargetDiscreteEmJointEndpointMeasureMapOfNamedInterpolation
5. SALD.generalMovingTargetDiscreteEmJointEndpointMarginalLawsOfNamedInterpolation
6. SALD.generalMovingTargetDiscreteConditionalDriftLinearCombination
7. SALD.generalMovingTargetDiscreteConditionalDriftFieldOfLinearCombination
8. SALD.generalMovingTargetDiscreteNamedConditionalDriftComponents
9. SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityHandoff
10. SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityOfComponents
11. SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract
12. sald.general_moving_target_discrete.em_interpolation_fp

sourceGaps : List String (explicit)

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

Ordered data items

1. The source defines bar b_{k,s} by conditional expectation but does not spell out the regular conditional probability/kernel.
2. The source does not separately state measurability and integrability of the selected drift field.
3. The source immediately invokes the associated Fokker-Planck equation; Lean needs this drift interface before the weak FP identity can be stated.

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 generalMovingTargetDiscreteConditionalDriftContract :
    GeneralMovingTargetDiscreteConditionalDriftContract where
  sourceBlock := saldGeneralMovingTargetDiscreteDerivativeSource
  parentInterface := "sald.general_moving_target_discrete.em_interpolation_fp / appendix.tex:1358-1387"
  randomVariables := "On a fixed interval [s_k,s_{k+1}], use the common probability space carrying X_k^eta, the frozen EM interpolation hat X_s, c_{t_k}(X_k^eta), and nabla log pi_{t_k}(X_k^eta)."
  conditioningMap := "Condition on hat X_s=x, with x in the Euclidean state space supporting hat rho_s=Law(hat X_s)."
  conditionalLawKernel := "Provide a regular conditional law of X_k^eta given hat X_s=x, or an equivalent kernel supporting conditional expectations of both drift summands."
  driftSummands := "dot t_k*c_{t_k}(X_k^eta) and (sigma_eta^2/2)*nabla log pi_{t_k}(X_k^eta), matching appendix.tex:1368-1377."
  conditionalExpectationLinearity := "The selected conditional expectation must be linear for integrable vector-valued summands; SALD.generalMovingTargetDiscreteConditionalDriftLinearCombination compiles only this algebra after linearity is supplied."
  selectedDriftField := "bar b_{k,s}(x)=E[dot t_k*c_{t_k}(X_k^eta)+(sigma_eta^2/2)*nabla log pi_{t_k}(X_k^eta) | hat X_s=x], defined pointwise or hat-rho_s-a.e. and usable as the drift field in divergence form."
  measurabilityInterface := "x |-> bar b_{k,s}(x), and the two selected conditional-expectation summands, must be measurable with respect to the state-space sigma algebra; SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityOfComponents derives bar b_{k,s} regularity from supplied component regularity and closure rules, while SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityHandoff transfers any already-supplied combo predicate by equality."
  integrabilityInterface := "Both summands must be conditionally integrable; hat rho_s*bar b_{k,s} must have enough local integrability for the weak divergence term; cycle 70 records this as a conditional-law/measurability obligation, not as a proved disintegration theorem."
  fokkerPlanckInput := "This interface supplies only the regular conditional drift input to partial_s hat rho_s = -div(hat rho_s*bar b_{k,s}) + (sigma_eta^2/2)*Delta hat rho_s; it does not prove the weak Fokker--Planck equation."
  exclusions := [
    "Do not prove or mark the regular conditional law itself as formalized in this contract.",
    "Do not prove density/absolute-continuity for hat rho_s or tilde pi_s here.",
    "Do not prove the weak Fokker-Planck equation, KL differentiation, boundary integration by parts, Laplacian split, LSI, DV, or Gronwall here.",
    "Do not add these requirements as hidden hypotheses to thm:general-moving-target-SALD-discrete."
  ]
  dependencies := [
    "eq:general_moving_target_SALD_frozen_interp",
    "SALD.generalVaSaldEulerMaruyamaContract",
    "SALD.generalMovingTargetDiscreteEmEndpointMeasureMapPairOfNamedInterpolation",
    "SALD.generalMovingTargetDiscreteEmJointEndpointMeasureMapOfNamedInterpolation",
    "SALD.generalMovingTargetDiscreteEmJointEndpointMarginalLawsOfNamedInterpolation",
    "SALD.generalMovingTargetDiscreteConditionalDriftLinearCombination",
    "SALD.generalMovingTargetDiscreteConditionalDriftFieldOfLinearCombination",
    "SALD.generalMovingTargetDiscreteNamedConditionalDriftComponents",
    "SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityHandoff",
    "SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityOfComponents",
    "SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract",
    "sald.general_moving_target_discrete.em_interpolation_fp"
  ]
  sourceGaps := [
    "The source defines bar b_{k,s} by conditional expectation but does not spell out the regular conditional probability/kernel.",
    "The source does not separately state measurability and integrability of the selected drift field.",
    "The source immediately invokes the associated Fokker-Planck equation; Lean needs this drift interface before the weak FP identity can be stated."
  ]
  status := ProofStatus.obligation