Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- The partial sums of a sequence of functions into [0,∞], taken pointwise, form a sequence of functions into [0,∞].
Measurable Functions and the Lebesgue Integral: Notation
settingset:integration-notation-2026aAnalysisProbabilityFixes the notation for measurable functions, simple functions, the Lebesgue integral of nonnegative and of integrable real-, vector- and matrix-valued functions, positive and negative parts, pointwise operations, null sets and integrals over measurable subsets.Sums, Multiples and Products of Functions into [0,∞]
definitiondef:pointwise-operations-extended-2026aAnalysisProbabilityFor functions f and g from a set into [0,∞] and c in [0,∞], defines the pointwise sum f+g, multiple cf and product fg, formed with the sum and product of [0,∞]; in particular the product f1_A with an indicator function.Continuity on a Subset Is Continuity on the Metric Subspace
lemmalem:continuity-metric-subspace-2026aAnalysisA map defined on a subset A of a metric space is continuous at a point relative to A, or continuous on A, exactly when it is continuous at that point, or continuous, as a map from A with the restricted metric.A Finite Sum of Nonnegative Real Numbers in [0,∞] Is Their Real Sum
helperhlp:finite-sum-forms-2026aAnalysisA finite sum of nonnegative real numbers formed in [0,∞] equals the same sum formed in the real numbers, and so is a real number.Sets and Functions Defined Componentwise on Families of Vector- and Matrix-Valued Functions
helperhlp:component-map-families-2026aAnalysisLinear AlgebraFor a set of maps from a set S into R^q, or into the real p x q matrices, the maps all of whose components, or entries, lie in a given set form exactly one set, and applying a map to every component, or entry, defines exactly one map on that set.The Functions f ↦ f⁺ and f ↦ f⁻ on the Real-Valued Functions on a Set, and a Predicative Form of g = f⁺ and g = f⁻
helperhlp:positive-negative-part-maps-2026aAnalysisFor a set X, the positive and negative parts are maps on the set of real-valued maps on X, the conditions g = f⁺ and g = f⁻ are expressed by predicative formulas, and z = max{a,0} is characterized by order conditions.- The integral over a measurable set A is the integral of the map multiplied by the indicator of A; it reduces to the ordinary integral when A is the whole space, exists for integrable maps, is additive over disjoint sets, increases with A for nonnegative maps, and vanishes on sets…
Integrals of Functions over a Measurable Subset
definitiondef:integral-over-measurable-subset-2026aAnalysisRestricts a measure space to a measurable subset A and defines the integral over A of a nonnegative measurable function, and of a real-valued function integrable on A, as the integral of its restriction to A.Rules for Integrals of Vector- and Matrix-Valued Functions
lemmalem:lebesgue-integral-vector-matrix-2026aAnalysisLinear AlgebraA measurable vector- or matrix-valued map is integrable exactly when its norm is; the integral is linear, commutes with multiplication by constant matrices and with dot products by constant vectors, and its norm is at most the integral of the norm.Positive Part, Negative Part and Absolute Value of a Real-Valued Function
definitiondef:positive-negative-parts-2026aAnalysisFor a real-valued function f on a set, defines its positive part f⁺ = max{f, 0}, its negative part f⁻ = max{−f, 0} and its absolute value |f|, all pointwise; each is also a function into [0,∞].Integrable Vector- and Matrix-Valued Functions and Their Integrals
definitiondef:lebesgue-integral-vector-matrix-2026aAnalysisLinear AlgebraA measurable function into ℝⁿ or into the real p×q matrices is integrable when all its components or entries are integrable, and its integral is formed componentwise or entrywise.The Strict Level Sets of a Sequence of Nonnegative Measurable Maps above a Simple Function Form a Sequence of Measurable Sets
helperhlp:strict-level-set-sequences-2026aFor a simple function t and a sequence of nonnegative measurable maps f_m, the sets where t lies strictly below f_m are measurable and form exactly one sequence of measurable sets.The Integers Lying in a Bounded Real Interval Form a Finite Set
helperhlp:integers-in-real-intervals-2026aFor real numbers a and b, the integers read in the real numbers that lie between a and b form a finite subset of the reals.Evaluating a Sequence of Maps at a Point Gives a Sequence, and Its Range
helperhlp:evaluation-sequences-2026aAnalysisFor a sequence of maps from X to Y and a point x of X, the values at x form exactly one sequence in Y, and its range is the set of these values.Unions and Intersections over a Countable Index Term of Terms with Values in a σ-Algebra Are Again Such Terms
helperhlp:countable-operations-terms-2026aIf t is a term of type 𝓕, a σ-algebra, under a guard that adds i ∈ I to γ, with I a term whose values are subsets of a fixed countable set, then the union of t over i ∈ I, and its intersection when I is never empty, is a term of type 𝓕 under γ; this lets nested countable unions…Rational Tuples and Rational Matrices Approximating a Real Tuple or Matrix from Below and Above in Every Component
lemmalem:rational-approximation-tuples-2026aFor a point of ℝⁿ, or a real p×q matrix, and a real δ>0 there are rational tuples, respectively tuples of rational tuples, whose components lie within δ strictly below, respectively strictly above, the corresponding components.The Set of Coordinate Preimages of Borel Sets in ℝⁿ and of Entry Preimages in the Real Matrices
helperhlp:coordinate-preimage-families-2026aThe sets π_i⁻¹(B), with i ∈ [n] and B a Borel subset of ℝ, form a set of subsets of ℝⁿ, and the sets E_ij⁻¹(B) form a set of subsets of the real p×q matrices; both are formed by set-builder from a predicative condition.Operations over the Finite Images of Maps, and the Summands of the Simple Integral
helperhlp:finite-sums-over-images-2026aAnalysisFor a set of maps with finite images, taking the operation over each image of a given summand map defines a map on that set; and for a measure and a set of maps whose level sets are measurable, the summands c times the measure of the level set at c form a map.- For a map g from a set X into [0,∞] and m in ℕ, the dyadic approximation s_m(g) rounds g(x) down to a multiple of 2^{-m} and truncates at m, with value m where g is infinite; the maps s_m(g) form a sequence of real-valued maps on X.