Cox proportional hazards model

DefinitionRisk set in survival analysis#✓fully proved

The risk set at the observed time of subject i: subjects still under observation, {l : T_l ≥ Tᵢ}.

noncomputable def riskSet (T : Fin n → ℝ) (i : Fin n) : Finset (Fin n) := {l | T i ≤ T l}

Used by 14

Used byConcavity of the Cox log partial likelihood · The Cox information at β = 0 is the Breslow information · The log-rank statistic is the Cox score at β = 0 · Derivative of the Cox score is minus the information · Derivative of the log partial likelihood is the Cox score · Cox log partial likelihood · Log of the Cox partial likelihood is the log partial likelihood · A subject belongs to its own risk set · Number at risk at a subject's time · Number of group-1 subjects at risk · Cox partial likelihood · Weighted mean of a covariate over a risk set · Risk sets are nonempty · Weighted variance of a covariate over a risk set

TheoremA subject belongs to its own risk set#✓fully proved

Subject i is in its own risk set.

theorem mem_riskSet (T : Fin n → ℝ) (i : Fin n) : i ∈ riskSet T i

Uses 1 · Used by 1

Statement usesRisk set in survival analysis

Used byRisk sets are nonempty

TheoremRisk sets are nonempty#✓fully proved

The risk set of subject i is nonempty.

theorem riskSet_nonempty (T : Fin n → ℝ) (i : Fin n) : (riskSet T i).Nonempty

Uses 2 · Used by 5

Statement usesRisk set in survival analysis

Proof usesA subject belongs to its own risk set

Used byConcavity of the Cox log partial likelihood · The Cox information at β = 0 is the Breslow information · Derivative of the Cox score is minus the information · Derivative of the log partial likelihood is the Cox score · Log of the Cox partial likelihood is the log partial likelihood

DefinitionCox partial likelihood#✓fully proved

Cox's partial likelihood ∏_{i : δᵢ} exp ⟪β, xᵢ⟫ / ∑_{l ∈ R(Tᵢ)} exp ⟪β, x_l⟫.

noncomputable def partialLikelihood (T : Fin n → ℝ) (δ : Fin n → Bool) (x : Fin n → Fin p → ℝ)
    (β : Fin p → ℝ) : ℝ :=
  ∏ i with δ i = true, exp (β ⬝ᵥ x i) / ∑ l ∈ riskSet T i, exp (β ⬝ᵥ x l)

Uses 1 · Used by 1

Statement usesRisk set in survival analysis

Used byLog of the Cox partial likelihood is the log partial likelihood

DefinitionCox log partial likelihood#✓fully proved

The log partial likelihood ∑_{i : δᵢ} (⟪β, xᵢ⟫ - log ∑_{l ∈ R(Tᵢ)} exp ⟪β, x_l⟫).

noncomputable def logPartialLikelihood (T : Fin n → ℝ) (δ : Fin n → Bool)
    (x : Fin n → Fin p → ℝ) (β : Fin p → ℝ) : ℝ :=
  ∑ i with δ i = true, (β ⬝ᵥ x i - log (∑ l ∈ riskSet T i, exp (β ⬝ᵥ x l)))

Uses 1 · Used by 3

Statement usesRisk set in survival analysis

Used byConcavity of the Cox log partial likelihood · Log of the Cox partial likelihood is the log partial likelihood · Log partial likelihood of a scalar covariate

TheoremLog of the Cox partial likelihood is the log partial likelihood#✓fully proved

The logarithm of the partial likelihood is the log partial likelihood.

theorem log_partialLikelihood (T : Fin n → ℝ) (δ : Fin n → Bool) (x : Fin n → Fin p → ℝ)
    (β : Fin p → ℝ) : log (partialLikelihood T δ x β) = logPartialLikelihood T δ x β

Uses 4

Statement usesCox log partial likelihood · Cox partial likelihood

Proof usesRisk set in survival analysis · Risk sets are nonempty

TheoremConcavity of the Cox log partial likelihood#✓fully proved

Concavity of the Cox log partial likelihood on ℝᵖ.

theorem concaveOn_logPartialLikelihood (T : Fin n → ℝ) (δ : Fin n → Bool)
    (x : Fin n → Fin p → ℝ) : ConcaveOn ℝ Set.univ (logPartialLikelihood T δ x)

Uses 3

Statement usesCox log partial likelihood

Proof usesRisk set in survival analysis · Risk sets are nonempty

DefinitionWeighted mean of a covariate over a risk set#✓fully proved

The exp (b z)-weighted mean of a scalar covariate z over the risk set of subject i.

noncomputable def riskMean (T : Fin n → ℝ) (z : Fin n → ℝ) (b : ℝ) (i : Fin n) : ℝ :=
  (∑ l ∈ riskSet T i, z l * exp (b * z l)) / ∑ l ∈ riskSet T i, exp (b * z l)

Uses 1 · Used by 6

Statement usesRisk set in survival analysis

Used byThe Cox information at β = 0 is the Breslow information · Cox score for a scalar covariate · The log-rank statistic is the Cox score at β = 0 · Derivative of the Cox score is minus the information · Derivative of the log partial likelihood is the Cox score · Weighted variance of a covariate over a risk set

DefinitionWeighted variance of a covariate over a risk set#✓fully proved

The exp (b z)-weighted variance of a scalar covariate over the risk set of subject i.

noncomputable def riskVar (T : Fin n → ℝ) (z : Fin n → ℝ) (b : ℝ) (i : Fin n) : ℝ :=
  (∑ l ∈ riskSet T i, z l ^ 2 * exp (b * z l)) / (∑ l ∈ riskSet T i, exp (b * z l)) -
    riskMean T z b i ^ 2

Uses 2 · Used by 3

Statement usesWeighted mean of a covariate over a risk set · Risk set in survival analysis

Used byCox observed information for a scalar covariate · The Cox information at β = 0 is the Breslow information · Derivative of the Cox score is minus the information

DefinitionCox score for a scalar covariate#✓fully proved

The Cox score for a scalar covariate: ∑_{i : δᵢ} (zᵢ - z̄ᵢ(b)).

noncomputable def coxScore (T : Fin n → ℝ) (δ : Fin n → Bool) (z : Fin n → ℝ) (b : ℝ) : ℝ :=
  ∑ i with δ i = true, (z i - riskMean T z b i)

Uses 1 · Used by 3

Statement usesWeighted mean of a covariate over a risk set

Used byThe log-rank statistic is the Cox score at β = 0 · Derivative of the Cox score is minus the information · Derivative of the log partial likelihood is the Cox score

DefinitionCox observed information for a scalar covariate#✓fully proved

The Cox observed information for a scalar covariate: ∑_{i : δᵢ} Varᵢ(b).

noncomputable def coxInformation (T : Fin n → ℝ) (δ : Fin n → Bool) (z : Fin n → ℝ) (b : ℝ) :
    ℝ :=
  ∑ i with δ i = true, riskVar T z b i

Uses 1 · Used by 2

Statement usesWeighted variance of a covariate over a risk set

Used byThe Cox information at β = 0 is the Breslow information · Derivative of the Cox score is minus the information

DefinitionLog partial likelihood of a scalar covariate#✓fully proved

The log partial likelihood of a scalar covariate z as a function of b ∈ ℝ.

noncomputable def logPartialLikelihood₁ (T : Fin n → ℝ) (δ : Fin n → Bool) (z : Fin n → ℝ)
    (b : ℝ) : ℝ :=
  logPartialLikelihood T δ (fun i _ => z i) (fun _ : Fin 1 => b)

Uses 1 · Used by 1

Statement usesCox log partial likelihood

Used byDerivative of the log partial likelihood is the Cox score

TheoremDerivative of the log partial likelihood is the Cox score#✓fully proved

The derivative of the scalar log partial likelihood is the Cox score.

theorem hasDerivAt_logPartialLikelihood (T : Fin n → ℝ) (δ : Fin n → Bool) (z : Fin n → ℝ)
    (b : ℝ) : HasDerivAt (logPartialLikelihood₁ T δ z) (coxScore T δ z b) b

Uses 5

Statement usesCox score for a scalar covariate · Log partial likelihood of a scalar covariate

Proof usesWeighted mean of a covariate over a risk set · Risk set in survival analysis · Risk sets are nonempty

TheoremDerivative of the Cox score is minus the information#✓fully proved

The derivative of the Cox score is minus the observed information.

theorem hasDerivAt_coxScore (T : Fin n → ℝ) (δ : Fin n → Bool) (z : Fin n → ℝ) (b : ℝ) :
    HasDerivAt (coxScore T δ z) (-coxInformation T δ z b) b

Uses 6

Statement usesCox observed information for a scalar covariate · Cox score for a scalar covariate

Proof usesWeighted mean of a covariate over a risk set · Risk set in survival analysis · Risk sets are nonempty · Weighted variance of a covariate over a risk set

DefinitionNumber at risk at a subject's time#✓fully proved

The number at risk at the time of subject i.

noncomputable def numAtRisk (T : Fin n → ℝ) (i : Fin n) : ℕ := #(riskSet T i)

Uses 1 · Used by 4

Statement usesRisk set in survival analysis

Used byBreslow information · The Cox information at β = 0 is the Breslow information · The log-rank statistic is the Cox score at β = 0 · Log-rank numerator: observed minus expected events

DefinitionNumber of group-1 subjects at risk#✓fully proved

The number of group-1 subjects at risk at the time of subject i.

noncomputable def numAtRiskIn (T : Fin n → ℝ) (g : Fin n → Bool) (i : Fin n) : ℕ :=
  #{l ∈ riskSet T i | g l = true}

Uses 1 · Used by 4

Statement usesRisk set in survival analysis

Used byBreslow information · The Cox information at β = 0 is the Breslow information · The log-rank statistic is the Cox score at β = 0 · Log-rank numerator: observed minus expected events

DefinitionGroup indicator covariate#✓fully proved

The group indicator zᵢ = 1 for group 1 (g i = true) and 0 otherwise.

def groupIndicator (g : Fin n → Bool) (i : Fin n) : ℝ := if g i = true then 1 else 0

Used by 3

Used byThe Cox information at β = 0 is the Breslow information · The log-rank statistic is the Cox score at β = 0 · Log-rank numerator: observed minus expected events

DefinitionLog-rank numerator: observed minus expected events#✓fully proved

The log-rank numerator O - E: observed minus expected group-1 events, ∑_{i : δᵢ} (zᵢ - n₁(Tᵢ) / n(Tᵢ)).

noncomputable def observedMinusExpected (T : Fin n → ℝ) (δ : Fin n → Bool) (g : Fin n → Bool) :
    ℝ :=
  ∑ i with δ i = true, (groupIndicator g i - (numAtRiskIn T g i : ℝ) / numAtRisk T i)

Uses 3 · Used by 1

Statement usesGroup indicator covariate · Number at risk at a subject's time · Number of group-1 subjects at risk

Used byThe log-rank statistic is the Cox score at β = 0

DefinitionBreslow information#✓fully proved

The Breslow (Cox) information ∑_{i : δᵢ} n₁ n₀ / n² at the risk sets of the events. This is -ℓ''(0) for a group indicator, not the tied log-rank variance: for one tied risk set with n = 4, n₁ = 2 and d = 2 events it gives 1 / 2, while the hypergeometric log-rank variance is 1 / 3. It equals the log-rank variance only when the event times are distinct (so each risk set contributes at most one event).

noncomputable def breslowInformation (T : Fin n → ℝ) (δ : Fin n → Bool) (g : Fin n → Bool) :
    ℝ :=
  ∑ i with δ i = true,
    (numAtRiskIn T g i : ℝ) * ((numAtRisk T i : ℝ) - numAtRiskIn T g i) / (numAtRisk T i) ^ 2

Uses 2 · Used by 1

Statement usesNumber at risk at a subject's time · Number of group-1 subjects at risk

Used byThe Cox information at β = 0 is the Breslow information

TheoremThe log-rank statistic is the Cox score at β = 0#✓fully proved

ℓ'(0) = O - E.

theorem coxScore_zero (T : Fin n → ℝ) (δ : Fin n → Bool) (g : Fin n → Bool) :
    coxScore T δ (groupIndicator g) 0 = observedMinusExpected T δ g

Uses 7

Statement usesCox score for a scalar covariate · Group indicator covariate · Log-rank numerator: observed minus expected events

Proof usesNumber at risk at a subject's time · Number of group-1 subjects at risk · Weighted mean of a covariate over a risk set · Risk set in survival analysis

TheoremThe Cox information at β = 0 is the Breslow information#✓fully proved

The Cox information at β = 0 is the Breslow information ∑ n₁ n₀ / n² (not the tied log-rank variance; see breslowInformation).

theorem coxInformation_zero (T : Fin n → ℝ) (δ : Fin n → Bool) (g : Fin n → Bool) :
    coxInformation T δ (groupIndicator g) 0 = breslowInformation T δ g

Uses 9

Statement usesBreslow information · Cox observed information for a scalar covariate · Group indicator covariate

Proof usesNumber at risk at a subject's time · Number of group-1 subjects at risk · Weighted mean of a covariate over a risk set · Risk set in survival analysis · Risk sets are nonempty · Weighted variance of a covariate over a risk set

21 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.