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.
Integral probability metrics and Wasserstein GANs
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Absolute Continuity and the Sharp Fundamental Theorem of Calculus
- Areas of Elementary Plane Figures
- Banach Valued Integration and the Radon Nikodym Property
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Variation and the Riemann–Stieltjes Integral
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Lp Spaces and Test-Function Conventions
- Complex Norms and Realification
- Complexification, Realification and Real Structures
- 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
- Convex and Semicontinuous Functions on Rⁿ
- Convexity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Density Separability and Convolution in Lᵖ
- Determinants of Matrices over a Commutative Ring
- Differentiation of Monotone Functions and the Vitali Covering Theorem
- Distributions Test Functions and Differentiation
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Euclidean Surface Measure, Divergence, and Green Identities
- F-Divergences, Rényi Information, and Hypothesis Testing
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite-metric transport duality
- Finite-window spatial likelihood
- Foundations of the Real Numbers for Analysis
- Fubini and Change of Variables
- Function Space Topologies and the Exponential Law
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Hausdorff via the Diagonal
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Kantorovich–Rubinstein duality on compact metric spaces
- Lebesgue Measure on Euclidean Space
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- 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
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Hamilton–Jacobi–Bellman schemes and policy iteration
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Norming and Separation under Hahn–Banach
- Order, Zorn's Lemma, and the Axiom of Choice
- Outer Measure and the Caratheodory Extension Theorem
- Pointwise Extended-Real Function Products
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- 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
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Schwartz Space and the Plancherel Theorem
- 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
- Smooth Approximation and Sobolev Extension
- Sobolev Poincare and Morrey Inequalities
- Subspaces, Products, and Quotients
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Derivative and the Mean Value Theorems
- The Exponential Function
- The Inverse and Implicit Function Theorems
- 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 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
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Weak Derivatives and Sobolev Spaces
2 · Logical flowchart
3 · Definitions, theorems and proofs
Integral probability metrics
Definition
Let be a measurable space, let and be probability measures on it, and let be a nonempty class of real-valued -measurable functions that are integrable under both and . The integral probability metric induced by is It is nonnegative and symmetric, and it may equal ; no separation property is asserted for an arbitrary class .
Continuity and ideal-critic gradients for compact-space Wasserstein GAN objectives
Statement
Let be a nonempty compact metric space, fix , and let satisfy for all . Let be a Borel probability measure on , let be a probability space, and let be open with . For every , let be measurable and define its law by for Borel . Assume is -measurable for every , and that there is a measurable set with on which is continuous. Let be the class of bounded Borel functions satisfying and for all , and set . Then and is continuous on .
Suppose in addition that for every there are an open neighborhood of , a measurable with , and a measurable full-measure set such that, for every and every ,
Then is locally Lipschitz, with for . At any such where is Fréchet differentiable, if the signed dual supremum at is attained by and is Fréchet differentiable in at for -almost every with measurable derivative, then
Here Fréchet differentiability of a scalar function at means there is a linear map such that as . The attainment and composite-differentiability assumptions are pointwise hypotheses for the gradient formula; compact dual attainment is not asserted.
Statement references
The coupling definition of the 1-Wasserstein cost on a compact metric space: Compact-space coupling definition of
Compact-metric Kantorovich–Rubinstein duality
Facts & Assumptions
Given: The compact metric data space and finite bound , base point , Borel probability , probability space , open finite-dimensional parameter set , measurable random elements , their laws , the pointwise continuity and distance-measurability hypotheses, and the additional common-neighborhood integrable envelope wherever the local-Lipschitz and gradient conclusions are used.
For a nonempty class of real-valued functions integrable under both laws, the IPM is the supremum of the absolute differences of their integrals. Integral probability metrics
For Borel probabilities on a nonempty compact metric space, the coupling cost equals the signed supremum over normalized -Lipschitz functions; the supplier proof establishes that these tests are bounded Borel and that no compact primal or dual attainment is asserted. Kantorovich–Rubinstein duality on compact metric spaces
The compact-space convention is the infimum of Borel coupling costs over couplings with the stated marginals. The coupling definition of the 1-Wasserstein cost on a compact metric space
A random element is a measurable map from a probability space into a measurable target space. Random elements and real random variables
The law of a random element is for each measurable target set . Law or distribution of a random element
The law of a random element is a probability measure. The law of a random element is a probability measure
A nonnegative simple measurable function has a finite representation by nonnegative coefficients on pairwise disjoint measurable sets, and its simple integral is the corresponding finite weighted sum. Nonnegative simple measurable functions The integral of a nonnegative simple function
The nonnegative Lebesgue integral agrees with that simple integral on nonnegative simple functions. The nonnegative integral agrees with the simple integral on simple functions
A nonnegative measurable function is the pointwise increasing limit of nonnegative simple functions. Every nonnegative measurable function is the increasing limit of simple measurable functions
If measurable functions converge almost everywhere and are dominated by one integrable nonnegative function, their integrals converge. Dominated convergence
For a bounded real measurable function, its signed Lebesgue integral is the difference of the integrals of its positive and negative parts. Integrable real and complex functions, and their integrals
The rationals are dense in the reals. Enumerate rational -tuples explicitly by integer numerators and positive denominators of increasing bounded height; coordinatewise rational approximation makes these tuples dense in . No selection of a sequence from arbitrary nonempty sets is involved. The rationals embed densely in the reals
The supremum of a sequence of measurable real or extended-real functions is measurable. Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable
Proof
Given: The hypotheses in the Statement and the additional envelope and pointwise attainment/composite-differentiability hypotheses for the gradient branch.
By [F4] and [F6], every is a probability measure. By [F5], for every Borel . If is nonnegative simple with disjoint Borel sets, [F7]–[F8] give . For any bounded Borel real , apply [F9] to and ; their increasing simple approximants are bounded by , whose integral is finite under both probability measures. Applying [F10] to the approximants and their compositions gives equality of the positive-part integrals and of the negative-part integrals; [F11] then yields .
The zero function belongs to , so this class is nonempty; it is also symmetric under , so its supremum of absolute integral differences equals its signed supremum. It is exactly the bounded Borel version of the compact KR test class in [F2]. Hence for every , with the coupling-cost convention in [F3].
Fix and its attaining critic, and choose such that the ball lies in the envelope neighborhood. Let be the intersection of its measurable full-measure set with a measurable full-measure set where the composite is Fréchet differentiable. Extend the measurable derivative by zero off . On its norm is at most , by the envelope and the critic's -Lipschitz inequality, so all coordinates are integrable. Write . For put and let be zero off and otherwise the supremum of over rational -tuples with , including zero among the values. The explicit enumeration and [F13] give measurability; the envelope gives , and pointwise Fréchet differentiability gives on . By [F10], . On the remainder ratio is continuous in nonzero by the envelope, so rational density [F12] bounds it by for every real . Therefore for all such , proving the full Fréchet limit without a sequential-criterion choice step. Thus has derivative .
Fix and a ball . Put . On , let be the supremum of over rational -tuples with , and set it to zero off . It is measurable by the assumed distance measurability, [F12] and [F13], is bounded by , and tends pointwise to zero by parameter continuity. Thus [F10] gives . Parameter continuity and rational density make dominate the same distance for all real increments on . For every critic , step 1.1 and its -Lipschitz property give , where . The same bound holds for the difference of their absolute values and hence of the two suprema. It follows that for all , proving continuity.
Under the common-neighborhood envelope, the same estimate gives for every and . Taking absolute values and then suprema proves the stated local-Lipschitz bound for .
By optimality, and for every . Thus has a local minimum of at . Along every direction , differentiability and the two one-sided difference quotients at this minimum give ; since this holds for every , the derivative of the difference is zero, giving the claimed gradient formula.
Remarks
The local-Lipschitz conclusion uses a single integrable envelope valid on one parameter neighborhood for almost every latent input. Arjovsky et al.'s Assumption 1 gives only pointwise local constants; Appendix C does not justify replacing the latent-dependent neighborhoods by a common parameter neighborhood. The two explicit false statements and witnesses on the examples companion separately refute that local-Lipschitz inference and the asserted gradient exchange under the original condition, including a density-latent witness where both derivatives exist. They do not refute the corrected common-envelope theorem or by themselves settle the source's bare almost-everywhere assertion. The present Statement's continuity, full local-Lipschitz bound and conditional optimal-critic Fréchet formula are preserved. No claim is made for approximate critics, arbitrary spaces, compact dual attainment, or convergence of saddle-point optimization. The additional source diagnosis and rational-supremum proof refinement are owner-delegated local work; original native proof and external source-reading history remain separately attributed.
The compact-space WGAN value is differentiable almost everywhere under choice
Statement
Assume the full Axiom of Choice and all hypotheses of the common-neighborhood integrable-envelope branch of the compact-space WGAN theorem. Then its value function is Fréchet differentiable outside a Lebesgue-null subset of .
Statement references
Facts & Assumptions
Given: The full Axiom of Choice, an open with , and the hypotheses of the common-neighborhood integrable-envelope branch of the WGAN theorem.
The Axiom of Choice states that every family of nonempty sets has a choice function. The Axiom of Choice
Under its common-neighborhood integrable-envelope hypothesis, the WGAN value is locally Lipschitz on . Continuity and ideal-critic gradients for compact-space Wasserstein GAN objectives
Assuming full AC, every locally Lipschitz map from an open subset of to is Fréchet differentiable outside a Lebesgue-null subset. Rademacher differentiability in Euclidean space
Proof
By [F1], is a locally Lipschitz real-valued function on the open set .
Under [A1], apply [F2] to on ; it is Fréchet differentiable outside a Lebesgue-null subset of .
4 · Examples, counterexamples and false statements
None yet.
Sources
- Martin Arjovsky, Soumith Chintala and Léon Bottou, Wasserstein GAN, §3, equation (2), PDF pp. 5–6
- Filippo Santambrogio, Introduction to Optimal Transport Theory, §§1.1–1.3, PDF pp. 3–7
- Martin Arjovsky, Soumith Chintala and Léon Bottou, Wasserstein GAN, §§2–3, Theorems 1 and 3, Assumption 1, Appendix C, physical PDF pp. 3–7, 20–21 and 24–25
- Martin Arjovsky, Soumith Chintala and Léon Bottou, Wasserstein GAN, Theorem 1 and Appendix C, physical PDF pp. 5 and 20–21