LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck pass

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.

CDF ordering and uniform error control quantile coverage

Statement

For a cumulative distribution function $F$ and $u \in (0, 1)$ , define the generalized quantile $q_{F} (u) : = \inf {x \in R : F (x) \geq u}$ , and put $q_{F} (0) : = - \infty$ and $q_{F} (1) : = + \infty$ . Let $X$ be a real random variable with CDF $F$ . In part 3, a random CDF $\hat{G}$ means that each $\hat{G} (x)$ is measurable and, for every outcome, $x \mapsto \hat{G} (x)$ is a right-continuous CDF. If the initial paths are CDFs only outside a specified measurable null set $N$ , first set $\hat{G} (x) = 1_{{x \geq 0}}$ on $N$ ; all suprema and quantiles in part 3 use this everywhere-CDF version. No completeness of the probability space is assumed. For $ε, δ \geq 0$ and $0 \leq α_{1}, α_{2} < 1$ with $α_{1} + α_{2} < 1$ , the following hold.

If $G$ is a CDF and $\sup_{x} (G (x) - F (x)) \leq ε$ , then $P {X \leq q_{G} (1 - α_{2})} \geq 1 - α_{2} - ε$ .
If $G$ is a CDF and $\sup_{x} (F (x) - G (x)) \leq ε$ , then $P {X \geq q_{G} (α_{1})} \geq 1 - α_{1} - ε$ .
If $\hat{G}$ is a random CDF and $P {\sup_{x} ∣ \hat{G} (x) - F (x) ∣ \leq ε / 2} \geq 1 - δ$ , then $P {q_{\hat{G}} (α_{1}) \leq X \leq q_{\hat{G}} (1 - α_{2})} \geq 1 - α_{1} - α_{2} - ε - δ .$

The endpoints $α_{i} = 0$ use the extended quantiles and make the corresponding tail event vacuous. No continuity of $F$ or absence of atoms at the target quantiles is required.

Facts & Assumptions

Given: CDFs $F, G$ , a real random variable $X$ with CDF $F$ , the stated tail-levels, and, in part 3, a random CDF $\hat{G}$ with measurable evaluations, right-continuous sample paths, and its uniform error event.

[F1]

Cumulative distribution function of a real random variable: The CDF of a real random variable is $F_{X} (x) = P (X \leq x)$ .

[F2]

Continuity from above when one set has finite measure: For decreasing measurable sets whose first set has finite measure, the measure of their intersection is the infimum of their measures.

[F3]

Continuity from below for measures: For increasing measurable sets, the measure of their union is the supremum of their measures.

Proof

Given: The objects and hypotheses in the statement.

1.1F1F2F3givenalgebra

For $u \in (0, 1)$ the quantile set ${x : F (x) \geq u}$ is nonempty and bounded below because the events ${X \leq k}$ increase to the whole space and ${X \leq - k}$ decrease to the empty set; [F2]–[F3] give the CDF limits $1$ and $0$ at the two tails. If $q = q_{F} (u)$ , then for every $r > 0$ there is $x < q + r$ with $F (x) \geq u$ , so $F (q + r) \geq u$ . The events ${X \leq q + 1 / k}$ decrease to ${X \leq q}$ ; by [F2], $F (q) = \lim_{k} F (q + 1 / k) \geq u$ . Also, for every $x < q$ , $F (x) < u$ by the definition of infimum.

2.1F1step 1.1givenalgebra

If $α_{2} = 0$ , the event is vacuous because $q_{G} (1) = + \infty$ . Otherwise, if $1 - α_{2} - ε \leq 0$ , the lower bound is nonpositive and is trivial. In the remaining case, every $x$ with $G (x) \geq 1 - α_{2}$ satisfies $F (x) \geq 1 - α_{2} - ε$ , so $q_{F} (1 - α_{2} - ε) \leq q_{G} (1 - α_{2})$ . Step 1.1 gives $F (q_{F} (1 - α_{2} - ε)) \geq 1 - α_{2} - ε$ , and monotonicity of $F$ proves the first probability bound.

2.2F1F3step 1.1givenalgebra

If $α_{1} = 0$ , the event is vacuous because $q_{G} (0) = - \infty$ . If $α_{1} + ε \geq 1$ , the lower bound is nonpositive and is trivial. Otherwise, each $x$ with $F (x) \geq α_{1} + ε$ has $G (x) \geq α_{1}$ , whence $q_{G} (α_{1}) \leq q_{F} (α_{1} + ε)$ . For every $y < q_{F} (α_{1} + ε)$ , step 1.1 gives $F (y) < α_{1} + ε$ . The events ${X \leq q_{F} (α_{1} + ε) - 1 / k}$ increase to ${X < q_{F} (α_{1} + ε)}$ ; [F3] therefore gives $P {X < q_{F} (α_{1} + ε)} \leq α_{1} + ε$ . This proves the second bound.

3.1F1step 1.1step 2.2givenalgebra∎

The stated replacement on $N$ preserves measurable evaluations and gives CDF paths everywhere. For $u \in (0, 1)$ , $q_{\hat{G}} (u)$ is measurable because ${q_{\hat{G}} (u) < a} = ⋃_{r \in Q, r < a} {\hat{G} (r) \geq u}$ ; the endpoint quantiles are constant, so the coverage event is measurable. Also $E : = {\sup_{x} ∣ \hat{G} (x) - F (x) ∣ \leq ε / 2}$ is measurable because $∣ \hat{G} - F ∣$ is right-continuous for every outcome and its supremum over $R$ equals its supremum over $Q$ . If $α_{1} + α_{2} + ε + δ \geq 1$ , part 3 is the trivial nonnegative lower bound. Otherwise, on $E$ , when $α_{1} > 0$ the pointwise order implies $q_{\hat{G}} (α_{1}) \leq q_{F} (α_{1} + ε / 2)$ ; hence the lower-tail failure on $E$ is contained in ${X < q_{F} (α_{1} + ε / 2)}$ and has probability at most $α_{1} + ε / 2$ by step 2.2. If $α_{1} = 0$ , this tail is empty. Similarly, when $α_{2} > 0$ , $q_{F} (1 - α_{2} - ε / 2) \leq q_{\hat{G}} (1 - α_{2})$ ; hence the upper-tail failure on $E$ is contained in ${X > q_{F} (1 - α_{2} - ε / 2)}$ , whose probability is at most $α_{2} + ε / 2$ by step 1.1. If $α_{2} = 0$ , that tail is empty. A union bound and $P (E^{c}) \leq δ$ give the claimed coverage bound; no independence between $E$ and $X$ is needed because each intersection with $E$ is bounded by the corresponding unconditional tail event.

Depends on

Used by

Dependency tree · two levels

8 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

J. P. Romano and A. M. Shaikh, On the Uniform Asymptotic Validity of Subsampling and the Bootstrap, Appendix A.1, Lemma A.1 (standard reference, not scraped)