TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

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.

Finite-support consistency of Nelson–Aalen and Kaplan–Meier

Statement

Let $(T_{i}, C_{i})$ be IID subject pairs with $T_{i}$ independent of $C_{i}$ , and suppose the event-time support is $0 \leq a_{1} < \dots < a_{m}$ . For any fixed $t \geq 0$ with $S (t) = P (T > t) > 0$ and $P (C \geq t) > 0$ , the Kaplan–Meier estimator satisfies ${\hat{S}}_{n} (t) \to_{P} S (t)$ . The Nelson–Aalen estimator satisfies ${\hat{Λ}}_{n} (t) \to_{P} Λ_{d} (t) : = \sum_{a_{j} \leq t} q_{j}, q_{j} = P (T = a_{j} ∣ T \geq a_{j}) .$ Only event times at or before $t$ enter the products and sums. In a discrete event-time model, $Λ_{d} (t)$ is the sum of discrete hazards and is generally not $- \log S (t)$ .

Facts & Assumptions

Given: IID subjects with right-censored observations $U_{i} = \min (T_{i}, C_{i})$ , $δ_{i} = 1 {T_{i} \leq C_{i}}$ ; independent $T_{i}, C_{i}$ ; finite nonnegative event-time support; and positive event and censoring survival through $t$ . Prove the two stated limits.

[F1]

Right-censored observations are $U_{i} = \min (T_{i}, C_{i})$ and $δ_{i} = 1 {T_{i} \leq C_{i}}$ . (Event-time observation, censoring, and truncation schemes)

[F2]

For pooled risk and failure counts, ${\hat{Λ}}_{n} (t) = \int_{[0, t]} \frac{1 {Y_{n} (u) > 0}}{Y_{n} (u)} d N_{n} (u)$ , with the integrand set to zero when $Y_{n} (u) = 0$ , and ${\hat{S}}_{n} (t) = \prod_{0 \leq u \leq t : Δ N_{n} (u) > 0} (1 - Δ N_{n} (u) / Y_{n} (u))$ . A baseline event at $a_{1} = 0$ is included; if $a_{1} > 0$ , there is no time-zero event contribution. (Nelson–Aalen, Kaplan–Meier, and Greenwood estimators)

[F3]

At each support point $a_{j}$ through $t$ , the empirical event-to-risk ratio $d N_{n} (a_{j}) / Y_{n} (a_{j})$ converges in probability to $q_{j}$ . (Finite-support risk-set proportion limits)

[A1]

$T$ and $C$ are independent, event support is finite, and $S (t) > 0$ , $P (C \geq t) > 0$ .

Proof

1.1A1F1F2F3given

Let $k$ be the number of event support points not exceeding $t$ . If $k = 0$ , then $a_{1} > t \geq 0$ , so $a_{1} > 0$ and $T > t$ almost surely; the empty product and sum give the claimed limits. If $k \geq 1$ , positivity of $S (t)$ and $P (C \geq t)$ implies $P (T \geq a_{j}) P (C \geq a_{j}) > 0$ for every $j \leq k$ , so [F3] applies at each of these finitely many points.

1.2A1F1F2F3algebra

Before the first support point, the product is $1 = P (T \geq a_{1})$ . After the product limit through $a_{j - 1}$ converges to $P (T > a_{j - 1})$ , this equals $P (T \geq a_{j})$ because there is no support in $(a_{j - 1}, a_{j})$ . By [F1]–[F2], at $a_{j}$ the product is multiplied by $1 - d N_{n} (a_{j}) / Y_{n} (a_{j})$ and the sum is incremented by $d N_{n} (a_{j}) / Y_{n} (a_{j})$ . [F3] and continuity of finite products and sums give limits $P (T \geq a_{j}) (1 - q_{j}) = P (T > a_{j}) = S (a_{j})$ and $\sum_{ℓ \leq j} q_{ℓ}$ . This also handles $a_{1} = 0$ , since $P (T \geq 0) = 1$ and the baseline failure increment is included.

2.1step 1.1step 1.2algebra∎

Finite induction over $j = 1, \dots, k$ proves both limits at every support point through $t$ . On each interval between successive support points, the estimators and their targets are constant, so the same limits hold at the given $t$ . The Nelson–Aalen limit is the discrete hazard sum displayed in the statement; the proof does not replace it by a continuous cumulative hazard.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 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

Qiqing Yu, Survival Analysis (Lecture Notes), §4.2.2, finite-support consistency proof, PDF pp. 35–36 (standard reference, not scraped)