LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Inter-event survival and density from a conditional intensity

Statement

Fix a supplied event history $h$ at time $t$ in the model of Temporal point-process models and conditional intensity. Let $λ_{h}^{*} (u)$ be its nonnegative no-event conditional hazard, supplied as a locally integrable version on every finite interval, and put $Λ_{h} (u) : = \int_{t}^{u} λ_{h}^{*} (s) d s .$ For each finite $U > t$ , on $t \leq u \leq U$ the conditional survivor and finite- time density of the next event are $S_{h} (u) = \exp (- Λ_{h} (u)), f_{h} (u) = λ_{h}^{*} (u) \exp (- Λ_{h} (u)) for almost every u .$ If $Λ_{h} (u) \to Λ_{h} (\infty) < \infty$ as $u \to \infty$ , then $K_{h} ({\infty}) = \exp (- Λ_{h} (\infty))$ . If $Λ_{h} (u) \to \infty$ , this terminal mass is zero. These conclusions concern one next-event law and do not prove non-explosion of an entire process.

Facts & Assumptions

Given: A history $h$ at time $t$ , a supplied probability kernel for the next waiting time on $(t, \infty]$ , its finite-time density $f_{h}$ , survivor $S_{h}$ , and a nonnegative locally integrable hazard $λ_{h}^{*}$ .

[F1]

The conditional law is a probability kernel on $(t, \infty]$ with finite-time density $f_{h}$ relative to Lebesgue measure, survivor $S_{h} (u) = K_{h} ((u, \infty])$ , and hazard $λ_{h}^{*} (u) = f_{h} (u) / S_{h} (u)$ wherever $S_{h} (u) > 0$ . (Temporal point-process models and conditional intensity, Lebesgue measurable sets, the family $L (R^{n})$ , and the restricted set function $λ_{n}$ )

[F2]

The indefinite integral of an $L^{1}$ function is absolutely continuous and has derivative equal to its integrand almost everywhere; the $L^{1}$ fundamental theorem uses Countable Choice. (The indefinite integral of an $L^{1}$ function is absolutely continuous, The indefinite integral of an $L^{1}$ function is differentiable almost everywhere)

[F3]

Absolutely continuous functions obey the product and chain rules where the derivatives exist, $(\exp)^{'} = \exp$ , and products of absolutely continuous functions are absolutely continuous. (The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The exponential function is smooth and $(\exp)^{'} = \exp$ , The product of two absolutely continuous functions is absolutely continuous)

[F4]

An absolutely continuous function with derivative zero almost everywhere is constant; this result uses Dependent Choice. (An absolutely continuous function with zero derivative almost everywhere is constant)

[F5]

The mean value theorem applies to the exponential on compact intervals, so it is Lipschitz on every bounded interval. (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ , The exponential function is smooth and $(\exp)^{'} = \exp$ )

[F6]

A finite measure is continuous from above on a decreasing sequence of measurable sets. (Continuity from above when one set has finite measure)

[A1]

Full AC is inherited from the temporal model. Countable Choice and Dependent Choice are declared for [F2] and [F4]. (The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ ), The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain)

Proof

1.1A1F1F2given

Since $K_{h} ((t, \infty]) = 1$ , [F1] gives $S_{h} (u) = 1 - \int_{t}^{u} f_{h} (s) d s$ . By [F2], $S_{h}$ and $Λ_{h}$ are absolutely continuous and $S_{h}^{'} = - f_{h} = - λ_{h}^{*} S_{h}$ almost everywhere where $S_{h} > 0$ , while $Λ_{h}^{'} = λ_{h}^{*}$ almost everywhere.

2.1A1F3F4F5step 1.1

Fix a compact interval on which $S_{h} > 0$ . The cumulative hazard is bounded there, say $0 \leq Λ_{h} \leq M$ . By [F5], there is $L > 0$ such that $∣ \exp (x) - \exp (y) ∣ \leq L ∣ x - y ∣$ for $x, y \in [0, M]$ . Since $Λ_{h}$ is absolutely continuous by step 1.1, for every $ε > 0$ its absolute-continuity condition supplies $δ > 0$ such that every permitted finite family of subintervals with total length below $δ$ satisfies $\sum_{j} ∣ Λ_{h} (v_{j}) - Λ_{h} (u_{j}) ∣ < ε / L$ . Therefore $\sum_{j} ∣ \exp (Λ_{h} (v_{j})) - \exp (Λ_{h} (u_{j})) ∣ \leq L \sum_{j} ∣ Λ_{h} (v_{j}) - Λ_{h} (u_{j}) ∣ < ε,$ so $G_{h} : = \exp (Λ_{h})$ is absolutely continuous. By [F3], $G_{h} S_{h}$ is absolutely continuous and $(G_{h} S_{h})^{'} = G_{h} (λ_{h}^{*} S_{h} + S_{h}^{'}) = 0$ almost everywhere. By [F4], $G_{h} S_{h}$ is constant. Its value at $t$ is $1$ , so $S_{h} (u) = \exp (- Λ_{h} (u))$ wherever $S_{h}$ is positive.

3.1F1F6step 2.1algebra∎

Fix finite $U > t$ and suppose $S_{h}$ first reaches zero at some $τ \leq U$ . On $[t, τ)$ , step 2.1 gives $S_{h} (u) = e^{- Λ_{h} (u)} \geq e^{- Λ_{h} (U)} > 0$ . Continuity of $S_{h}$ then gives $S_{h} (τ) > 0$ , a contradiction. Thus the formula holds on all of $[t, U]$ ; substituting it into [F1] gives the density formula almost everywhere. Also $S_{h} (u) = K_{h} ((u, \infty])$ decreases to $K_{h} ({\infty})$ along integer $u \to \infty$ by [F6]. Taking the limit in the survivor formula gives the two stated terminal-mass cases.

Source notes

Rasmussen proves the hazard-to-survival relation by integrating the logarithmic derivative of the survivor, then differentiates to obtain the density. Kass, Eden, and Brown give the same conditional hazard identity and derive the waiting-time density in their full Section 19.4. The proof above keeps the finite-cumulative-hazard case, including its possible mass at $+ \infty$ , separate from process existence and non-explosion.

Depends on

Used by

Dependency tree · two levels

69 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Joseph G. Rasmussen, Lecture Notes: Temporal Point Processes and the Conditional Intensity Function (standard reference, not scraped)
Robert E. Kass, Uri T. Eden, and Emery N. Brown, Analysis of Neural Data, Chapter 19: Point Processes (standard reference, not scraped)