Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Second-Order Structure Condition for an Equation Operator on a Hilbert Triple
definitiondef:second-order-structure-condition-hilbert-triple-2026aAnalysisPDEThe structure inequality of the first-order condition, but required only for those pairs of symmetric forms that the doubling lemma produces at a quadratic penalty of a given strength.An Orthonormal Basis of the Ambient Space Contained in the Form Space of a Hilbert Triple
lemmalem:orthonormal-basis-in-v-hilbert-triple-2026aAnalysisIn a Hilbert triple whose ambient space is infinite-dimensional, the ambient space has an orthonormal basis all of whose members lie in the densely embedded form space.Lions' Lemma on a Hilbert Space: Test Data and Form Bounds at a Sequentially Strict Maximum of a Quadratically Penalised Difference
lemmalem:lions-doubling-hilbert-2026aAnalysisPDEThe infinite-dimensional counterpart of Ishii's lemma: at a sequentially strict maximum of a quadratically penalised difference on a Hilbert space, both functions admit test data whose second-order parts are controlled by a pair of forms supported on a finite orthonormal tuple, u…Fibre Suprema along a Coordinate Map and Their Semicontinuous Envelopes
lemmalem:fibre-supremum-envelope-hilbert-2026aAnalysisTaking suprema and infima over the fibres of a coordinate map turns a quadratically penalised difference on a subspace of a Hilbert space into one on Euclidean space whose semicontinuous envelopes still attain their maximum at the image of the original maximum point.Coordinate Maps of a Finite Orthonormal Tuple: Forms, the Tail Form, and Quadratic Test Functions
lemmalem:coordinate-quadratic-hilbert-2026aAnalysisLinear AlgebraA finite orthonormal tuple in a Hilbert space gives a coordinate map onto Euclidean space; this lemma records its elementary properties, the bilinear forms and tail form it determines, and the fact that a Euclidean quadratic read through it is a twice continuously differentiable…Localisation at a Sequentially Strict Maximum of a Quadratically Penalised Difference
lemmalem:penalised-difference-localisation-2026aAnalysisIf a quadratically penalised difference attains a sequentially strict maximum, then near-maximising pairs are close to the maximum point and their values are close to the values there.Quadruple Approximable by Test Data on a Subset of a Real Inner Product Space
definitiondef:approximable-test-data-hilbert-2026aAnalysisPDEThe Hilbert-space analogue of approximability by test data: a point, value, gradient and Hessian that are matched, to within any prescribed accuracy, by a test function touching the given function from above or from below at a nearby point of a subset.The Gradient of the Quartic Energy on the First Sobolev Space of the Torus
lemmalem:phi4-energy-frechet-derivative-torus-2026aAnalysisPDEThe quartic energy is differentiable everywhere on the first Sobolev space of the torus, with gradient expressed through the Riesz map of the Sobolev Hilbert triple; on the domain of the form operator the gradient is twice the Riesz image of the Allen-Cahn drift.Well-Posedness of the Allen-Cahn Hamilton-Jacobi Equation on the Torus
corollarycor:allen-cahn-hamilton-jacobi-well-posed-torus-2026aAnalysisPDEOn the torus of dimension at most three, the Hamilton-Jacobi equation whose drift is the Allen-Cahn field has a unique bounded continuous viscosity solution on the square-integrable space, obtained by instantiating the general Hilbert-triple well-posedness theorem at the Sobolev…The Quartic Energy Functional on the First Sobolev Space of the Torus
definitiondef:phi4-energy-torus-2026aAnalysisPDEOn the torus of dimension at most three, the energy of a Sobolev class is the sum of the squared square-integrable norms of its weak partial derivatives, plus a multiple of the integral of the fourth power of a representative, minus a multiple of its squared square-integrable nor…Integrability of Products of Four Sobolev Classes on the Torus in Dimensions at Most Three
lemmalem:quartic-product-torus-2026aAnalysisPDEOn the torus of dimension at most three, the pointwise product of representatives of four members of the first Sobolev space is integrable, with integral bounded by the product of their Sobolev norms and independent of the representatives; in particular fourth powers are integrab…The Expansion of the Square and the Fourth Power of a Sum of Real Numbers
lemmalem:fourth-power-binomial-real-2026aAnalysisAlgebraThe square of a sum of two real numbers expands as the usual three terms, and the fourth power as the five terms with coefficients one, four, six, four and one.Euclidean, Metric and Sequential Continuity of a Real Function of a Real Variable
lemmalem:real-function-continuity-readings-2026aAnalysisFor a function from the real line to itself, continuity in the Euclidean sense and in the metric sense coincide, a local Lipschitz bound implies both, and continuity everywhere implies sequential continuity.The Cube Map is a Monotone Nonlinearity on the Sobolev Hilbert Triple of the Torus
lemmalem:cube-map-monotone-nonlinearity-torus-2026aAnalysisPDEIn dimensions at most three the map sending a Sobolev class on the torus to a nonnegative multiple of its pointwise cube is a monotone nonlinearity for the Hilbert triple formed by the square-integrable and Sobolev spaces.- Composing a class in the Sobolev space of the torus with a continuously differentiable function of bounded derivative again lies in that space, and its weak partial derivatives are given by the classical chain rule formula.
A Bounded-Derivative Truncation of the Cube Map on the Real Line
lemmalem:truncated-cube-real-2026aAnalysisFor a positive real parameter, the rational function s^3/(1+eps s^2) is differentiable with continuous, nonnegative and bounded derivative, is sign-preserving and dominated by |s|^3, and approximates the cube map with an explicit error.The Sobolev Embedding of the First Sobolev Space of the Torus into the Sixth Lebesgue Space in Dimensions at Most Three
theoremthm:sobolev-embedding-h1-torus-2026aAnalysisOn the torus of dimension one, two or three, every member of the first Sobolev space is six-fold power integrable, with sixth seminorm at most five times its Sobolev norm. The bound is first proved for continuously differentiable periodic functions and then extended by mollificat…The Gagliardo-Nirenberg Inequality on the Torus in Dimensions at Most Three
theoremthm:gagliardo-nirenberg-torus-2026aAnalysisFor a continuously differentiable periodic function on the torus of dimension one, two or three, a power of a Lebesgue seminorm is bounded by the product of the quantities obtained by adding the first seminorm of the function to the first seminorm of one of its partial derivative…- For a continuous periodic function on the torus, averaging over one period in a single coordinate direction yields again a continuous periodic function, free of that coordinate. The lemma records the elementary properties of this slice average: positivity, factoring out coordinat…
The One-Dimensional Slice Bound for a Continuously Differentiable Periodic Function
lemmalem:one-dimensional-sup-bound-torus-2026aAnalysisA continuously differentiable periodic function is bounded at every point by the integral, over one period in any single coordinate direction, of its absolute value plus the absolute value of the corresponding partial derivative.