AutoSamplingTheory.SALD.saldGronwallCandidateContract

Data definition / provenance and workflow record

Meaning and type

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

def saldGronwallCandidateContract : GronwallCandidateContract

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.

timeDomain : String (explicit)

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

0 <= t1, with all hypotheses over t in Set.Icc (0 : Real) t1.

aRegularity : String (explicit)

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

a : Real -> Real is ContinuousOn a (Set.Icc 0 t1), matching the source continuous a_t.

bRegularity : String (explicit)

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

b : Real -> Real is ContinuousOn b (Set.Icc 0 t1), matching the source continuous b_t.

kRegularity : String (explicit)

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

K : Real -> Real is differentiable on [0,t1] in the source; the Lean backend should choose HasDerivWithinAt on Set.Icc 0 t1 or an equivalent endpoint-safe formulation.

differentialInequality : String (explicit)

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

For t in [0,t1], dK/dt t <= -(a t) * K t + b t.

boundAtT1 : String (explicit)

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

K t1 <= exp (-(int u in 0..t1, a u)) * K 0 + int t in 0..t1, exp (-(int u in t..t1, a u)) * b t.

integratingFactorDerivative : String (explicit)

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

d/dt (exp (int u in 0..t, a u) * K t) <= exp (int u in 0..t, a u) * b t.

integratedFactorInequality : String (explicit)

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

exp (int u in 0..t1, a u) * K t1 <= K 0 + int t in 0..t1, exp (int u in 0..t, a u) * b t.

mathlibRoute : List String (explicit)

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

Ordered data items

1. MeasureTheory intervalIntegral over volume on Real intervals
2. ContinuousOn.intervalIntegrable for a, b, and integrating-factor products
3. HasDerivWithinAt or HasDerivAt plus Real.hasDerivAt_exp and product derivative rules
4. SALD.gronwallIntegratingFactorProductDerivative for appendix.tex:58-60
5. SALD.gronwallIntegratingFactorDerivativeInequalityScalar and SALD.gronwallIntegratingFactorDerivativeLeOfIntegral for appendix.tex:60-61
6. SALD.gronwallIntegratingFactorBoundOfDerivatives, SALD.gronwallIntegratingFactorBoundOfIntegral, and SALD.gronwallIntegratingFactorBoundOfContinuousData assemble appendix.tex:58-69 under explicit global Mathlib side conditions
7. SALD.gronwallIntegratingFactorBoundOfDifferentiable rewrites the paper derivative as deriv K, with one explicit product-derivative interval-integrability side condition; SALD.gronwallIntegratingFactorBoundOfC1 discharges that condition when deriv K is continuous
8. SALD.gronwallOrderIntegrationOfHasDerivRight, SALD.gronwallIntegratingFactorBoundOfInteriorDerivatives, SALD.gronwallIntegratingFactorBoundOfInteriorContinuousData, and SALD.gronwallIntegratingFactorBoundOfInteriorC1 remove endpoint derivative hypotheses by using continuity on [0,t1] and right derivatives on (0,t1)
9. intervalIntegral fundamental theorem of calculus / integration by parts for the integrating factor

source : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldGronwallSource — audited data reference, not expanded and not a compiled dependency edge

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 saldGronwallCandidateContract : GronwallCandidateContract where
  timeDomain := "0 <= t1, with all hypotheses over t in Set.Icc (0 : Real) t1."
  aRegularity := "a : Real -> Real is ContinuousOn a (Set.Icc 0 t1), matching the source continuous a_t."
  bRegularity := "b : Real -> Real is ContinuousOn b (Set.Icc 0 t1), matching the source continuous b_t."
  kRegularity := "K : Real -> Real is differentiable on [0,t1] in the source; the Lean backend should choose HasDerivWithinAt on Set.Icc 0 t1 or an equivalent endpoint-safe formulation."
  differentialInequality := "For t in [0,t1], dK/dt t <= -(a t) * K t + b t."
  boundAtT1 := "K t1 <= exp (-(int u in 0..t1, a u)) * K 0 + int t in 0..t1, exp (-(int u in t..t1, a u)) * b t."
  integratingFactorDerivative := "d/dt (exp (int u in 0..t, a u) * K t) <= exp (int u in 0..t, a u) * b t."
  integratedFactorInequality := "exp (int u in 0..t1, a u) * K t1 <= K 0 + int t in 0..t1, exp (int u in 0..t, a u) * b t."
  mathlibRoute := [
    "MeasureTheory intervalIntegral over volume on Real intervals",
    "ContinuousOn.intervalIntegrable for a, b, and integrating-factor products",
    "HasDerivWithinAt or HasDerivAt plus Real.hasDerivAt_exp and product derivative rules",
    "SALD.gronwallIntegratingFactorProductDerivative for appendix.tex:58-60",
    "SALD.gronwallIntegratingFactorDerivativeInequalityScalar and SALD.gronwallIntegratingFactorDerivativeLeOfIntegral for appendix.tex:60-61",
    "SALD.gronwallIntegratingFactorBoundOfDerivatives, SALD.gronwallIntegratingFactorBoundOfIntegral, and SALD.gronwallIntegratingFactorBoundOfContinuousData assemble appendix.tex:58-69 under explicit global Mathlib side conditions",
    "SALD.gronwallIntegratingFactorBoundOfDifferentiable rewrites the paper derivative as deriv K, with one explicit product-derivative interval-integrability side condition; SALD.gronwallIntegratingFactorBoundOfC1 discharges that condition when deriv K is continuous",
    "SALD.gronwallOrderIntegrationOfHasDerivRight, SALD.gronwallIntegratingFactorBoundOfInteriorDerivatives, SALD.gronwallIntegratingFactorBoundOfInteriorContinuousData, and SALD.gronwallIntegratingFactorBoundOfInteriorC1 remove endpoint derivative hypotheses by using continuity on [0,t1] and right derivatives on (0,t1)",
    "intervalIntegral fundamental theorem of calculus / integration by parts for the integrating factor"
  ]
  source := saldGronwallSource
  status := ProofStatus.obligation