An integrable positive-time derivative recovers the zero-origin primitive
ProvedAvramDividend.Classical.integrable_derivative_primitive_at_zeroavram-classicalboundary-regularitycausal-resolventfundamental-theoremzero-discount
A continuous function vanishing at zero is recovered by integrating its derivative on the positive half-line, assuming that derivative is globally integrable there. Differentiability at zero is deliberately unnecessary, allowing a singular kernel at the boundary. This is the missing primitive step for exponentially damped zero-discount scale functions.
Preamble
import Definitions.Def_AvramDividend_Classical_ScaleFunction import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus open AvramDividend.Classical MeasureTheory Set intervalIntegral
Formal statement
theorem AvramDividend.Classical.integrable_derivative_primitive_at_zero
(g k : ℝ → ℝ) (h0 : g 0 = 0)
(hgcont : ContinuousOn g (Ici (0 : ℝ)))
(hk : IntegrableOn k (Ioi (0 : ℝ)) volume)
(hderiv : ∀ t : ℝ, 0 < t → HasDerivAt g (k t) t) :
∀ x : ℝ, 0 < x →
(∫ t in Ioc (0 : ℝ) x, k t ∂volume) = g x := by sorrySource
Mathlib intervalIntegral.integral_deriv_eq_sub_uIoo, intervalIntegrable_iff_integrableOn_Ioc_of_le, and intervalIntegral.integral_congr_uIoo. Application uses weighted derivative integrability and g_theta(0)=0.