Skip to content

Kaplan–Meier estimator

22 fully proved

Kaplan Meier

StructureGrouped right-censored survival data#✓fully proved

Right-censored survival data grouped at k distinct, increasing observation times: deaths j subjects die and censored j subjects are censored at time j.

structure CensoredData (k : ℕ) where
  /-- The distinct observation times, in increasing order. -/
  time : Fin k → ℝ
  /-- The observation times are strictly increasing. -/
  strictMono_time : StrictMono time
  /-- The number of observed deaths at each time. -/
  deaths : Fin k → ℕ
  /-- The number of subjects censored at each time. -/
  censored : Fin k → ℕ
Used by 21
Used byNumber at risk at an observation time · Deaths at a time are among those at risk · Kaplan–Meier factor · Kaplan–Meier factor is at most one · Kaplan–Meier factor is nonnegative · Kaplan–Meier jump at an observation time · Kaplan–Meier jumps are nonnegative · Kaplan–Meier measure · Kaplan–Meier measure is a probability measure · Mass of a set under the Kaplan–Meier measure · Survival function of the Kaplan–Meier measure · Kaplan–Meier survival estimate · Kaplan–Meier estimate without censoring is the empirical survival · Kaplan–Meier survival is positive at a censoring time · Kaplan–Meier mass after the last observation · Leftover Kaplan–Meier mass is nonnegative · Likelihood of right-censored data · Kaplan–Meier is the nonparametric MLE · Sample size of censored survival data · Self-consistency · Kaplan–Meier jumps and leftover mass sum to one

Censored Data

DefinitionSample size of censored survival data#✓fully proved

The number of subjects in the sample.

def size : ℕ := ∑ j, (D.deaths j + D.censored j)
Uses 1 · Used by 2
Statement usesGrouped right-censored survival data
Used byKaplan–Meier estimate without censoring is the empirical survival · Self-consistency

DefinitionNumber at risk at an observation time#✓fully proved

The number at risk at time j: subjects whose observation time is at least time j.

def atRisk (j : Fin k) : ℕ := ∑ l with j ≤ l, (D.deaths l + D.censored l)
Uses 1 · Used by 11
Statement usesGrouped right-censored survival data
Used byDeaths at a time are among those at risk · Kaplan–Meier factor · Kaplan–Meier factor is at most one · Kaplan–Meier factor is nonnegative · Kaplan–Meier jump at an observation time · Kaplan–Meier jumps are nonnegative · Survival function of the Kaplan–Meier measure · Kaplan–Meier survival is positive at a censoring time · Kaplan–Meier is the nonparametric MLE · Self-consistency · Kaplan–Meier jumps and leftover mass sum to one

DefinitionKaplan–Meier factor#✓fully proved

The Kaplan–Meier factor 1 - dⱼ / nⱼ at time j (it is 1 if nobody is at risk, where also dⱼ = 0).

noncomputable def kmFactor (j : Fin k) : ℝ := 1 - (D.deaths j : ℝ) / D.atRisk j
Uses 2 · Used by 12
Statement usesGrouped right-censored survival data · Number at risk at an observation time
Used byKaplan–Meier factor is at most one · Kaplan–Meier factor is nonnegative · Kaplan–Meier jump at an observation time · Kaplan–Meier jumps are nonnegative · Survival function of the Kaplan–Meier measure · Kaplan–Meier survival estimate · Kaplan–Meier survival is positive at a censoring time · Kaplan–Meier mass after the last observation · Leftover Kaplan–Meier mass is nonnegative · Kaplan–Meier is the nonparametric MLE · Self-consistency · Kaplan–Meier jumps and leftover mass sum to one

DefinitionKaplan–Meier survival estimate#✓fully proved

The Kaplan–Meier estimate Ŝ(t) = ∏_{tⱼ ≤ t} (1 - dⱼ / nⱼ) of the survival function.

noncomputable def kmSurvival (t : ℝ) : ℝ := ∏ j with D.time j ≤ t, D.kmFactor j
Uses 2 · Used by 5
Statement usesGrouped right-censored survival data · Kaplan–Meier factor
Used bySurvival function of the Kaplan–Meier measure · Kaplan–Meier estimate without censoring is the empirical survival · Kaplan–Meier survival is positive at a censoring time · Kaplan–Meier is the nonparametric MLE · Self-consistency

DefinitionKaplan–Meier jump at an observation time#✓fully proved

The Kaplan–Meier jump at time j: Ŝ(tⱼ₋) · dⱼ / nⱼ.

noncomputable def kmMass (j : Fin k) : ℝ :=
  (∏ l with l < j, D.kmFactor l) * ((D.deaths j : ℝ) / D.atRisk j)
Uses 3 · Used by 7
Statement usesGrouped right-censored survival data · Number at risk at an observation time · Kaplan–Meier factor
Used byKaplan–Meier jumps are nonnegative · Kaplan–Meier measure · Kaplan–Meier measure is a probability measure · Mass of a set under the Kaplan–Meier measure · Survival function of the Kaplan–Meier measure · Kaplan–Meier is the nonparametric MLE · Kaplan–Meier jumps and leftover mass sum to one

DefinitionKaplan–Meier mass after the last observation#✓fully proved

The Kaplan–Meier mass left after the last observation time, ∏ⱼ (1 - dⱼ / nⱼ).

noncomputable def kmTail : ℝ := ∏ j, D.kmFactor j
Uses 2 · Used by 7
Statement usesGrouped right-censored survival data · Kaplan–Meier factor
Used byKaplan–Meier measure · Kaplan–Meier measure is a probability measure · Mass of a set under the Kaplan–Meier measure · Survival function of the Kaplan–Meier measure · Leftover Kaplan–Meier mass is nonnegative · Kaplan–Meier is the nonparametric MLE · Kaplan–Meier jumps and leftover mass sum to one

DefinitionKaplan–Meier measure#✓fully proved

The Kaplan–Meier measure: the jumps kmMass j at time j and the leftover mass kmTail at a chosen point τ (taken after the last observation time).

noncomputable def kmMeasure (τ : ℝ) : Measure ℝ :=
  ∑ j, ENNReal.ofReal (D.kmMass j) • Measure.dirac (D.time j) +
    ENNReal.ofReal D.kmTail • Measure.dirac τ
Uses 3 · Used by 4
Statement usesGrouped right-censored survival data · Kaplan–Meier jump at an observation time · Kaplan–Meier mass after the last observation
Used byKaplan–Meier measure is a probability measure · Mass of a set under the Kaplan–Meier measure · Survival function of the Kaplan–Meier measure · Kaplan–Meier is the nonparametric MLE

DefinitionLikelihood of right-censored data#✓fully proved

The censored-data likelihood of a law μ of the survival time: ∏ⱼ μ{tⱼ}^{dⱼ} · μ(tⱼ, ∞)^{cⱼ}.

noncomputable def likelihood (μ : Measure ℝ) : ℝ :=
  ∏ j, μ.real {D.time j} ^ D.deaths j * μ.real (Set.Ioi (D.time j)) ^ D.censored j
Uses 1 · Used by 1
Statement usesGrouped right-censored survival data
Used byKaplan–Meier is the nonparametric MLE

TheoremDeaths at a time are among those at risk#✓fully proved

The deaths at a time are among those at risk.

theorem deaths_le_atRisk (j : Fin k) : D.deaths j ≤ D.atRisk j
Uses 2 · Used by 2
Statement usesGrouped right-censored survival data · Number at risk at an observation time
Used byKaplan–Meier factor is nonnegative · Self-consistency

TheoremKaplan–Meier factor is at most one#✓fully proved

The Kaplan–Meier factor is at most 1.

theorem kmFactor_le_one (j : Fin k) : D.kmFactor j ≤ 1
Uses 3
Statement usesGrouped right-censored survival data · Kaplan–Meier factor
Proof usesNumber at risk at an observation time

TheoremKaplan–Meier factor is nonnegative#✓fully proved

The Kaplan–Meier factor is non-negative.

theorem kmFactor_nonneg (j : Fin k) : 0 ≤ D.kmFactor j
Uses 4 · Used by 3
Statement usesGrouped right-censored survival data · Kaplan–Meier factor
Proof usesNumber at risk at an observation time · Deaths at a time are among those at risk
Used byKaplan–Meier jumps are nonnegative · Leftover Kaplan–Meier mass is nonnegative · Kaplan–Meier is the nonparametric MLE

TheoremKaplan–Meier jumps are nonnegative#✓fully proved

The Kaplan–Meier jumps are non-negative.

theorem kmMass_nonneg (j : Fin k) : 0 ≤ D.kmMass j
Uses 5 · Used by 1
Statement usesGrouped right-censored survival data · Kaplan–Meier jump at an observation time
Proof usesNumber at risk at an observation time · Kaplan–Meier factor · Kaplan–Meier factor is nonnegative
Used byMass of a set under the Kaplan–Meier measure

TheoremLeftover Kaplan–Meier mass is nonnegative#✓fully proved

The leftover Kaplan–Meier mass is non-negative.

theorem kmTail_nonneg : 0 ≤ D.kmTail
Uses 4 · Used by 1
Statement usesGrouped right-censored survival data · Kaplan–Meier mass after the last observation
Proof usesKaplan–Meier factor · Kaplan–Meier factor is nonnegative
Used byMass of a set under the Kaplan–Meier measure

TheoremKaplan–Meier jumps and leftover mass sum to one#✓fully proved

The Kaplan–Meier jumps and the leftover mass add up to 1.

theorem sum_kmMass_add_kmTail : ∑ j, D.kmMass j + D.kmTail = 1
Uses 5 · Used by 2
Statement usesGrouped right-censored survival data · Kaplan–Meier jump at an observation time · Kaplan–Meier mass after the last observation
Proof usesNumber at risk at an observation time · Kaplan–Meier factor
Used byKaplan–Meier measure is a probability measure · Survival function of the Kaplan–Meier measure

TheoremMass of a set under the Kaplan–Meier measure#✓fully proved

The mass of a measurable set under the Kaplan–Meier measure.

theorem kmMeasure_real_apply (τ : ℝ) {B : Set ℝ} (hB : MeasurableSet B) :
    (D.kmMeasure τ).real B =
      ∑ j, (if D.time j ∈ B then D.kmMass j else 0) + if τ ∈ B then D.kmTail else 0
Uses 6 · Used by 3
Statement usesGrouped right-censored survival data · Kaplan–Meier jump at an observation time · Kaplan–Meier measure · Kaplan–Meier mass after the last observation
Proof usesKaplan–Meier jumps are nonnegative · Leftover Kaplan–Meier mass is nonnegative
Used byKaplan–Meier measure is a probability measure · Survival function of the Kaplan–Meier measure · Kaplan–Meier is the nonparametric MLE

TheoremKaplan–Meier measure is a probability measure#✓fully proved

The Kaplan–Meier measure is a probability measure.

theorem kmMeasure_isProbabilityMeasure (τ : ℝ) : IsProbabilityMeasure (D.kmMeasure τ)
Uses 6
Statement usesGrouped right-censored survival data · Kaplan–Meier measure
Proof usesKaplan–Meier jump at an observation time · Mass of a set under the Kaplan–Meier measure · Kaplan–Meier mass after the last observation · Kaplan–Meier jumps and leftover mass sum to one

TheoremSurvival function of the Kaplan–Meier measure#✓fully proved

The survival function of the Kaplan–Meier measure is the Kaplan–Meier estimate on (-∞, τ): P(T > t) = Ŝ(t) for t < τ.

theorem kmMeasure_real_Ioi {τ : ℝ} {t : ℝ} (ht : t < τ) :
    (D.kmMeasure τ).real (Set.Ioi t) = D.kmSurvival t
Uses 9 · Used by 1
Statement usesGrouped right-censored survival data · Kaplan–Meier measure · Kaplan–Meier survival estimate
Proof usesNumber at risk at an observation time · Kaplan–Meier factor · Kaplan–Meier jump at an observation time · Mass of a set under the Kaplan–Meier measure · Kaplan–Meier mass after the last observation · Kaplan–Meier jumps and leftover mass sum to one
Used byKaplan–Meier is the nonparametric MLE

TheoremKaplan–Meier is the nonparametric MLE#✓fully proved

Kaplan–Meier is the nonparametric MLE (Kaplan–Meier 1958): every probability measure on ℝ has censored-data likelihood at most that of the Kaplan–Meier measure.

theorem likelihood_le_kmMeasure (μ : Measure ℝ) [IsProbabilityMeasure μ] {τ : ℝ}
    (hτ : ∀ j, D.time j < τ) : D.likelihood μ ≤ D.likelihood (D.kmMeasure τ)
Uses 11
Statement usesGrouped right-censored survival data · Kaplan–Meier measure · Likelihood of right-censored data
Proof usesNumber at risk at an observation time · Kaplan–Meier factor · Kaplan–Meier factor is nonnegative · Kaplan–Meier jump at an observation time · Survival function of the Kaplan–Meier measure · Mass of a set under the Kaplan–Meier measure · Kaplan–Meier survival estimate · Kaplan–Meier mass after the last observation

TheoremKaplan–Meier survival is positive at a censoring time#✓fully proved

A time at which some subject is censored has positive Kaplan–Meier survival.

theorem kmSurvival_pos_of_censored_pos {j : Fin k} (hj : 0 < D.censored j) :
    0 < D.kmSurvival (D.time j)
Uses 4 · Used by 1
Statement usesGrouped right-censored survival data · Kaplan–Meier survival estimate
Proof usesNumber at risk at an observation time · Kaplan–Meier factor
Used bySelf-consistency

TheoremSelf-consistency#✓fully proved

Self-consistency (Efron 1967, (7.4)): n Ŝ(t) is the number of observations exceeding t plus, for each subject censored at or before t, the conditional survival Ŝ(t) / Ŝ(tⱼ).

theorem size_mul_kmSurvival (t : ℝ) :
    (D.size : ℝ) * D.kmSurvival t =
      (∑ j with t < D.time j, ((D.deaths j : ℝ) + D.censored j)) +
        ∑ j with D.time j ≤ t,
          (D.censored j : ℝ) * (D.kmSurvival t / D.kmSurvival (D.time j))
Uses 7 · Used by 1
Statement usesGrouped right-censored survival data · Kaplan–Meier survival estimate · Sample size of censored survival data
Proof usesNumber at risk at an observation time · Deaths at a time are among those at risk · Kaplan–Meier factor · Kaplan–Meier survival is positive at a censoring time
Used byKaplan–Meier estimate without censoring is the empirical survival

TheoremKaplan–Meier estimate without censoring is the empirical survival#✓fully proved

Without censoring, the Kaplan–Meier estimate is the empirical survival function: the fraction #{observations > t} / n = 1 - Fₙ(t).

theorem kmSurvival_of_censored_eq_zero (hc : ∀ j, D.censored j = 0) (hn : 0 < D.size)
    (t : ℝ) : D.kmSurvival t = (∑ j with t < D.time j, (D.deaths j : ℝ)) / D.size
Uses 4
Statement usesGrouped right-censored survival data · Kaplan–Meier survival estimate · Sample size of censored survival data
Proof usesSelf-consistency

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.