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.
The standard normal CDF is continuous and strictly increasing
Statement
Assume the Axiom of Choice. Let for . Then is continuous and strictly increasing on , with and .
Facts & Assumptions
Given: The Axiom of Choice and the standard normal law.
The Axiom of Choice is assumed in the current definition of the standard normal law. The Axiom of Choice
The standard normal law has density and total mass one. Standard normal and normal laws
The real exponential function is smooth, so the displayed normal density is continuous. The exponential function is smooth and
A continuous real-valued function on a nonempty compact subset of attains finite maximum and minimum values. Extreme value theorem: a continuous real function on a nonempty compact subset of attains a greatest and a least value
Measures are continuous along increasing sequences of measurable sets. Continuity from below for measures
A measure finite on one set of a decreasing sequence is continuous along that sequence. Continuity from above when one set has finite measure
Proof
The density in [F1] is positive and continuous by [F2]. Fix . By [F3], attains a minimum on ; since is positive at every point, . The density formula and additivity over give , so is strictly increasing.
Fix . By [F3], is bounded by some finite on the compact interval . If , then by integrating the density over the interval between and . Letting proves continuity at , and was arbitrary.
The sets increase to , so [F4] and the total mass in [F1] give . The sets decrease to the empty set and have finite measure, so [F5] gives . Monotonicity from step 1.1 then gives the two stated limits at infinity.
Depends on
- The Axiom of Choice
- Standard normal and normal laws
- The exponential function is smooth and $(\exp)'=\exp$
- Extreme value theorem: a continuous real function on a nonempty compact subset of $\mathbb{R}$ attains a greatest and a least value
- Continuity from below for measures
- Continuity from above when one set has finite measure
Used by
- Bias-corrected and accelerated bootstrap interval Algorithm
- Bias-corrected bootstrap interval Algorithm
- The IID bootstrap can fail at the kink of the absolute mean Counterexample
- Blom rank-normal scores for pooled draws Definition
- Heavy tails and a location shift in split R-hat Example
- Selective inference after choosing the larger of two means Example
- Conditional quantile couplings for Gaussian anchored sums Lemma
- Conditional IID bootstrap CLT for an empirical law Theorem
- Finite-dimensional Gaussian isoperimetric expansion Theorem
- First-order IID bootstrap validity for smooth functions of a mean Theorem
- The truncated normal selective pivot is conditionally uniform Theorem
Dependency tree · two levels
39 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
- Jason D. Lee, Dennis L. Sun, Yuekai Sun, and Jonathan E. Taylor, Exact Post-Selection Inference, with Application to the Lasso (standard reference, not scraped)
- Daniel García Rasines, LTCC Week 3: Selective Inference (standard reference, not scraped)