Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- There is a set with no elements.
- For any two sets there is a set whose elements are exactly those two sets.
- Two classes with the same elements are equal.
Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations
definitiondef:formula-class-theory-nbg-2026aLogicSet TheoryA metatheoretic definition of the formulas of class theory, built from membership and equality between class and set variables, of their free variables, of predicative formulas (no quantifier over a class variable), and of defined set symbols as abbreviations.- The primitive notions of class theory are class and membership; a set is a class that is an element of some class, and a proper class is a class that is not a set.
Compatible Noise Penalty Pairs at a Fine and a Coarse Level
definitiondef:compatible-noise-penalty-pairs-hilbert-2026aAnalysisProbabilityTwo noise penalty pairs at a fine and a coarse level, joined by a mode-restriction link, are compatible with constant c_0 if the push-forward under the mode restriction maps the fine penalty and score domains into the coarse ones and raises the penalty by at most c_0.Two Noise Levels over Hilbert Spaces: a Fine and a Coarse Reading of the Noise Framework and Level-Indexed Notation
settingset:noise-levels-hilbert-2026aAnalysisProbabilityFixes two readings, a fine and a coarse level, of the standing noise Wasserstein and noise penalty framework over two Hilbert spaces with their bases, noise weights and reference measures, together with the level-indexed notation (noise norms, field norms, couplings, distances, t…Comparison, Uniqueness and Convergence of Coarse Solutions Inherited by a Fine First-Order Equation on the Noise Wasserstein Space from a Consistent Family of Coarse Levels
corollarycor:inherited-comparison-first-order-hilbert-2026aAnalysisProbabilityUnder the hypotheses of the cross-level comparison principle, if every coarse equation has a viscosity solution and these are bounded uniformly in the level, then the fine equation satisfies comparison and uniqueness for bounded solutions, and a bounded fine solution is the limit…A Cross-Level Comparison Principle for First-Order Equations on a Fine Noise Wasserstein Space and a Family of Coarse Levels Linked by Mode Restrictions
theoremthm:cross-level-comparison-first-order-hilbert-2026aAnalysisProbabilityIf a family of coarse noise levels, linked to a fine level by mode restrictions, satisfies the hypotheses of the single-level comparison principle with constants uniform in the level, and the consistency defect between the fine and the coarse operators vanishes as the level grows…Bounds, Monotonicity and Borwein-Preiss Perturbed Maximisers of the Cross-Level Doubled Function in the Coarse Noise Wasserstein Distance for Compatible Noise-Closed Penalty Pairs
lemmalem:cross-level-doubling-perturbed-maximiser-hilbert-2026aAnalysisProbabilityFor compatible noise-closed penalty pairs at a fine and a coarse level and upper semicontinuous functions dominated by minus delta times the penalties, the doubled function U(mu)+V(nu)-(alpha/2)W(p_#mu,nu)^2 has a finite supremum, controlled by its diagonal, monotone in the doubl…Cross-Level Data and Eta-Consistency of a Fine and a Coarse Level at (delta, R)
definitiondef:cross-level-consistency-hilbert-2026aAnalysisProbabilityFor compatible noise penalty pairs at a fine and a coarse level linked by a mode restriction, defines cross-level data (a fine measure, a real number and a coarse tangent field) and their R-boundedness, and calls the two levels eta-sub-, eta-super- or eta-consistent at (delta, R)…Noise Intrinsic Test Functions Pulled Back along a Mode Restriction, and the Squared Coarse Noise Wasserstein Distance as a Fine Test Function
lemmalem:restricted-noise-test-function-hilbert-2026aAnalysisProbabilityComposing a coarse-level noise intrinsic test function with push-forward by the mode restriction gives a fine-level test function whose gradient is the pulled-back coarse gradient; in particular the squared coarse distance from the restricted measure to a fixed measure is a fine…Properties of a Mode-Restriction Link: Isometric Embedding, Contraction of Noise Norms and Noise Wasserstein Distances, and Pull-Back of Cylindrical Functions and Tangent Fields
lemmalem:mode-restriction-link-hilbert-2026aAnalysisProbabilityThe mode restriction p of a mode-restriction link is a left inverse of the isometric mode embedding j; both respect the noise norms and are adjoint for them, push-forward by p contracts noise costs and noise Wasserstein distances, and composing with p and j carries cylindrical fu…Mode-Restriction Links between a Fine and a Coarse Noise Level
definitiondef:mode-restriction-link-hilbert-2026aAnalysisProbabilityDefines a mode-restriction link from a fine to a coarse noise level: an injective relabelling of basis modes that preserves the noise weights, together with its mode restriction p and its mode embedding j.Finite Linear Combinations of Continuous Real-Valued Maps on a Metric Space are Continuous
lemmalem:finite-sum-continuous-metric-2026aAnalysisTopologyA finite linear combination, over a nonempty finite index set, of continuous real-valued maps on a metric space is continuous.The Maps from a Finite Set to a Nonempty Finite Set Form a Nonempty Finite Set
lemmalem:maps-between-finite-sets-finite-2026aCombinatoricsThe set of all maps from a nonempty finite set to a nonempty finite set is nonempty and finite.The Hubbard-Stratonovich Ising Field on the Lattice Torus: What the Lattice Results Model, the Role of the Choices, and the Temperature Regimes
remarkrem:hubbard-stratonovich-ising-regimes-torus-hilbert-2026aProbabilityExplains why the Ising model enters through the Hubbard-Stratonovich field: spin laws are singular to every Gaussian. It also covers which choices are canonical (the kernels) and which are not (the shift, the split, the lattice-to-torus embedding), and when the convex theory appl…The Gibbs Entropy Pair of the Hubbard-Stratonovich Ising Field is Lambda-Displacement Convex, with Lambda Uniform in the Cutoff when the Shifted Symbol Stays below One
lemmalem:hubbard-stratonovich-ising-convex-torus-hilbert-2026aProbabilityPDEThe Gibbs entropy pair of the Hubbard-Stratonovich Ising field is (1/r-bar_s - K_s)-displacement convex for every admissible split; when the shifted symbol stays below q-bar < 1 it is lambda(q-bar)-displacement convex with lambda(q-bar) = min{1/(1+q-bar), (1-q-bar)/q-bar} > 0, in…Well-Posedness of the Hamilton-Jacobi Equation of the Hubbard-Stratonovich Ising Field on the Lattice Torus at Every Cutoff, Interaction and Shift: Comparison, Existence and Uniqueness
corollarycor:hubbard-stratonovich-ising-hamilton-jacobi-well-posed-torus-hilbert-2026aProbabilityPDEFor every cube cutoff, reflection-symmetric periodic pair interaction and shift, the Hamilton-Jacobi equation driven by the Gibbs score of the Hubbard-Stratonovich Ising field satisfies comparison and has exactly one bounded viscosity solution, for every bounded uniformly continu…The Hamilton-Jacobi Equation of the Hubbard-Stratonovich Ising Field on the Lattice Torus with White Noise
equationeq:hubbard-stratonovich-ising-hamilton-jacobi-torus-hilbert-2026aProbabilityPDEThe Hamilton-Jacobi equation of the Hubbard-Stratonovich Ising field is the Hamilton-Jacobi equation with Gibbs score drift whose Gibbs measure is the Hubbard-Stratonovich field law, written through any admissible split of its Gaussian. Its penalty pair, and hence its operator, i…