Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
A Nonnegative Continuous Function with Zero Integral
problemprob:nonnegative-zero-integral-2026aAnalysisHonours to analysis level. A continuous nonnegative function on a closed interval whose integral vanishes is identically zero.A Function with Small Derivative Has Exactly One Fixed Point
problemprob:contraction-unique-fixed-point-2026aAnalysisHonours level. A function differentiable on the whole real line whose derivative is bounded in absolute value by one half has exactly one fixed point.- Honours level. Show that the sequence given by and is increasing and bounded above by , hence convergent, and that its limit is .
- Introductory to honours level. A continuous function on the unit interval taking equal values at the endpoints takes equal values at some pair of points half a unit apart.
- Introductory calculus. Show that has exactly one real zero and locate it in the open interval from to , combining the intermediate value theorem with strict monotonicity from the sign of the derivative.
The Rectangle of Greatest Area with a Given Perimeter
problemprob:rectangle-maximal-area-2026aAnalysisIntroductory calculus. Show that the area function of a rectangle of fixed perimeter attains a greatest value on the relevant closed interval and does so only at the square, using the extreme value theorem and the vanishing of the derivative at an interior extremum.A Limit Computed from the Epsilon-Delta Definition
problemprob:limit-square-epsilon-delta-2026aAnalysisBeginner level. Verify the limit of at straight from the epsilon-delta definition, by exhibiting a delta for each epsilon.- A function continuous on an interval and differentiable at its interior points is nondecreasing when its derivative is nonnegative there and strictly increasing when its derivative is positive, with the corresponding statements for the reverse inequalities.
A Bounded Monotone Sequence of Real Numbers Converges
theoremthm:monotone-bounded-sequence-converges-2026aAnalysisA nondecreasing sequence of real numbers whose terms are bounded above converges to the supremum of its set of terms, and the nonincreasing case converges to the infimum.Intermediate Value Theorem on a Closed Real Interval
theoremthm:intermediate-value-closed-interval-2026aAnalysisA function continuous on a closed real interval attains every value lying between its values at the two endpoints.Continuity at a Point of an Interval in Terms of the Limit
lemmalem:limit-continuity-bridge-2026aAnalysisA real function on an interval is continuous at a point of that interval exactly when its limit at the point exists and equals its value there.- Defines nondecreasing, nonincreasing, strictly increasing and strictly decreasing real-valued functions on a subset of the real line, and the terms monotone and strictly monotone.
- The epsilon-delta definition of the limit of a real-valued function at a point of an interval, and the notation for it. Uniqueness of the limiting value is established separately.
- Fixes the standing objects and vocabulary of single-variable calculus on an interval: continuity, the derivative at an interior point, the Riemann integral, and the standard theorems about them, all carried by reference.
- Fixes the notation and background facts about the real numbers, intervals, continuity and sequences that the calculus items adopting it use throughout. It introduces no new concept and carries its background results by reference.
The Asymptotically Optimal Value of the Recentred N-Agent Cost of the Ising Population Model
corollarycor:ising-asymptotic-value-2026aAnalysisProbabilityThe Ising population model satisfies every standing hypothesis of the fluctuation optimality theorem at its even-split equilibrium, so the asymptotically optimal value of its recentred N-agent cost is the explicit integral of the two scalar Riccati solutions.The Control and Filter Riccati Families of the Ising Equilibrium in Closed Form
lemmalem:ising-riccati-families-2026aAnalysisProbabilityBoth Riccati families of the Ising equilibrium reduce to scalar equations along the tangential direction and are solved in closed form; this verifies the Riccati hypothesis of the completion-of-squares theorem and identifies the Kalman covariance and the two integrands of the flu…The Even-Split Equilibrium of the Ising Population Model is a Stationary Mean-Field Triple and is Optimal
lemmalem:ising-stationary-triple-2026aAnalysisProbabilityThe constant triple with an even population split, unit transition rates and vanishing co-state is a stationary mean-field triple whose control is the unique Hamiltonian minimiser and is globally optimal for the mean-field problem, and the first-order to-go regularity hypothesis…The Ising Population Model Instantiates the Data of the Fluctuation Theory
lemmalem:ising-data-well-posed-2026aAnalysisProbabilityThe Ising rates, observation rates and costs form an affine-controlled transition-rate family, an observation-rate family and population cost data with the stated smooth extensions, and satisfy the compactness, uniform observation positivity and Lipschitz cost hypotheses of the f…- Constructs a globally , convex, nonnegative function on the real line that coincides with the entropic rate cost near the rest rate 1, vanishes only there, and has bounded, Lipschitz first and second derivatives.