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.
A vanishing density prevents a uniform linear spatial inverse bound
Example
Let for , for , and for . Its density on has no positive lower bound near zero. At target , the endpoint inverse is by convention; for each , the point has CDF residual but spatial error .
Facts & Assumptions
Given: The CDF and points in the Example.
A nonnegative real has a unique nonnegative square root whose square equals . Square roots exist: a unique with ; the positives are
For , a CDF residual at most yields the spatial bound if both points lie in the bracket, there, and almost everywhere. This is a sufficient condition for a linear bound. Certified bisection controls CDF residual, spatial error, and distribution error
Verification
For , [F1] gives and , so . If , then , contradicting ; hence and . Under the stated endpoint convention, the target is , so the residual is while the spatial error is .
The ratio is unbounded as : for any , take , so [F1] gives by comparing nonnegative squares, and the ratio exceeds . Thus no constant independent of gives for these points; their nonlinear error is exactly . The density has essential infimum on every with , so the sufficient positive-density condition in [F2] fails near zero. The endpoint computation uses the declared convention , independently of [F2]'s interior-target theorem.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
15 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
- Luc Devroye, Non-Uniform Random Variate Generation, Chapter II §2.2, numerical inversion (standard reference, not scraped)
- D. Pollard, A User's Guide to Measure Theoretic Probability, generalized inverse discussion (standard reference, not scraped)