Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- 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.
- Defines, from eight parameters, the data of a two-state controlled population of Ising type: the compact box of admissible transition rates, the rates themselves, the entropic running cost with its splitting interaction, the two observation channels, and the smooth extensions of…
Regimes of the Ising Population Model Outside the Fluctuation Optimality Theorem
remarkrem:ising-excluded-regimes-2026bProbabilityRecords which regimes of the Ising population model the fluctuation optimality theorem excludes and why: the ferromagnetic sign of the interaction breaks joint coercivity, a vanishing background observation rate breaks uniform observation positivity, and the convexity weight is a…The Ising Population Model: A Worked Instance of the Fluctuation Theory
exampleex:ising-population-model-2026aProbabilityA self-contained account of a two-state controlled population whose controls are the transition rates and whose observations are noisy per-state counts: its mean-field equilibrium, the scalar fluctuation problem it reduces to, and the closed-form asymptotically optimal value of i…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 Fluctuation LQG Data of the Ising Equilibrium and Its Joint Coercivity
lemmalem:ising-fluctuation-lqg-data-2026aProbabilityLinear AlgebraComputes every matrix of the fluctuation linear-quadratic-Gaussian data at the even-split equilibrium of the Ising model in closed form, and shows that the fluctuation Hessian is positive definite with an explicit coercivity constant.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.