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.
Function-space pCN and invariant posterior kernels — Examples and Counterexamples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Algebraic Closure, Embeddings, and Separability
- Algebraic Extensions, Extension Degree, and Finite Fields
- Areas of Elementary Plane Figures
- Banach Gaussian priors, RKHS support, and concentration
- Banach Valued Integration and the Radon Nikodym Property
- Bayesian models, priors, and posterior laws
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Brownian Motion Construction and Continuity
- Central Limit Theorems
- Characteristic Functions Inversion and Continuity
- Compactness
- Compactness in Metric Spaces
- Complete Metrizability, Čech-Completeness, and Baire Category
- Completeness, Completion, and Uniform Continuity
- Complex Lp Spaces and Test-Function Conventions
- Complex Norms and Realification
- Complexification, Realification and Real Structures
- Composition Series, the Jordan–Hölder Theorem and Solvable Groups
- Conditional Distributions and Regular Conditional Probability
- Conditional Expectation
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Conjugate families and Gaussian conditioning
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Convergence: Nets and Filters
- Cosets, Index and Lagrange's Theorem
- Cost-Constrained, Gaussian, and Feedback Channels
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Cyclic Groups and Direct Products
- Density Separability and Convolution in Lᵖ
- Detection and quantification limits
- Determinants of Matrices over a Commutative Ring
- Diagonalisation and the Minimal Polynomial
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Domination and Likelihood Ratios
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Eigenvalues, Eigenvectors and the Characteristic Polynomial
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite Probability and the Probabilistic Method
- Finite Probability Spaces and Random Variables
- Finite-window spatial likelihood
- Foundations of the Real Numbers for Analysis
- Fourier Transform Convolution and Approximate Identities
- Fubini and Change of Variables
- Function-space pCN and invariant posterior kernels
- Function-space priors and sample regularity
- Fundamental Trigonometric Identities
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- General-state Markov kernels, invariance, and reversibility
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Hausdorff via the Diagonal
- Hilbert Space Geometry and Riesz Representation
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Improper and Parameter-Dependent Multiple Integrals
- Improper Integrals
- Independence Borel Cantelli and Zero One Laws
- Infinite Product Measures and Kolmogorov Extension
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Inverse maps, identifiability, and stability
- Lebesgue Measure on Euclidean Space
- Lebesgue-Stieltjes Measures and Distribution Functions
- Likelihood potentials and posterior propriety
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Loss, Risk and Decision Theory
- Markov Kernels and Markov Chains
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Measurable Functions and Simple Approximation
- Measures and Their Basic Properties
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Modes of Convergence Egorov and Lusin
- Modes of Convergence for Random Variables
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Norming and Separation under Hahn–Banach
- Order, Zorn's Lemma, and the Axiom of Choice
- Orthonormal Bases, Parseval and Fourier Series
- Outer Measure and the Caratheodory Extension Theorem
- Partitions of Unity and Paracompactness
- Pointwise Extended-Real Function Products
- Polynomial Rings, the Division Algorithm and Roots
- Posterior propriety and dominated Bayes formula
- Power Series and Real-Analytic Functions
- Primes, Euclid's Lemma and the Fundamental Theorem of Arithmetic
- Probability Spaces Random Variables and Expectation
- Product Measures and the Fubini Tonelli Theorems
- Properties of the Integral and the Working FTC
- Radon Measures and the Riesz Markov Kakutani Theorem
- Recurrence Transience and Hitting Times for Markov Chains
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Sigma Algebras and Borel Sets
- Signed and Complex Measures Hahn and Jordan
- Simple Field Extensions and the Construction of the Complex Numbers
- Sine, Cosine, and the Definition of Pi
- Spectral regularization and parameter choice
- Splitting Fields
- Standard-Borel Real Codings and Determining Classes
- State-space model laws
- Stationary Markov Chains and Ergodic Limits
- Statistical Experiments, Models and Identifiability
- Strong Laws of Large Numbers
- Subspaces, Products, and Quotients
- Suprema and Infima
- Sylow's Theorems, p-Groups and Nilpotent Groups
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- The Analytic Hahn Banach Theorem
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Exponential Function
- The Fundamental Theorem of Algebra
- The Fundamental Theorem of Finite Abelian Groups
- The Galois Correspondence
- The Inverse and Implicit Function Theorems
- The Lebesgue and Riemann Integrals Compared
- The Lebesgue Integral and the Convergence Theorems
- The Logarithm and General Powers
- The Lᵖ Spaces Holder Minkowski and Riesz Fischer
- The Maximal Function and Lebesgue Differentiation
- The Radon Nikodym Theorem and Lebesgue Decomposition
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Spectral Theorem, Positive Operators and Singular Value Decomposition
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Urysohn's Lemma and the Tietze Extension Theorem
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Weak Convergence Tightness and Representation
- Weak Laws and Series of Independent Random Variables
- Weak nonparametric Bernstein–von Mises limits
2 · Logical flowchart
3 · Definitions, theorems and proofs
None yet.
4 · Examples, counterexamples and false statements
Infinite-dimensional Gaussian random-walk reverse flow is singular
Statement refuted
Assume the Axiom of Choice and fix . Let with its complete coordinate basis positively indexed as , where has its nonzero coordinate at . Write for coefficients in this basis throughout. Take mutually independent standard normal variables and set These series converge almost surely in and define independent centered Borel Gaussian random elements with the same law . Define the Gaussian random-walk proposal , its probability kernel its forward flow , and its transpose . Then and are mutually singular: a Borel set satisfies For the same reference law and scale, the pCN proposal flow is symmetric.
Statement references
Facts & Assumptions
Given: AC, , and the Gaussian sequence and Hilbert-space notation of the Statement.
AC implies both Dependent Choice and Countable Choice. The Axiom of Choice AC implies DC implies countable choice
Under Countable Choice and Dependent Choice, a countable independent sequence with the standard normal law exists. The Axiom of Countable Choice () The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain Countably many independent copies of a prescribed law exist
After the explicit reindexing for , the coordinate vectors form a complete orthonormal basis of , and the norm squared is the sum of coordinate squares. Coordinate vectors form the Hilbert basis of real ell-two
For independent standard normal coordinates and weights , the series converges almost surely in and defines a centered Borel Gaussian random element. Its coordinates are . Weighted Hilbert Gaussian series and prior regularity Coordinate vectors form the Hilbert basis of real ell-two
Disjoint subfamilies of an independent family generate independent sigma-algebras, and measurable functions of independent random elements remain independent. Independent random elements Disjoint groups of an independent sigma-algebra family remain independent Measurable coordinatewise functions preserve independence
A variable has mean zero, second moment one, and fourth moment three. Location-scale normal laws have their stated mean and variance A normal variable has finite fourth moment
Expectations of integrable products of independent variables factor. Expectations factor over finite products of independent random variables
IID square-integrable real variables satisfy the strong law of large numbers. Identical distribution and IID families Iid finite variance strong law
For a probability measure and a probability kernel, the associated joint flow is a probability measure with the iterated-integral identity. Measure kernel and probability kernel A prior and model kernel define a joint law
Integrating a Borel function against a random-element law equals its expectation; independent random elements have product joint law. Law or distribution of a random element Change of variables for expectation Independent random elements have product joint law
The Borel sigma-algebra of a topological space is generated by its open sets; Borel measurable functions are closed under finite arithmetic operations. The Borel sigma-algebra of a topological space Arithmetic and lattice operations preserve measurability whenever they are defined
The finite-support vectors with rational coordinates form a countable dense subset of : for each the rational vectors supported in the first coordinates are countable by the rational countability and finite product facts, their union is countable by Countable Choice, and density follows from finite truncation convergence and rational approximation of each finite coordinate list. The positive rational-radius norm balls are open in the induced metric topology and give a countable base: given with open, choose with , then in the dense set with and a positive rational with ; the triangle inequality gives . Thus is second-countable, the Borel sigma-algebra on is the product sigma-algebra, and integration of a nonnegative product-measurable function against a probability kernel gives a measurable function of its source point. The Axiom of Choice AC implies DC implies countable choice The Axiom of Countable Choice () Coordinate vectors form the Hilbert basis of real ell-two is countably infinite A product of two at most countable sets is at most countable Every subset of an at most countable set is at most countable Countable unions of at most countable sets, assuming The rationals embed densely in the reals Separability: the existence of an at most countable dense subset Second countability: an at most countable basis for the topology A norm on a real vector space, the induced metric, and the dictionary with the metric axioms Open ball, closed ball and sphere in a metric space The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed Borel sigma-algebra of a product of second-countable spaces Measurability of integration against a kernel A continuous map has Borel preimages of Borel sets
For the same Gaussian reference law and , the pCN proposal pair law is symmetric. The pCN Gaussian reference pair law is symmetric
Under Countable Choice, Borel probability laws on a separable Hilbert space with the same finite coordinate laws in a complete orthonormal basis are equal. The Axiom of Countable Choice () AC implies DC implies countable choice Borel laws on a separable Hilbert space are determined by basis coordinates
Proof
Given: The hypotheses and notation in the Statement.
By [A1] and [F1], take a countable independent sequence with law and put , . Each subsequence is again IID standard normal. The odd and even coordinate sigma-algebras are independent by [F4]. Apply [F3] with , , and to each subsequence. Since , both series converge almost surely in and define centered Borel Gaussian random elements. Their finite coordinate laws agree: by [F3], each finite coordinate vector is obtained by multiplying independent standard normals by the same coefficients , so each vector has the same product normal law by [F5] and [F9]. AC implies Countable Choice by [A1], so [F13] identifies their Borel laws. Each limit is measurable with respect to its own coordinate sigma-algebra: its partial sums are block-measurable, the event that they are Cauchy is a countable combination of measurable norm inequalities, and the limit, set to zero on the null complement, is therefore block-measurable. In detail, for a proper open with closed complement , on the convergence event the preimage of is the condition ; the distance function is 1-Lipschitz, and the zero value assigned off that event is included exactly when . This is a measurable condition on the block. The odd and even coordinate sigma-algebras are independent by [F4], hence and are independent. Denote their common law by .
For , set Each coordinate map is continuous since by [F2]; finite arithmetic operations make Borel by [F10]. Explicitly, so is Borel by [F10]. The limit criterion follows because for every one can choose with .
For each , is the pushforward of under the continuous map , hence is a probability measure. By [F11], is second-countable and the product Borel sigma-algebra is . For Borel , addition and scalar multiplication make continuous, so is product-measurable. Integrating it against the constant kernel is measurable by [F11], so is a probability kernel. Its joint flow exists by [F8]. By the product joint law [F9] and the proposal pushforward, is the law of .
For each , define The pairs are independent by grouping the independent coordinates, and have the same product standard-normal law by [F9]. Applying the same polynomial map to each pair therefore makes IID by [F4] and [F9]. By [F5]–[F6], , , and They are square-integrable: using , where independence gives and [F5] gives . By [F7],
Under the forward flow , the pair has the law of from step 2.1, and . Step 2.2 therefore gives . Under the transpose , the pair has the law of , and . Since , , hence .
Thus and its complement are disjoint Borel sets with and . This is mutual singularity of the two probability measures, and in particular neither is absolutely continuous with respect to the other. By [F12], the pCN reference proposal flow at this same scale equals its transpose.
A Gaussian pCN kernel leaves a normal posterior invariant
Example
Assume the Axiom of Choice. Let , give the unknown parameter the prior law , and observe one datum from the model . The Gaussian conjugate update gives posterior . Use the potential in the pCN algorithm. For , write , propose with independent of the current state, and accept with probability The resulting pCN probability kernel leaves invariant for every .
Example references
Facts & Assumptions
Given: The Axiom of Choice, the one-observation normal model and pCN rule in the Example.
For prior and one observation from , the posterior mean is and the posterior variance is ; evidence is finite and positive. Known-variance Normal-Normal conjugate update
The law has density with respect to Lebesgue measure. Standard normal and normal laws A positive-variance normal law has its location-scale density
The pCN rule proposes and accepts with probability for finite potential values. Prior-preserving Crank–Nicolson sampler
The pCN accept-reject probability kernel leaves its normalized posterior target invariant. The pCN accept-reject kernel preserves the posterior
Proof
Given: The Axiom of Choice, prior , observation variance , datum , and potential .
Apply [F1] with , , , , and . The posterior variance is , and its mean is . The evidence is finite and positive, so the posterior is the proper law .
By [F2], the likelihood density at is . Its constant factor cancels when the likelihood is normalized against the prior, so the potential gives exactly the posterior from step 1.1. It is finite on , and the pCN target assumptions are satisfied.
For the proposal in [F3], so the stated acceptance probability is precisely the algorithm's pCN acceptance rule for this target.
Step 1.1 identifies the normalized target, and step 3.1 identifies the kernel as the pCN accept-reject kernel for that target. Applying [F4] proves that is invariant for every .
Sources
- S. L. Cotter, G. O. Roberts, A. M. Stuart, and D. White, MCMC Methods for Functions: Modifying Old Algorithms to Make Them Faster, Statistical Science 28(3) (2013)
- Yury Korolev and Jonas Latz, Inverse Problems: Lecture Notes, Michaelmas Term 2020 (University of Cambridge, 18 May 2021)
- MIT 18.05, Spring 2022, Class 15: Conjugate priors: Beta and normal