AutoSamplingTheory.SALD.generalMovingTargetDiscreteDerivativeSideConditionContract

Data definition / provenance and workflow record

Meaning and type

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

def generalMovingTargetDiscreteDerivativeSideConditionContract :
    GeneralMovingTargetDiscreteDerivativeSideConditionContract

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

endpointLawInterface : String (explicit)

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

For each EM interval s in [s_k,s_{k+1}], hat rho_s=Law(hat X_s), with hat rho_{s_k}=rho_k^eta and hat rho_{s_{k+1}}=rho_{k+1}^eta before stitching K(t) globally. SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation compiles this endpoint bookkeeping once named law representations and pointwise interpolation identities are supplied.

conditionalDriftInterface : 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 against the joint law of (X_k^eta,hat X_s) through SALD.generalMovingTargetDiscreteConditionalDriftContract, SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract, and SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityContract; only the Measure.map marginal transport plus abstract named-component and regularity handoffs are compiled locally.

fokkerPlanckSplitInterface : String (explicit)

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

partial_s hat rho_s=-div(hat rho_s*bar b_{k,s})+(sigma_eta^2/2)*Delta hat rho_s, then Delta hat rho_s=div(hat rho_s*A_s)+div(hat rho_s*nabla log tilde pi_s); SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignContract states the weak-test FP source-sign interface, SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff, SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff, and SALD.generalMovingTargetDiscreteConditionalFpSourceSignsHandoff preserve the source signs and sigma_eta^2/2 coefficient under explicit weak-FP hypotheses, SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffContract records the log-ratio-test substitution into eq:general_KL_derivative_0_discrete, SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfSourceSigns isolates the normalized weak-FP-to-KL handoff, SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfSourceSignsWithLogAction keeps the log-ratio weak-FP action adjacent to the dK display, SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfAdmissibleSourceSigns composes that substitution through the cycle-72 admissible source-sign wrapper, SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfGeneratorPieces composes it through the cycle-77 generator-piece source-sign wrapper, and SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff proves the sigma-weighted regrouping under abstract divergence linearity.

transportVelocityInterface : String (explicit)

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

If v_t generates pi_t, then tilde v_s=dot t(s)*v_{t(s)} generates tilde pi_s=pi_{t(s)} on the same interval.

frozenResidualAlgebra : String (explicit)

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

(sigma_eta^2/2)*nabla log tilde pi_s - bar b_{k,s} + tilde v_s = delta_pi_{t(s)}^VA + dot t(s)*m_{t(s)}, using m_t=v_t-c_t and eq:general_discrete_delta_def.

youngCoefficientBookkeeping : String (explicit)

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

The source splits the two cross terms with sigma_eta^2/8 each: the m_t term gives 2*sigma_eta^(-2)*dot t(s)^2*||m||^2 and lem:frozen_delta_cross_lip gives 2*Gamma*eta^2*alpha'^(-1)*K+2*Delta*eta.

lsiBookkeeping : String (explicit)

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

After the two sigma_eta^2/8 Young contributions, the remaining -(sigma_eta^2/4)*FI is converted by LSI into -(sigma_eta^2/2)*C_LSI*K.

dvFiniteMgfInterface : String (explicit)

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

DV is applied to Z=alpha*||m_{t(s)}||^2 under hat rho_s versus tilde pi_s, requiring SALD.generalMovingTargetDiscreteDvFiniteLogMgfWitnessContract: alpha0 finite log-mgf, monotonicity for alpha <= alpha0, EM common-space/absolute-continuity, and positive-alpha scaling.

timeChangeAndStitchingInterface : String (explicit)

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

K(t)=KL(hat rho_{s(t)}||pi_t), dK/dt=dot s(t)*d/ds KL at s=s(t), dot t(s(t))=dot s(t)^(-1), and endpoint laws stitch the interval estimates for Gronwall.

requiredRegularity : List String (explicit)

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

Ordered data items

1. conditional law/disintegration for (X_k^eta,hat X_s) and bar b_{k,s}
2. weak-test Fokker-Planck identity with negative drift-divergence and positive sigma_eta^2/2 Laplacian signs
3. smooth positive densities for hat rho_s and tilde pi_s on each EM interval
4. mass conservation, differentiation under the integral, and integration by parts for the KL derivative
5. transport-velocity regularity for v_t and the slowed path tilde pi_s
6. positive sigma_eta(t), dot s(t), and finite KL/FI/residual-energy quantities

sourceGaps : List String (explicit)

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

Ordered data items

1. appendix.tex lines 1354-1387 invoke endpoint laws and the conditional-drift Fokker--Planck equation without a standalone lemma
2. appendix.tex lines 1469-1478 use the frozen/residual algebra after defining delta_pi^VA, but Lean needs an explicit rewrite interface
3. appendix.tex lines 1493-1542 rely on the exact sigma_eta^2/8 + sigma_eta^2/8 Young split to obtain the later doubled residual coefficients
4. appendix.tex lines 1573-1600 pass from interval-wise s-derivatives to a global t-Gronwall inequality without spelling out stitched regularity

dependencies : List String (explicit)

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

Ordered data items

1. eq:SALD_general_EM
2. eq:general_moving_target_SALD_frozen_interp
3. eq:general_discrete_delta_def
4. SALD.generalMovingTargetDiscreteFrozenResidualAlgebraVector
5. SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation
6. SALD.generalMovingTargetDiscreteConditionalDriftContract
7. SALD.generalMovingTargetDiscreteConditionalDriftLinearCombination
8. SALD.generalMovingTargetDiscreteConditionalDriftFieldOfLinearCombination
9. SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract
10. SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityContract
11. SALD.generalMovingTargetDiscreteHatRhoMarginalOfJointMap
12. SALD.generalMovingTargetDiscreteConditionalKernelCompatibilityOfJointMapMarginal
13. SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityOfJointMap
14. SALD.generalMovingTargetDiscreteNamedConditionalDriftComponents
15. SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityHandoff
16. SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityOfComponents
17. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignContract
18. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff
19. SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff
20. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffContract
21. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffScalar
22. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfSourceSigns
23. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfSourceSignsWithLogAction
24. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfAdmissibleSourceSigns
25. SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfGeneratorPieces
26. SALD.generalMovingTargetDiscreteConditionalFpSourceSignsHandoff
27. sald.general_moving_target_discrete.cycle69_em_fp_source_signs_lower
28. SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff
29. sald.general_moving_target_discrete.cycle54_em_fp_lower
30. lem:frozen_delta_cross_lip
31. TransportVelocityContract
32. FokkerPlanckContract
33. KLContract
34. FIContract
35. probability.dv_variational_formula
36. sald.forward_kl.schedule_time_change

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 generalMovingTargetDiscreteDerivativeSideConditionContract :
    GeneralMovingTargetDiscreteDerivativeSideConditionContract where
  sourceBlock := saldGeneralMovingTargetDiscreteDerivativeSource
  endpointLawInterface := "For each EM interval s in [s_k,s_{k+1}], hat rho_s=Law(hat X_s), with hat rho_{s_k}=rho_k^eta and hat rho_{s_{k+1}}=rho_{k+1}^eta before stitching K(t) globally. SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation compiles this endpoint bookkeeping once named law representations and pointwise interpolation identities are supplied."
  conditionalDriftInterface := "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 against the joint law of (X_k^eta,hat X_s) through SALD.generalMovingTargetDiscreteConditionalDriftContract, SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract, and SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityContract; only the Measure.map marginal transport plus abstract named-component and regularity handoffs are compiled locally."
  fokkerPlanckSplitInterface := "partial_s hat rho_s=-div(hat rho_s*bar b_{k,s})+(sigma_eta^2/2)*Delta hat rho_s, then Delta hat rho_s=div(hat rho_s*A_s)+div(hat rho_s*nabla log tilde pi_s); SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignContract states the weak-test FP source-sign interface, SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff, SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff, and SALD.generalMovingTargetDiscreteConditionalFpSourceSignsHandoff preserve the source signs and sigma_eta^2/2 coefficient under explicit weak-FP hypotheses, SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffContract records the log-ratio-test substitution into eq:general_KL_derivative_0_discrete, SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfSourceSigns isolates the normalized weak-FP-to-KL handoff, SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfSourceSignsWithLogAction keeps the log-ratio weak-FP action adjacent to the dK display, SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfAdmissibleSourceSigns composes that substitution through the cycle-72 admissible source-sign wrapper, SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfGeneratorPieces composes it through the cycle-77 generator-piece source-sign wrapper, and SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff proves the sigma-weighted regrouping under abstract divergence linearity."
  transportVelocityInterface := "If v_t generates pi_t, then tilde v_s=dot t(s)*v_{t(s)} generates tilde pi_s=pi_{t(s)} on the same interval."
  frozenResidualAlgebra := "(sigma_eta^2/2)*nabla log tilde pi_s - bar b_{k,s} + tilde v_s = delta_pi_{t(s)}^VA + dot t(s)*m_{t(s)}, using m_t=v_t-c_t and eq:general_discrete_delta_def."
  youngCoefficientBookkeeping := "The source splits the two cross terms with sigma_eta^2/8 each: the m_t term gives 2*sigma_eta^(-2)*dot t(s)^2*||m||^2 and lem:frozen_delta_cross_lip gives 2*Gamma*eta^2*alpha'^(-1)*K+2*Delta*eta."
  lsiBookkeeping := "After the two sigma_eta^2/8 Young contributions, the remaining -(sigma_eta^2/4)*FI is converted by LSI into -(sigma_eta^2/2)*C_LSI*K."
  dvFiniteMgfInterface := "DV is applied to Z=alpha*||m_{t(s)}||^2 under hat rho_s versus tilde pi_s, requiring SALD.generalMovingTargetDiscreteDvFiniteLogMgfWitnessContract: alpha0 finite log-mgf, monotonicity for alpha <= alpha0, EM common-space/absolute-continuity, and positive-alpha scaling."
  timeChangeAndStitchingInterface := "K(t)=KL(hat rho_{s(t)}||pi_t), dK/dt=dot s(t)*d/ds KL at s=s(t), dot t(s(t))=dot s(t)^(-1), and endpoint laws stitch the interval estimates for Gronwall."
  requiredRegularity := [
    "conditional law/disintegration for (X_k^eta,hat X_s) and bar b_{k,s}",
    "weak-test Fokker-Planck identity with negative drift-divergence and positive sigma_eta^2/2 Laplacian signs",
    "smooth positive densities for hat rho_s and tilde pi_s on each EM interval",
    "mass conservation, differentiation under the integral, and integration by parts for the KL derivative",
    "transport-velocity regularity for v_t and the slowed path tilde pi_s",
    "positive sigma_eta(t), dot s(t), and finite KL/FI/residual-energy quantities"
  ]
  sourceGaps := [
    "appendix.tex lines 1354-1387 invoke endpoint laws and the conditional-drift Fokker--Planck equation without a standalone lemma",
    "appendix.tex lines 1469-1478 use the frozen/residual algebra after defining delta_pi^VA, but Lean needs an explicit rewrite interface",
    "appendix.tex lines 1493-1542 rely on the exact sigma_eta^2/8 + sigma_eta^2/8 Young split to obtain the later doubled residual coefficients",
    "appendix.tex lines 1573-1600 pass from interval-wise s-derivatives to a global t-Gronwall inequality without spelling out stitched regularity"
  ]
  dependencies := [
    "eq:SALD_general_EM",
    "eq:general_moving_target_SALD_frozen_interp",
    "eq:general_discrete_delta_def",
    "SALD.generalMovingTargetDiscreteFrozenResidualAlgebraVector",
    "SALD.generalMovingTargetDiscreteEmEndpointLawPairOfNamedInterpolation",
    "SALD.generalMovingTargetDiscreteConditionalDriftContract",
    "SALD.generalMovingTargetDiscreteConditionalDriftLinearCombination",
    "SALD.generalMovingTargetDiscreteConditionalDriftFieldOfLinearCombination",
    "SALD.generalMovingTargetDiscreteConditionalLawMeasurabilityContract",
    "SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityContract",
    "SALD.generalMovingTargetDiscreteHatRhoMarginalOfJointMap",
    "SALD.generalMovingTargetDiscreteConditionalKernelCompatibilityOfJointMapMarginal",
    "SALD.generalMovingTargetDiscreteEndpointConditionalCompatibilityOfJointMap",
    "SALD.generalMovingTargetDiscreteNamedConditionalDriftComponents",
    "SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityHandoff",
    "SALD.generalMovingTargetDiscreteNamedConditionalDriftRegularityOfComponents",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignContract",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsHandoff",
    "SALD.generalMovingTargetDiscreteWeakConditionalFpSourceSignsAdmissibleHandoff",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffContract",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffScalar",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfSourceSigns",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfSourceSignsWithLogAction",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfAdmissibleSourceSigns",
    "SALD.generalMovingTargetDiscreteKlDerivativeWeakFpHandoffOfGeneratorPieces",
    "SALD.generalMovingTargetDiscreteConditionalFpSourceSignsHandoff",
    "sald.general_moving_target_discrete.cycle69_em_fp_source_signs_lower",
    "SALD.generalMovingTargetDiscreteConditionalFpSigmaLaplacianSplitHandoff",
    "sald.general_moving_target_discrete.cycle54_em_fp_lower",
    "lem:frozen_delta_cross_lip",
    "TransportVelocityContract",
    "FokkerPlanckContract",
    "KLContract",
    "FIContract",
    "probability.dv_variational_formula",
    "sald.forward_kl.schedule_time_change"
  ]
  status := ProofStatus.obligation