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.

Conditional hypergeometric moments for a logrank risk set

Statement

Fix a risk set with $Y_{1}$ group-1 subjects, $Y_{0}$ group-0 subjects, and $Y = Y_{1} + Y_{0}$ . Conditional on the margins, suppose the $d$ failing subjects are a uniform $d$ -subset of these $Y$ subjects, where $0 \leq d \leq Y$ . Let $O$ be the number of failures in group 1. If $Y > 1$ , then $E [O] = d \frac{Y_{1}}{Y}, Var (O) = \frac{Y_{1} Y_{0} d (Y - d)}{Y^{2} (Y - 1)} .$ If $Y = 0$ or $Y = 1$ , set the contribution to the variance to zero; the expectation remains $d Y_{1} / Y$ when $Y > 0$ , and is zero when $Y = 0$ .

For the sequential assertion, take a finite sequence $j = 1, \dots, J$ on a probability space with a filtration $H_{0} \subseteq H_{1} \subseteq \dots \subseteq H_{J}$ . Before the failures at step $j$ are revealed, the current risk-set subjects, their group counts $Y_{1 j}, Y_{0 j}$ , and the total $d_{j}$ are $H_{j - 1}$ -measurable, with $0 \leq d_{j} \leq Y_{j} : = Y_{1 j} + Y_{0 j}$ . Conditionally on $H_{j - 1}$ , the failing subjects are a uniform $d_{j}$ -subset of the current $Y_{j}$ subjects; their identities are revealed in $H_{j}$ . If $Y_{j} = 0$ , necessarily $d_{j} = 0$ and the failing subset is empty. Put $E_{j} = d_{j} Y_{1 j} / Y_{j}$ when $Y_{j} > 0$ and $E_{j} = 0$ when $Y_{j} = 0$ ; let $V_{j}$ be the displayed risk-set variance when $Y_{j} > 1$ and zero when $Y_{j} \leq 1$ . Suppose each real weight $w_{j}$ is $H_{j - 1}$ -measurable and $E ⁣ [\sum_{j = 1}^{J} w_{j}^{2} V_{j}] < \infty .$ Then $D_{j} = w_{j} (O_{j} - E_{j})$ are square-integrable martingale differences and $E ⁣ [\sum_{j} D_{j}] = 0, Var ⁣ (\sum_{j} D_{j}) = E ⁣ [\sum_{j} w_{j}^{2} V_{j}],$ where the nonempty-risk-set variance contribution is the one in Two-group logrank and weighted logrank scores.

Facts & Assumptions

Given: A finite risk set, its two group counts, a total failure count $d$ , the uniform-subset allocation model, and, for the sequential assertion, the finite filtration, measurable pre-reveal margins, zero-risk convention, conditional law, predictable weights, and integrability condition stated above.

[F1]

The uniform probability space on a nonempty finite set: the uniform law on a nonempty finite set assigns each element probability equal to the reciprocal of the set's cardinality.

[F2]

The indicator random variable of an event: an indicator is one on its event and zero elsewhere.

[F3]

Expectation is linear for every finite family of random variables, without any independence hypothesis: expectation of a finite sum is the sum of the expectations; independence is not required.

[F4]

Indicators turn event probabilities, intersections, and finite counts into expectations and products: indicator expectations equal event probabilities, and products of indicators equal indicators of intersections.

[F5]

Variance, standard deviation, and covariance on a finite probability space: variance and covariance are expectations of the centered square and centered product.

[F6]

$Var (X) = E [X^{2}] - E [X]^{2}$ and $Cov (X, Y) = E [X Y] - E [X] E [Y]$ : variance and covariance may be expanded as $E [X^{2}] - (E X)^{2}$ and $E [X Y] - E X E Y$ .

[F7]

Two-group logrank and weighted logrank scores: $E_{j} = d_{j} Y_{1 j} / Y_{j}$ , and under the conditional hypergeometric model $V_{j} = Y_{1 j} Y_{0 j} d_{j} (Y_{j} - d_{j}) / (Y_{j}^{2} (Y_{j} - 1))$ when $Y_{j} > 1$ , with zero contribution for $Y_{j} = 1$ .

[A1]

Conditional on $H_{j - 1}$ , which includes the risk-set margins and $d_{j}$ , each $d_{j}$ -subset of the $Y_{j}$ risk-set subjects has equal probability.

Proof

1.1A1F1F2F3F4given

If $Y = 0$ , then $d = 0$ , $O = 0$ , and both stated moments are zero. Suppose $Y \geq 1$ . For each of the $Y_{1}$ group-1 subjects let $I_{a}$ indicate that subject $a$ is in the failing subset. Under [A1], when $d \geq 1$ , $P (I_{a} = 1) = (\binom{Y - 1}{d - 1}) / (\binom{Y}{d}) = d / Y$ ; for $d = 0$ , both sides are zero. Since $O = \sum_{a = 1}^{Y_{1}} I_{a}$ , [F3] and [F4] give $E O = Y_{1} d / Y$ .

1.2F1F5given

If $Y = 1$ , then $d \in {0, 1}$ and the failing subset is deterministic: $O = d Y_{1}$ . Its expectation is $d Y_{1} / Y$ and its variance is zero, as stipulated.

2.1F3F5F6givenalgebrastep 1.1

Suppose $Y > 1$ . For distinct group-1 subjects $a, b$ , if $d \geq 2$ the same subset count gives $P (I_{a} = I_{b} = 1) = (\binom{Y - 2}{d - 2}) / (\binom{Y}{d}) = d (d - 1) / (Y (Y - 1))$ ; for $d = 0$ or $d = 1$ the probability and the displayed ratio are both zero. Using [F5] and [F6], $Var (I_{a}) = \frac{d (Y - d)}{Y^{2}}, Cov (I_{a}, I_{b}) = - \frac{d (Y - d)}{Y^{2} (Y - 1)} .$ Thus [F3] and [F5] give $Var (O) = Y_{1} \frac{d (Y - d)}{Y^{2}} - Y_{1} (Y_{1} - 1) \frac{d (Y - d)}{Y^{2} (Y - 1)} = \frac{Y_{1} (Y - Y_{1}) d (Y - d)}{Y^{2} (Y - 1)} .$ Since $Y - Y_{1} = Y_{0}$ , this is the stated variance, including $d = 0$ , $d = Y$ , $Y_{1} = 0$ , and $Y_{1} = Y$ .

3.1A1F3F7step 1.1step 2.1algebrastep 1.2∎

In the sequential model, step 1.1 and the $Y_{j} = 0$ convention give $E [O_{j} - E_{j} ∣ H_{j - 1}] = 0$ , and step 2.1 gives conditional variance $V_{j}$ . Since $w_{j}$ is $H_{j - 1}$ -measurable, $D_{j}$ has conditional mean zero and conditional second moment $w_{j}^{2} V_{j}$ . The stated integrability condition makes each $D_{j}$ square-integrable. If $k < j$ , the filtration property and the revelation convention make $D_{k}$ $H_{j - 1}$ -measurable, so $E [D_{k} D_{j}] = E [D_{k} E (D_{j} ∣ H_{j - 1})] = 0$ . Expanding the finite sum's variance therefore yields both sequential identities.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 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, STAT331 Unit 6: Logrank Test, PDF pp. 3-4 (standard reference, not scraped)
Michal Kulich, NMST531 Censored Data Analysis: Extended Course Notes, §5.3, PDF pp. 59-60 (standard reference, not scraped)