AutoSamplingTheory.SALD.saldGronwallEndpointCalculusContract

Data definition / provenance and workflow record

Meaning and type

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

def saldGronwallEndpointCalculusContract :
    GronwallEndpointCalculusContract

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

intervalInterface : String (explicit)

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

The source works on the closed interval t in [0,t1]; a Lean theorem must choose either endpoint-safe HasDerivWithinAt hypotheses or an absolutely-continuous interval formulation.

derivativeMode : String (explicit)

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

K is only stated differentiable on [0,t1]; the derivative inequality at endpoints and the FTC step must be phrased so endpoint values K 0 and K t1 are admissible.

integratingFactor : String (explicit)

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

I(t)=exp(int u in 0..t, a u), exactly the factor in appendix.tex:58.

productDerivativeStep : String (explicit)

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

Show d/dt (I(t)*K(t)) <= I(t)*b(t) by differentiating I, using d/dt int_0^t a=a(t), and substituting dK/dt <= -a(t)*K(t)+b(t); the pointwise HasDerivAt/product/scalar part now builds as SALD.gronwallIntegratingFactorDerivativeLeOfIntegral.

orderIntegrationStep : String (explicit)

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

Integrate the derivative inequality from 0 to t1 and preserve the inequality direction using interval-integral monotonicity; the local HasDerivAt/FTC order step now builds as SALD.gronwallOrderIntegrationOfHasDerivAt once f' and g are interval-integrable.

endpointEvaluation : String (explicit)

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

The integrated expression is I(t1)*K(t1) <= K(0)+int_0^t1 I(t)*b(t)dt, since I(0)=exp(0)=1; the scalar endpoint/multiplication algebra now builds as SALD.gronwallEndpointEvaluationScalar and SALD.gronwallEndpointMultiplyByExpNegScalar.

exponentAlgebra : String (explicit)

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

After multiplying by exp(-int_0^t1 a), rewrite exp(-int_0^t1 a)*exp(int_0^t a) as exp(-int_t^t1 a), matching appendix.tex:65-69; SALD.gronwallEndpointIntegralRewrite now packages this endpoint integral rewrite.

reusableInstantiations : List String (explicit)

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

Ordered data items

1. continuous forward-KL Gronwall application
2. discrete forward-KL Gronwall accumulation
3. continuous general moving-target VA-SALD Gronwall application
4. discrete general moving-target VA-SALD Gronwall application

dependencies : List String (explicit)

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

Ordered data items

1. SALD.saldGronwallCandidateContract
2. SALD.gronwallIntegratingFactorProductDerivative
3. SALD.gronwallIntegratingFactorDerivativeInequalityScalar
4. SALD.gronwallIntegratingFactorDerivativeLe
5. SALD.gronwallIntegratingFactorDerivativeLeOfIntegral
6. SALD.gronwallOrderIntegrationOfHasDerivAt
7. SALD.gronwallOrderIntegrationOfHasDerivRight
8. SALD.gronwallEndpointEvaluationScalar
9. SALD.gronwallEndpointMultiplyByExpNegScalar
10. SALD.gronwallEndpointIntegralRewrite
11. SALD.gronwallIntegratingFactorBoundOfDerivatives
12. SALD.gronwallIntegratingFactorBoundOfIntegral
13. SALD.gronwallIntegratingFactorBoundOfInteriorDerivatives
14. SALD.gronwallCoefficientSideConditionsOfContinuous
15. SALD.gronwallIntegratingFactorBoundOfContinuousData
16. SALD.gronwallIntegratingFactorBoundOfDifferentiable
17. SALD.gronwallIntegratingFactorBoundOfC1
18. SALD.gronwallIntegratingFactorBoundOfInteriorContinuousData
19. SALD.gronwallIntegratingFactorBoundOfInteriorC1
20. Real intervalIntegral FTC
21. closed-interval derivative or absolute-continuity backend
22. Real.exp positivity and interval-integral additivity

sourceGaps : List String (explicit)

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

Ordered data items

1. appendix.tex:47-71 does not specify whether differentiability on [0,t1] means endpoint one-sided derivatives or an open-neighborhood derivative with endpoint continuity
2. the proof integrates a derivative inequality without spelling out the absolute-continuity or FTC hypotheses
3. the final exponent rewrite uses interval-integral additivity and exp addition algebra that must be supplied locally

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 saldGronwallEndpointCalculusContract :
    GronwallEndpointCalculusContract where
  sourceBlock := saldGronwallSource
  intervalInterface := "The source works on the closed interval t in [0,t1]; a Lean theorem must choose either endpoint-safe HasDerivWithinAt hypotheses or an absolutely-continuous interval formulation."
  derivativeMode := "K is only stated differentiable on [0,t1]; the derivative inequality at endpoints and the FTC step must be phrased so endpoint values K 0 and K t1 are admissible."
  integratingFactor := "I(t)=exp(int u in 0..t, a u), exactly the factor in appendix.tex:58."
  productDerivativeStep := "Show d/dt (I(t)*K(t)) <= I(t)*b(t) by differentiating I, using d/dt int_0^t a=a(t), and substituting dK/dt <= -a(t)*K(t)+b(t); the pointwise HasDerivAt/product/scalar part now builds as SALD.gronwallIntegratingFactorDerivativeLeOfIntegral."
  orderIntegrationStep := "Integrate the derivative inequality from 0 to t1 and preserve the inequality direction using interval-integral monotonicity; the local HasDerivAt/FTC order step now builds as SALD.gronwallOrderIntegrationOfHasDerivAt once f' and g are interval-integrable."
  endpointEvaluation := "The integrated expression is I(t1)*K(t1) <= K(0)+int_0^t1 I(t)*b(t)dt, since I(0)=exp(0)=1; the scalar endpoint/multiplication algebra now builds as SALD.gronwallEndpointEvaluationScalar and SALD.gronwallEndpointMultiplyByExpNegScalar."
  exponentAlgebra := "After multiplying by exp(-int_0^t1 a), rewrite exp(-int_0^t1 a)*exp(int_0^t a) as exp(-int_t^t1 a), matching appendix.tex:65-69; SALD.gronwallEndpointIntegralRewrite now packages this endpoint integral rewrite."
  reusableInstantiations := [
    "continuous forward-KL Gronwall application",
    "discrete forward-KL Gronwall accumulation",
    "continuous general moving-target VA-SALD Gronwall application",
    "discrete general moving-target VA-SALD Gronwall application"
  ]
  dependencies := [
    "SALD.saldGronwallCandidateContract",
    "SALD.gronwallIntegratingFactorProductDerivative",
    "SALD.gronwallIntegratingFactorDerivativeInequalityScalar",
    "SALD.gronwallIntegratingFactorDerivativeLe",
    "SALD.gronwallIntegratingFactorDerivativeLeOfIntegral",
    "SALD.gronwallOrderIntegrationOfHasDerivAt",
    "SALD.gronwallOrderIntegrationOfHasDerivRight",
    "SALD.gronwallEndpointEvaluationScalar",
    "SALD.gronwallEndpointMultiplyByExpNegScalar",
    "SALD.gronwallEndpointIntegralRewrite",
    "SALD.gronwallIntegratingFactorBoundOfDerivatives",
    "SALD.gronwallIntegratingFactorBoundOfIntegral",
    "SALD.gronwallIntegratingFactorBoundOfInteriorDerivatives",
    "SALD.gronwallCoefficientSideConditionsOfContinuous",
    "SALD.gronwallIntegratingFactorBoundOfContinuousData",
    "SALD.gronwallIntegratingFactorBoundOfDifferentiable",
    "SALD.gronwallIntegratingFactorBoundOfC1",
    "SALD.gronwallIntegratingFactorBoundOfInteriorContinuousData",
    "SALD.gronwallIntegratingFactorBoundOfInteriorC1",
    "Real intervalIntegral FTC",
    "closed-interval derivative or absolute-continuity backend",
    "Real.exp positivity and interval-integral additivity"
  ]
  sourceGaps := [
    "appendix.tex:47-71 does not specify whether differentiability on [0,t1] means endpoint one-sided derivatives or an open-neighborhood derivative with endpoint continuity",
    "the proof integrates a derivative inequality without spelling out the absolute-continuity or FTC hypotheses",
    "the final exponent rewrite uses interval-integral additivity and exp addition algebra that must be supplied locally"
  ]
  status := ProofStatus.obligation