Alphabeta MathHow 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 positive-variance normal law has its location-scale density
Statement
Assume AC. For and , the normal law of Standard normal and normal laws has Lebesgue density
Facts & Assumptions
Given: AC, the standard-normal probability law and its specified density, and , .
is the pushforward of by , and has density . Standard normal and normal laws, The standard normal density has total mass one
AC implies Countable Choice. AC implies DC implies countable choice, The Axiom of Countable Choice ()
Under Countable Choice, a diffeomorphism transforms nonnegative Lebesgue integrals by its absolute Jacobian. A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions
AC holds; it is used in [F1] and implies the Countable Choice hypothesis of [F3]. The Axiom of Choice
Proof
Given: The hypotheses in the Statement.
By [A1] and [F2], Countable Choice holds, so the change-of-variables theorem [F3] applies. For , the map is a diffeomorphism of with derivative .
For any Borel set , apply [F3] to the nonnegative Borel function . The change of variables gives , where the last equality is the pushforward identity in [F1]. Therefore the displayed function is a density on every Borel set, proving the statement.
Depends on
Used by
- Gaussian mean-field reverse KL underestimates correlated marginal variance Counterexample
- A diffuse normal prior changes the point-null Bayes factor Example
- A negative balanced-ANOVA moment estimate Example
- An improper flat-prior scale makes a formal evidence arbitrary Example
- An improper variance hyperprior can give an improper posterior Example
- Gaussian mixture likelihood is unbounded under covariance collapse Example
- Gaussian reparameterization gives two gradient estimators Example
- Integrating hyperparameter uncertainty versus plugging in Example
- Compactly supported Gaussian mixtures admit logarithmic-size finite approximations Lemma
- Gaussian convolution has second-order KL and log-square error Lemma
- Hellinger entropy for compact-location normal mixtures in a scale band Lemma
- Interval masses give a log-free local KL neighborhood for the mixture prior Lemma
- The Dirichlet normal-mixture density is jointly measurable and normalized Lemma
- The mixture prior places local KL and log-square mass near a compact smooth truth Lemma
- The posterior excludes large scales and mixing mass far from compact data Lemma
- Known-variance Normal-Normal conjugate update Theorem
Dependency tree · two levels
37 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
- Andrew Gelman, John B. Carlin, Hal S. Stern, David B. Dunson, Aki Vehtari, and Donald B. Rubin, Bayesian Data Analysis, 3rd ed., §5.4 (standard reference, not scraped)
- Alicia A. Johnson, Miles Q. Ott, and Mine Dogucu, Bayes Rules!, Chapter 16, §16.3 (standard reference, not scraped)