TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

Cause-specific cumulative incidence as an integral against its hazard measure

Statement

For every cause $k \in {1, \dots, K}$ and every $t \geq 0$ , the cumulative incidence decomposes as $F_{k} (t) = \int_{[0, t]} S (u -) d Λ_{k} (u) .$ If $ν_{k}$ has a Lebesgue density $f_{k}$ and $S (u) > 0$ for every $u \in (0, t]$ , then $d Λ_{k} (u) = λ_{k} (u) d u$ for Lebesgue-a.e. $u \in (0, t]$ with $λ_{k} (u) : = f_{k} (u) / S (u)$ , and $F_{k} (t) = \int_{0}^{t} S (u) λ_{k} (u) d u .$

Facts & Assumptions

Given: A finite-cause competing-risk model as in Competing-risk data, cause-specific hazard measures, and cumulative incidence, its event subdistribution $ν_{k}$ , survival function $S$ , and cause-specific hazard measure $Λ_{k}$ .

[F1]

Competing-risk data, cause-specific hazard measures, and cumulative incidence: $F_{k} (t) = ν_{k} ([0, t])$ , $S (u -) = P (T \geq u)$ , and $Λ_{k} = w ν_{k}$ with $w (u) = 1 / S (u -)$ when $S (u -) > 0$ and $w (u) = 0$ otherwise.

[F2]

The measure with density $f$ relative to $μ$ : if $w$ is nonnegative and measurable, then $w ν_{k}$ is the measure defined by $(w ν_{k}) (B) = \int_{B} w d ν_{k}$ .

[F3]

Integrating against a density agrees with integrating the product: for nonnegative measurable $f, g$ , $\int g d (f d μ) = \int g f d μ$ .

[F4]

Every monotone real function is Borel measurable: every monotone real function is Borel measurable.

Proof

1.1F1givenalgebra

The set function $ν_{k} (B) = P (T \in B, D = k)$ is a finite measure: it is the restriction of the law of $(T, D)$ to the measurable cause slice $D = k$ , so disjoint Borel sets have disjoint preimages and probability countable additivity applies.

2.1F1F4step 1.1

The function $s (u) : = S (u -) = P (T \geq u)$ is nonincreasing, hence Borel by [F4]. Thus $R : = {u : s (u) > 0}$ is Borel and $w = s^{- 1} 1_{R}$ is nonnegative Borel.

3.1F1step 2.1given

The set $R^{c}$ is an upper interval. If $R^{c} = [a, \infty)$ , then $ν_{k} (R^{c}) \leq P (T \geq a) = s (a) = 0$ . If $R^{c} = (a, \infty)$ , then ${T > a} = ⋃_{m \geq 1} {T \geq a + 1 / m}$ and each event on the right has probability $s (a + 1 / m) = 0$ ; hence again $ν_{k} (R^{c}) = 0$ . The empty case is immediate.

3.2F2step 2.1

By [F2], $Λ_{k} = w ν_{k}$ is a measure.

4.1F1F3step 3.1step 3.2algebra

Applying [F3] with $g (u) = 1_{[0, t]} (u) s (u)$ gives $\int_{[0, t]} s (u) d Λ_{k} (u) = \int_{[0, t]} s (u) w (u) d ν_{k} (u) = \int_{[0, t]} 1_{R} (u) d ν_{k} (u) = ν_{k} ([0, t]) = F_{k} (t)$ . The penultimate equality uses step 3.1, so this proves the measure-valued identity, including atoms and $t = 0$ .

5.1F1F3givenstep 4.1algebra∎

Suppose $ν_{k} (d u) = f_{k} (u) d u$ and $S (u) > 0$ for every $u \in (0, t]$ . For each integer $m \geq 1$ , the set $A_{m} : = {u \in (0, t] : P (T = u) \geq 1 / m}$ has at most $m$ points, since distinct singleton events are disjoint and their probabilities sum to at most $1$ . Every positive atom belongs to some $A_{m}$ , so $A : = ⋃_{m \geq 1} A_{m}$ is countable and therefore Lebesgue-null. For $0 < u \leq t$ , the definitions $s (u) = P (T \geq u)$ and $S (u) = P (T > u)$ give $s (u) - S (u) = P (T = u)$ ; hence $s (u) = S (u)$ outside $A$ . Also $s (u) \geq S (u) > 0$ , so $w (u) = 1 / s (u)$ on $(0, t]$ . Since $d ν_{k} = f_{k} d u$ , [F1, F3] give $d Λ_{k} = w f_{k} d u$ , whose density agrees with $f_{k} / S = λ_{k}$ Lebesgue-a.e. on $(0, t]$ . Finally, $ν_{k} ({0}) = 0$ because $ν_{k}$ has a Lebesgue density, so the point $0$ contributes nothing to either side of step 4.1; substituting the density on $(0, t]$ into that identity gives the stated formula, including $t = 0$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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

Lu Tian and Richard Olshen, Competing Risk and Alternatives to Cox Model, Stanford University STAT331, slides 2–12 (standard reference, not scraped)
Janne Pitkäniemi and Esa Läärä, Survival analysis with competing risks, Statistical Practice in Epidemiology using R, University of Tartu, slides 13–24 (standard reference, not scraped)
Peter C. Austin, D. S. Lee, and Jason P. Fine, Introduction to the Analysis of Survival Data in the Presence of Competing Risks, Circulation 133(6) (2016), pp. 601–609 (standard reference, not scraped)