Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- A Hahn set for a finite signed measure is a measurable set on whose measurable subsets the measure is nonnegative and on whose complement's measurable subsets it is nonpositive.
- Under dependent choice a finite signed measure has a Hahn set; for any Hahn set it splits as the difference of two finite measures, which do not depend on the Hahn set and inherit absolute continuity; and two Hahn sets differ only by a set all of whose measurable subsets have mea…
- A measure, or a finite signed measure, is absolutely continuous with respect to a measure μ if it vanishes on every measurable set of μ-measure zero.
- A finite signed measure on a measurable space is a real-valued, countably additive function on the measurable sets that vanishes on the empty set.
- For a probability measure, an integrable function with values in an open interval has its integral in that interval, and a convex function of the integral is at most the integral of the convex function, when the latter is integrable.
Convex Functions on an Open Interval: Monotone Slopes, Supporting Lines, Continuity, and the Supremum of Rational Supporting Lines
lemmalem:convex-supporting-lines-2026aAnalysisFor a convex function on an open interval the difference quotients increase, every point carries a supporting line whose slope is the infimum of the right difference quotients, the function is continuous, and it is the supremum of its supporting lines at rational points.- A real function on an interval of the real line is convex when its value at every weighted average of two points is at most the same weighted average of its values; the convex functions on the interval form a set.
The Quotient 1/x, Order Rules for Sums, and Nesting of Closed Intervals in ℝ
helperhlp:real-order-rules-estimates-2026aAlgebraFor real numbers: 1/x is the reciprocal of x when x is nonzero, 1 ≤ p implies 0 < p, sums of nonnegative numbers are nonnegative, adding a nonnegative number or adding on the left preserves ≤, and [c,d] lies in [a,b] when a ≤ c and d ≤ b.The Borel Sets of ℝ Form a σ-Algebra, and Integrable Functions Are Measurable Real-Valued Maps
helperhlp:borel-integrable-bookkeeping-2026aAnalysisProbabilityThe Borel σ-algebra of the real line is a σ-algebra on ℝ, and every integrable function on a measure space is a measurable map into ℝ.Ordinary Differential Equations with Measurable Time Dependence: Standing Notation and Background
settingset:measurable-ode-2026aAnalysisStanding notation and background for ordinary differential equations on a closed interval whose right-hand side is only measurable in time: integrals over subintervals, Carathéodory solutions of the integral equation, and Carathéodory–Lipschitz right-hand sides.Functions and Function-Valued Operators Given by Integrals over Subintervals
helperhlp:interval-integral-maps-2026aAnalysisUnder dependent choice, integrals over the subintervals [a,t] of [a,b] define functions of t, for scalar, vector-valued and parametric integrands, and the assignments g ↦ (t ↦ ∫ over [a,t] of g) and z ↦ (r ↦ F(r,z(r))) are functions between the relevant sets of functions.Composition of a Carathéodory–Lipschitz Function with a Measurable Path
lemmalem:caratheodory-superposition-2026aAnalysisAlong a measurable path x, a Carathéodory–Lipschitz right-hand side F gives a measurable function r ↦ F(r, x(r)), integrable when x is bounded, in particular when x is continuous, and Lipschitz in the path pointwise.- A function F on [a,b]×ℝⁿ is Carathéodory–Lipschitz with constant Λ if it is measurable in time for each fixed state, Λ-Lipschitz in the state, and integrable in time at the origin; CL_Λ is the set of such functions.
- A Carathéodory solution on [a,b] is a function along which the right-hand side is integrable and which satisfies the integral equation at every point; Sol(F,ξ) is the set of them.
The Integral Equation of an Initial Value Problem with Measurable Time Dependence
equationeq:caratheodory-integral-equation-2026aAnalysisNames the integral equation x(t) = ξ + ∫ over [a,t] of F(r, x(r)) dr on [a,b], with a Lebesgue integral, for a right-hand side F on [a,b]×ℝⁿ and an initial value ξ.- Integrals of real- and vector-valued integrable functions over subintervals of [a,b] vanish on points, are additive and monotone, satisfy the norm bound, and give uniformly continuous indefinite integrals, Lipschitz for bounded integrands; for continuous integrands they are Riema…
- The integral of a nonnegative function with finite integral, or of the absolute value of an integrable function, over a measurable set is small whenever the measure of the set is small enough.
Integrals over Subintervals of a Closed Interval: Notation
settingset:interval-integration-notation-2026aAnalysisNotation for Lebesgue integrals of real- and vector-valued integrable functions over subintervals of a closed interval, used for ordinary differential equations with measurable time dependence.Real Numbers Lie Strictly below ∞, and Each Element of a Subset of [−∞,∞] Lies below Its Supremum
helperhlp:extended-real-bounds-2026aAnalysisEvery real number is strictly less than ∞ in the extended real line, and every element of a subclass of the extended real line is at most its supremum.The Number n Lies in the Segment [n], and Membership in the Addition Class on ω
helperhlp:segment-top-omega-addition-2026aSet TheoryEvery natural number n lies in the segment [n], and a set ((a, b), c) belongs to the addition on omega exactly when a and b lie in omega and c = a + b.