Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Integrals of Uniform Limits and of Uniformly Convergent Series
lemmalem:uniform-limit-integral-2026aAnalysisA uniform limit of integrable functions on a closed interval is integrable, and its integral is the limit of the integrals; a uniformly convergent series of integrable functions may be integrated term by term.- If the values of a sequence of real-valued maps on a set are bounded in absolute value by the terms of a convergent series of reals, then the series of values converges absolutely at each point, its remainder after n terms is bounded by the n-th tail of the dominating series, and…
Continuity and Uniform Continuity of a Uniform Limit of Real-Valued Maps
lemmalem:uniform-limit-continuous-2026bAnalysisA uniform limit of continuous real-valued maps on a subset of a metric space is continuous, and a uniform limit of uniformly continuous ones is uniformly continuous; continuity at one point needs uniform convergence only near that point.Pointwise and Uniform Convergence of a Sequence of Real-Valued Maps
definitiondef:uniform-convergence-real-functions-2026bAnalysisDefines when a sequence of real-valued maps on a set converges pointwise, and when it converges uniformly, to a real-valued map on a subset, by epsilon-K conditions.An Absolutely Convergent Series of Real Numbers Converges
lemmalem:absolutely-convergent-series-converges-2026aAnalysisAn absolutely convergent series of real numbers converges, its sum is bounded in absolute value by the sum of the absolute values, and a series whose terms are dominated in absolute value by a convergent series converges absolutely.Well-Posedness for a Viscous Hamilton-Jacobi Equation with a Monotone Nonlinearity on a Hilbert Triple
theoremthm:viscous-monotone-hamilton-jacobi-well-posed-hilbert-triple-2026aAnalysisPDEOn a Hilbert triple whose ambient space is not finite-dimensional, the viscous Hamilton-Jacobi equation with a monotone nonlinearity, a Lipschitz drift, a trace term along a square-summable sequence and a bounded uniformly continuous cost has exactly one bounded continuous viscos…A Viscous Hamilton-Jacobi Operator with a Monotone Nonlinearity Satisfies the Second-Order Comparison Hypotheses
propositionprop:viscous-monotone-hamilton-jacobi-hilbert-triple-2026bAnalysisPDEA viscous Hamilton-Jacobi operator on a Hilbert triple whose Hamiltonian is half a nonnegative form dominated by the identity, with a monotone nonlinearity, a Lipschitz drift and a trace term along a square-summable sequence in the form space, is degenerate elliptic and strictly…A Real Hilbert Space Containing an Orthonormal Sequence Is Not Finite-Dimensional
lemmalem:orthonormal-sequence-not-finite-dimensional-2026aAnalysisIf a real Hilbert space contains an orthonormal sequence indexed by the natural numbers, then it has no finite basis.Elementary Properties of the Trace of a Form along a Square-Summable Sequence
lemmalem:trace-form-basic-hilbert-triple-2026aAnalysisThe trace along a square-summable sequence is linear and monotone for the order on forms, is bounded by the norm of the form times the sum of the squared norms of the sequence, gives that sum at the identity form, and vanishes in the limit on the tail forms of an orthonormal basi…Square-Summable Sequences in the Form Space of a Hilbert Triple and the Trace of a Form along Them
definitiondef:trace-form-hilbert-triple-2026aAnalysisDefines a sequence in the form space of a Hilbert triple to be square-summable when the series of squared form norms converges, and defines the trace of a bounded symmetric bilinear form on that space along such a sequence as the sum of its quadratic values there.A Comparison Principle on a Hilbert Triple under the Second-Order Structure Condition
theoremthm:comparison-second-order-hilbert-triple-2026aAnalysisPDEFor a locally strictly proper operator satisfying the second-order structure, shift-continuity and tail-insensitivity conditions, a bounded viscosity subsolution and a bounded viscosity supersolution satisfy a uniform comparison estimate on nearby points, and the subsolution does…The Second-Order Test-Datum Estimate at a Sequentially Strict Maximum of the Doubled Function
lemmalem:second-order-doubled-test-estimate-hilbert-triple-2026bAnalysisPDEAt a sequentially strict maximum of the doubled function, both functions admit test data at nearby points of the domain of the form operator with a common gradient alpha(x1 - y1) and an admitted pair of forms, satisfying the sub- and supersolution inequalities up to the shift mod…First-Order Operators Satisfy the Second-Order Structure and Tail-Insensitivity Conditions
lemmalem:first-order-implies-second-order-hilbert-triple-2026aAnalysisPDEA structure pair for the first-order condition is a structure pair for the second-order condition, and an operator that ignores its form argument is tail-insensitive along every admissible basis.The Tail-Insensitivity Condition for an Equation Operator on a Hilbert Triple
definitiondef:tail-insensitivity-condition-hilbert-triple-2026aAnalysisPDEAn operator is tail-insensitive if, along an orthonormal basis of the ambient space lying in the form space, adding or subtracting a multiple of the tail form eventually changes the shifted operator by at most any prescribed amount on bounded convergent test data.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.