Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- The factorial satisfies and for every natural number .
- Defines cosine and sine on the real line by their power series, with the convergence of those series discharged by comparison with the series of powers over factorials.
Iterated Powers, Factorials, and Convergence of the Series of Powers over Factorials
lemmalem:factorial-power-series-majorant-2026aAnalysisFactorials are positive and nondecreasing, the series of powers of a nonnegative real number divided by factorials converges, and it dominates the two series of even and odd order that define cosine and sine.Differentiability at an Interior Point is a Local Property
lemmalem:derivative-local-interval-2026aAnalysisIf a real function restricted to a subinterval containing a neighbourhood of an interior point is differentiable there, then the function itself is differentiable at that point, with the same derivative.- A series of real numbers converges exactly when the series of its terms from the second onward converges, and then its sum is the first term plus that sum.
Series of Real-Valued Functions and Their Partial Sums
definitiondef:series-of-functions-2026aAnalysisDefines the partial sums of a sequence of real-valued functions on a set, and pointwise and uniform convergence of the resulting series on a subset of that set.Linearity of the Riemann Integral of Continuous Functions, and Passage to a Uniform Limit
lemmalem:uniform-convergence-riemann-integral-2026aAnalysisThe Riemann integral of continuous functions on a compact interval is linear and bounded by the length of the interval times a bound on the integrand, and it passes to uniform limits and to termwise integration of uniformly convergent series.- If the terms of a series of real-valued functions are bounded in absolute value by the terms of a convergent series of constants, then the series converges absolutely at each point and uniformly, with the tail of the dominating series as an explicit error bound.
Continuity and Uniform Continuity of a Uniform Limit of Real-Valued Functions
lemmalem:uniform-limit-continuous-2026aAnalysisA uniform limit of continuous real-valued functions is continuous, and a uniform limit of uniformly continuous functions is uniformly continuous; continuity at a single point requires uniform convergence only on a neighbourhood of that point.Pointwise and Uniform Convergence of a Sequence of Real-Valued Functions
definitiondef:uniform-convergence-real-functions-2026aAnalysisDefines pointwise and uniform convergence of a sequence of real-valued functions on a subset of their common domain, together with the corresponding notions for a series of functions.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.