TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

Exponential and Weibull survival specifications define probability laws

Statement

Assume Countable Choice. For $λ > 0$ , the density $f_{λ} (t) = {\begin{cases} λ e^{- λ t}, & t > 0, \\ 0, & t \leq 0 \end{cases}$ defines a probability law on $R$ with survival $S (t) = e^{- λ t}$ for $t \geq 0$ . For $k, η > 0$ , the density $f_{k, η} (t) = {\begin{cases} \frac{k}{η} (t / η)^{k - 1} e^{- (t / η)^{k}}, & t > 0, \\ 0, & t \leq 0 \end{cases}$ defines a probability law with survival $S (t) = e^{- (t / η)^{k}}$ for $t \geq 0$ . Each law is unique among probability laws on $[0, \infty)$ with that survival. The density hazards are respectively $λ$ and $\frac{k}{η} (t / η)^{k - 1}$ for $t > 0$ .

Facts & Assumptions

Given: Positive parameters $λ$ , $k$ , $η$ and Lebesgue measure $d t$ on $R$ .

[F1]

A nonnegative measurable function $f$ defines the measure $A \mapsto \int_{A} f (t) d t$ . The measure with density $f$ relative to $μ$

[F2]

For $t > 0$ , $(t / η)^{k}$ is differentiable with derivative $\frac{k}{η} (t / η)^{k - 1}$ ; $\exp^{'} = \exp$ and the chain rule holds. Continuity and derivatives of positive-base real powers, The exponential function is smooth and $(\exp)^{'} = \exp$ , The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , The exponential function is strictly increasing, The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$

[F3]

A positive derivative implies increase by the mean value theorem. The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$

[F4]

The positive-base power satisfies $x^{k} = e^{k \log x}$ , and $\log$ is increasing and unbounded in both directions. Real powers for positive bases, with the zero-base positive-exponent convention, The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, The integral logarithm is unbounded above and below

[F5]

$e^{x} \to + \infty$ as $x \to + \infty$ and $e^{x} \to 0$ as $x \to - \infty$ . The exponential tends to $+ \infty$ at $+ \infty$ and to $0$ at $- \infty$

[F6]

If $G^{'} = f$ on a compact interval and $f$ is Riemann integrable, then $\int_{a}^{b} f = G (b) - G (a)$ . The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$

[F7]

Continuous functions on a compact interval are Riemann integrable, and a bounded Riemann integrable function has the same Riemann and Lebesgue integrals under Countable Choice. A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral

[F8]

Increasing limits of nonnegative measurable functions pass through their Lebesgue integrals. Monotone convergence for the integral

[F9]

Under Countable Choice, a CDF determines a unique probability law. Cumulative distribution function of a real random variable, Probability laws correspond to distribution functions

[F10]

On the real line, Lebesgue measure is the restriction of Lebesgue outer measure to the Lebesgue-measurable sets, and under Countable Choice it is a measure on that sigma-algebra. Lebesgue measurable sets, the family $L (R^{n})$ , and the restricted set function $λ_{n}$ , Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume

[F11]

Open sets generate the Borel sigma-algebra, whose members are the Borel sets. The Borel sigma-algebra of a topological space

[F12]

Under Countable Choice, every Borel subset of the real line is Lebesgue measurable. Assuming countable choice, every Borel subset of $R^{n}$ is Lebesgue measurable

[A1]

Countable Choice is used in [F7] to identify Riemann and Lebesgue integrals, in [F9] to construct and identify the probability law, and in [F10] and [F12] for the measure and Borel-measurability properties of Lebesgue measure. The Axiom of Countable Choice ( ${A C}_{ω}$ )

Proof

technique · direct

1.1F2F3F4F5F11given

Define $F_{λ} (t) = 0$ for $t < 0$ and $F_{λ} (t) = 1 - e^{- λ t}$ for $t \geq 0$ ; define $F_{k, η} (t) = 0$ for $t < 0$ and $F_{k, η} (t) = 1 - e^{- (t / η)^{k}}$ for $t \geq 0$ . Both are continuous at $0$ by [F2], [F4], and [F5]. On $t > 0$ their derivatives are the displayed densities and are positive by [F2]. The piecewise densities are Borel measurable: on $(0, \infty)$ they are products of continuous functions, and on $(- \infty, 0]$ they vanish; both domains are Borel by [F11]. The mean value theorem in [F3] makes each increasing on $(0, \infty)$ . For $t > 0$ , both $a = λ t$ and $a = (t / η)^{k}$ are positive, so strict increase of the exponential gives $e^{- a} < e^{0} = 1$ ; hence both candidate CDFs are positive there; thus their value $0$ at $0$ is consistent with monotonicity. Their limits are $0$ at $- \infty$ and $1$ at $+ \infty$ , so each is a CDF on $R$ .

2.1A1F6F7F8F10step 1.1

Fix $0 < a < b$ . Each CDF is differentiable on $[a, b]$ with the continuous derivative $f$ from the Statement. By [F6] its Riemann integral is $F (b) - F (a)$ ; by [F7] this equals its Lebesgue integral with respect to the measure in [F10]. Letting $a = 1 / n ↓ 0$ for integers $n$ large enough that $1 / n < b$ , [F8] and continuity at $0$ give $\int_{(0, b]} f (u) d u = F (b) .$ This applies separately to the exponential and Weibull formulas.

3.1A1F1F8F9F10F12step 1.1step 2.1

For either displayed nonnegative density $f$ , [F1] defines the measure $ν_{f} = f d t$ on Lebesgue-measurable sets. By [F12], its restriction to Borel sets is a measure. Step 2.1 gives $ν_{f} ((0, t]) = F (t)$ for every $t > 0$ . Since $f = 0$ on $(- \infty, 0]$ , this part has $ν_{f}$ -measure zero, so $ν_{f} ((- \infty, t]) = F (t)$ ; for $t \leq 0$ both sides are $0$ . Also $ν_{f} (R) = \lim_{n \to \infty} ν_{f} ((- \infty, n]) = \lim_{n \to \infty} F (n) = 1$ by [F8] and step 1.1. Thus $ν_{f}$ is a probability law with CDF $F$ , and [F9] identifies it with the unique law specified by the survival formula. Consequently $f$ is the stated density.

4.1givenstep 3.1algebra

Dividing the exponential density by its positive survival gives hazard $λ$ . Dividing the Weibull density by its positive survival gives $\frac{k}{η} (t / η)^{k - 1}$ for $t > 0$ .

5.1step 1.1step 2.1step 3.1step 4.1∎

Steps 1.1, 2.1, 3.1, and 4.1 establish CDF validity, density-law existence, survival formulas, uniqueness, and the density hazards for both parameter families.

Depends on

Used by

Cited to discharge well-definedness by Parametric survival and reliability models.

Dependency tree · two levels

123 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

NIST/SEMATECH Engineering Statistics Handbook, Chapter 8, §§8.1.2.1, 8.1.6.1–8.1.6.2, PDF pp. 12–19 (standard reference, not scraped)
Lu Tian, STAT331 Unit 2: Likelihood Construction, Inference for Parametric Survival Distributions, §2.2, PDF pp. 5–7 (standard reference, not scraped)
Qiqing Yu, Survival Analysis (Lecture Notes), §2.2.1–2.2.2, PDF pp. 10–11 (standard reference, not scraped)