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.

Terminal normal limit for weighted logrank scores

Statement

Assume the Axiom of Choice. For $g \in {0, 1}$ , let $(T_{g i}, C_{g i})_{i \geq 1}$ be IID within group, with $T_{g i}, C_{g i} \in [0, \infty)$ almost surely and the two group families independent. Assume conditional independent censoring $T_{g i} ⊥ C_{g i} ∣ g$ , and a common absolutely continuous event-time law with hazard density $λ$ on $[0, τ]$ , where $Λ (τ) = \int_{0}^{τ} λ (t) d t < \infty$ . Censoring distributions may differ between groups. Use the horizon-truncated record $U_{g i} : = \min (T_{g i}, C_{g i}, τ)$ and $δ_{g i} : = 1 {T_{g i} \leq C_{g i}, T_{g i} \leq τ}$ , which lies in $[0, τ] \times {0, 1}$ as required by Two-group logrank and weighted logrank scores.

For deterministic positive sample sizes $n_{g}$ along a sequence with $n = n_{0} + n_{1} \to \infty$ and $n_{1} / n \to ρ \in (0, 1)$ , set $ρ_{1} = ρ$ , $ρ_{0} = 1 - ρ$ , $y_{g} (t) = ρ_{g} P (U_{g 1} \geq t)$ , $y (t) = y_{0} (t) + y_{1} (t)$ , and $\overset{ˉ}{z} (t) = y_{1} (t) / y (t)$ . Assume $\inf_{t \leq τ} y (t) > 0$ . For each subject define $N_{g i} (t) = 1 {U_{g i} \leq t, δ_{g i} = 1}$ and $Y_{g i} (t) = 1 {U_{g i} \geq t}$ . Under one common filtration, assume $Y_{g i}$ is predictable and, separately, that $A_{g i} (t) = \int_{0}^{t} Y_{g i} (s) λ (s) d s, M_{g i} = N_{g i} - A_{g i}$ satisfies the finite-horizon square-integrable martingale contract of Simple counting-process intensity and compensator contract. Assume no two subjects have simultaneous event jumps. Conditional independent censoring and the displayed hazard are scientific model premises; they are not used as substitutes for the explicit martingale contract.

Use $U_{n, w_{n}}$ and ${\hat{V}}_{n, w_{n}}$ as defined in Two-group logrank and weighted logrank scores. Let $w_{n}$ be a common predictable weight sequence with $∣ w_{n} ∣ \leq C$ and a measurable supremum satisfying $\sup_{t \leq τ} ∣ w_{n} (t) - w (t) ∣ \to_{P} 0$ for a deterministic bounded Borel predictable weight $w$ . Define $σ_{w}^{2} : = \int_{0}^{τ} w (t)^{2} \frac{y_{0} (t) y_{1} (t)}{y_{0} (t) + y_{1} (t)} λ (t) d t .$ Then $\frac{U_{n, w_{n}}}{\sqrt{n}} \Rightarrow N (0, σ_{w}^{2}) .$ If $σ_{w}^{2} > 0$ , define the standardized statistic as $U_{n, w_{n}} / \sqrt{{\hat{V}}_{n, w_{n}}}$ when the denominator is positive and assign any fixed finite value on the event that it is zero. Every such extension converges to $N (0, 1)$ . If $σ_{w}^{2} = 0$ , only the degenerate score limit is asserted. For a fixed deterministic weight, take $w_{n} = w$ . This is a terminal finite-dimensional limit; it asserts no process central limit theorem.

Facts & Assumptions

Given: Assume AC; two independent IID groups of subject records, deterministic allocation fractions tending to $ρ_{g} \in (0, 1)$ , equal continuous event hazard, group-conditional independent censoring, the explicit counting-process contracts and no-simultaneous-jump condition, positive pooled risk support, finite $Λ (τ)$ , and the bounded predictable weights in the Statement.

[A1]

Assume the Axiom of Choice (AC), inherited from the counting-process integral and independent-groups terminal-limit suppliers. (The Axiom of Choice)

[A2]

Since each $U_{g i}$ is the same measurable function of its within-group IID pair $(T_{g i}, C_{g i})$ , the observed times are IID within each group. The deterministic allocation limits and positive pooled-risk bound in the Statement therefore meet the hypotheses of Uniform convergence of the risk-set treatment fraction, which supplies the uniform risk-fraction limits required by [F4] and [F5].

[F1]

Identical distribution and IID families: within each group the subject records share one law and are mutually independent.

[F2]

Independent families of event classes: independence of the two subject families means every finite choice of events from distinct subjects has product probability.

[F3]

Two-group logrank and weighted logrank scores: $U_{n, w_{n}}$ and ${\hat{V}}_{n, w_{n}}$ are the weighted risk-set score and its plug-in variance sum.

[F4]

Weighted logrank score expansion under a common-hazard model: under its stated martingale, risk-fraction, no-simultaneous-jump, and weight hypotheses, $U_{n, w_{n}} / \sqrt{n} = n^{- 1 / 2} \sum_{g = 0}^{1} \sum_{i = 1}^{n_{g}} ϕ_{g} (U_{g i}, δ_{g i}) + o_{P} (1),$ where $ϕ_{g} = \int_{0}^{τ} w (t) (g - \overset{ˉ}{z} (t)) d M_{g i} (t)$ .

[F5]

Consistency of the weighted logrank variance estimate: ${\hat{V}}_{n, w_{n}} / n \to_{P} σ_{w}^{2}$ under its stated continuous-event and plug-in variance hypotheses.

[F6]

Independent-group terminal influence limit: for a fixed finite number of independent IID groups, centered square-integrable measurable group influences and a separately established terminal expansion imply a Gaussian limit with covariance $\sum_{g} ρ_{g}^{- 1} Σ_{g}$ .

[F7]

Simple counting-process intensity and compensator contract: $M_{g i} = N_{g i} - A_{g i}$ is a square-integrable martingale under the explicit model contract, and $A_{g i} = \int Y_{g i} λ$ .

[F8]

L² counting-process integral when the limit exists: predictable integrands of finite compensator energy have the stated $L^{2}$ counting-process integral when the approximating integrals converge.

[F9]

L² extension of the predictable counting-process integral: the integral is a square-integrable martingale and $E (\int H d M)^{2} = E \int H^{2} d A$ for finite-energy predictable $H$ .

[F10]

Covariance matrix of a finite-dimensional random vector: for a centered square-integrable scalar, its covariance is its second moment.

[F11]

Tonelli's theorem for nonnegative measurable functions on a sigma-finite product: a nonnegative measurable integrand may be integrated in either order on the product space.

[F12]

Expectations factor over finite products of independent random variables: expectations of products of finitely many independent integrable real random variables factor into the product of their expectations.

[F13]

Variance of a finite sum as the sum of all variances and covariances: the variance of a finite sum is the sum of its variances and pairwise covariance terms.

[F14]

Markov's inequality for random variables: for $X \geq 0$ and $a > 0$ , $P (X \geq a) \leq E [X] / a$ .

[F15]

Dominated convergence: pointwise convergence under one integrable majorant permits passage to the limit in the integral.

[F16]

Stochastic order and convergence notation for finite-dimensional random vectors: $X_{n} = O_{P} (1)$ means its tails are bounded in probability, and $X_{n} = o_{P} (1)$ means convergence in probability to zero.

[F17]

Standard normal and normal laws: $N (0, v)$ is the law of $\sqrt{v} Z$ for $Z \sim N (0, 1)$ , including $v = 0$ .

[F18]

Vector Slutsky theorem: weak convergence is preserved after adjoining a quantity converging in probability to a constant and applying a continuous map.

Proof

1.1A1F1F2F7F8F9given

Put $h_{g} (t) = w (t) (g - \overset{ˉ}{z} (t))$ . For a subject record $(u, δ)$ , define the real map $ϕ_{g} (u, δ) = 1 {δ = 1, u \leq τ} h_{g} (u) - \int_{0}^{u \land τ} h_{g} (t) λ (t) d t .$ The deterministic integrand is bounded and Borel, so its indefinite integral is Borel and this map is measurable. From the definitions of $N_{g i}$ , $Y_{g i}$ and $A_{g i}$ , this is exactly $\int_{0}^{τ} h_{g} (t) d M_{g i} (t)$ . Its energy is at most $∥ h_{g} ∥_{\infty}^{2} Λ (τ)$ ; [F8] and [F9] therefore make it square-integrable and centered. It is the same measurable function of each subject record within group $g$ , so [F1] makes the transformed records IID within group and [F2] makes the two groups independent.

2.1F9F11givenstep 1.1algebra

By [F9] and [F11], $E [ϕ_{g}^{2}] = \int_{0}^{τ} w (t)^{2} (g - \overset{ˉ}{z} (t))^{2} P (U_{g 1} \geq t) λ (t) d t .$ Multiplying by $ρ_{g}$ and summing over $g = 0, 1$ gives $\sum_{g = 0}^{1} ρ_{g} E [ϕ_{g}^{2}] = \int_{0}^{τ} w (t)^{2} {y_{1} (t) (1 - \overset{ˉ}{z} (t))^{2} + y_{0} (t) \overset{ˉ}{z} (t)^{2}} λ (t) d t = σ_{w}^{2},$ where the last equality follows by substituting $\overset{ˉ}{z} = y_{1} / (y_{0} + y_{1})$ . The integral is finite since $w$ is bounded, $0 \leq y_{g} \leq 1$ , and $Λ (τ) < \infty$ .

2.2F1F12F13F14F15F16step 1.1

Fix $ϵ > 0$ . Since $n_{g} \to \infty$ , the integrand $ϕ_{g}^{2} 1 {∣ ϕ_{g} ∣ > ϵ \sqrt{n_{g}}}$ tends pointwise to zero and is bounded by the integrable $ϕ_{g}^{2}$ . [F15] gives $n_{g} P (∣ ϕ_{g} ∣ > ϵ \sqrt{n_{g}}) \leq ϵ^{- 2} E [ϕ_{g}^{2} 1 {∣ ϕ_{g} ∣ > ϵ \sqrt{n_{g}}}] ⟶ 0.$ Thus each group satisfies the finite-variance no-large-jump condition. Also, for $S_{g, n} = n_{g}^{- 1 / 2} \sum_{i = 1}^{n_{g}} ϕ_{g} (U_{g i}, δ_{g i})$ , [F1] and [F12] make the cross covariances zero, and [F13] gives $E [S_{g, n}^{2}] = E [ϕ_{g}^{2}]$ . Applying [F14] to $S_{g, n}^{2}$ yields $P (∣ S_{g, n} ∣ > M) \leq E [ϕ_{g}^{2}] / M^{2}$ ; hence $S_{g, n} = O_{P} (1)$ by [F16].

3.1A2F3F4F6step 2.2algebra

By [A2], the risk-fraction hypotheses used by [F4] hold. Let ${\hat{θ}}_{n} = U_{n, w_{n}} / n$ and set $θ = 0$ . By [F4], $\sqrt{n} ({\hat{θ}}_{n} - θ) = n^{- 1 / 2} \sum_{g = 0}^{1} \sum_{i = 1}^{n_{g}} ϕ_{g} (U_{g i}, δ_{g i}) + o_{P} (1) .$ Set $ψ_{g} = ρ_{g} ϕ_{g}$ . The group-sum term in [F6] is $S_{n}^{*} = \sum_{g = 0}^{1} \sqrt{\frac{n}{n_{g}}} \frac{1}{\sqrt{n_{g}}} \sum_{i = 1}^{n_{g}} ψ_{g} (U_{g i}, δ_{g i}) .$ Its difference from $n^{- 1 / 2} \sum_{g, i} ϕ_{g} (U_{g i}, δ_{g i})$ equals $\sum_{g = 0}^{1} \sqrt{\frac{n}{n_{g}}} (ρ_{g} - \frac{n_{g}}{n}) S_{g, n} = o_{P} (1),$ because $S_{g, n} = O_{P} (1)$ by step 2.2, $n_{g} / n \to ρ_{g} > 0$ , and there are only two groups. Thus the expansion required by [F6] is established with centered group influences $ψ_{g}$ .

4.1A1F6F10step 1.1step 2.1step 3.1

Each $ψ_{g}$ is centered and square-integrable by step 1.1, and $Var (ψ_{g}) = ρ_{g}^{2} E [ϕ_{g}^{2}]$ by [F10]. The covariance in [F6] is therefore $\sum_{g = 0}^{1} ρ_{g}^{- 1} Var (ψ_{g}) = \sum_{g = 0}^{1} ρ_{g} E [ϕ_{g}^{2}] = σ_{w}^{2}$ by step 2.1. Applying [F6] to the proved expansion in step 3.1 yields $U_{n, w_{n}} / \sqrt{n} \Rightarrow N (0, σ_{w}^{2})$ .

5.1A2F5F17F18step 4.1∎

Suppose $σ_{w}^{2} > 0$ and put $V_{n} = {\hat{V}}_{n, w_{n}} / n$ . By [A2] and [F5], $V_{n} \to_{P} σ_{w}^{2}$ , so $P (V_{n} > σ_{w}^{2} / 2) \to 1$ . The function $(x, v) \mapsto x / \sqrt{\max (v, σ_{w}^{2} / 2)}$ is continuous everywhere. Apply [F18] and this map to the score limit and $V_{n}$ ; the result converges to $Z / σ_{w}$ for $Z \sim N (0, σ_{w}^{2})$ , which has law $N (0, 1)$ by [F17]. On ${V_{n} > σ_{w}^{2} / 2}$ this map equals the stated standardized statistic. Since the complement has probability tending to zero, changing the statistic there has no effect on weak convergence, including any fixed finite extension on the zero-denominator event. When $σ_{w}^{2} = 0$ , step 4.1 gives the degenerate score law and no standardized conclusion.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

90 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 13: Large Sample Theory for 2-Sample Tests, PDF pp. 1-12 (standard reference, not scraped)
Michal Kulich, NMST531 Censored Data Analysis: Extended Course Notes, §5.4, PDF pp. 61-62 (standard reference, not scraped)