Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- Elementwise identities for products of sets, for sections of subsets of a product under complements, countable unions and intersections, for sections as preimages under the insertion functions, and for preimages under the swap of the factors.
- For a bijection f from X to Y with inverse g and a subset E of X, the image f[E] is the preimage of E under g, and the preimage of f[E] under f is E.
- The open box R(a,b) in ℝⁿ is the set of points whose i-th component lies strictly between a_i and b_i for every i; R_n is the set of all open boxes of ℝⁿ.
Linear Change of Variables for Lebesgue Measure on ℝⁿ
theoremthm:linear-change-of-variables-2026aAnalysisFor an invertible matrix A and a vector b, the affine map T(x)=Ax+b multiplies Lebesgue measure on ℝⁿ by |det A|, its image measure is |det A|⁻¹λₙ, and integrals of nonnegative and of integrable functions transform accordingly.Translation-Invariant Measures on ℝⁿ Are Multiples of Lebesgue Measure
lemmalem:translation-invariant-measures-euclidean-2026aAnalysisA translation-invariant measure on the Borel sets of ℝⁿ that is finite on the open unit cube is c times Lebesgue measure, where c is the measure of that cube.Product Measures, Lebesgue Measure on ℝⁿ and Image Measures: Notation
settingset:product-notation-2026aAnalysisNotation for products of measure spaces, sections, product measures, image measures, measures with a density, Lebesgue measure on ℝⁿ, open boxes, and images of sets under translations, reflections, scalings and matrices.Lebesgue Measure on ℝ^{m+n} as the Product of Lebesgue Measures on ℝ^m and ℝ^n
lemmalem:lebesgue-euclidean-products-2026aAnalysisAssuming dependent choice, Lebesgue measure on ℝ¹ is the copy of Lebesgue measure on ℝ, and Lebesgue measure on ℝ^{m+n} is the image of the product of Lebesgue measures on ℝ^m and ℝ^n under concatenation; hence integrals over ℝ^{m+n} are iterated integrals, for nonnegative and fo…Null Sets of a Product Measure, and Exchanging the Factors
lemmalem:product-measure-properties-2026aAnalysisProbabilityA product-measurable set is null for μ⊗ν exactly when almost all of its sections are ν-null, and the image of ν⊗μ under the swap (y,x) ↦ (x,y) is μ⊗ν.- Assuming dependent choice, the open boxes of ℝⁿ form a π-system generating the Borel sets, two measures agreeing and finite on open boxes are equal, and exactly one Borel measure on ℝⁿ gives every nonempty open box its volume.
- The product μ⊗ν of two σ-finite measures is the unique measure on the product σ-algebra with value μ(A)ν(B) on each measurable rectangle A×B, and the product measure space is the product set with the product σ-algebra and this measure.
- For a σ-finite measure ν, the ν-measure of the section at x of a product-measurable set is a measurable function of x, and integrating it against μ gives a measure on the product σ-algebra that takes the value μ(A)ν(B) on each measurable rectangle A×B; μ need not be σ-finite.
Every Invertible Real Matrix Is an Orthogonal Matrix Times a Positive Diagonal Matrix Times an Orthogonal Matrix
lemmalem:invertible-matrix-singular-values-2026aLinear AlgebraAn invertible real square matrix factors as an orthogonal matrix times a diagonal matrix with positive diagonal times the transpose of an orthogonal matrix, and the absolute value of its determinant is the product of those diagonal entries.Borel Sets of ℝ^{m+n} and the Product σ-Algebra of ℝ^m and ℝ^n
lemmalem:borel-euclidean-product-2026aAnalysisProbabilityConcatenation of an m-tuple and an n-tuple is measurable from the product of the Borel σ-algebras of ℝ^m and ℝ^n to the Borel σ-algebra of ℝ^{m+n}, with measurable inverse, so a set of pairs is product-measurable exactly when its concatenated image is Borel; likewise ℝ and ℝ^1 ar…- For a subset E of X×Y, the section at x is the set of y with (x,y) in E and the section at y the set of x with (x,y) in E; for a function f on X×Y, its sections are the functions y↦f(x,y) and x↦f(x,y).
- For a nonnegative measurable function h, the measure with density h with respect to a measure assigns to each measurable set the integral of h over it.
- The image measure of a measure under a measurable function assigns to each measurable set of the target the measure of its preimage.
The Sets Where a Function Is at Least 1/n Form a Sequence of Measurable Sets
helperhlp:reciprocal-superlevel-sequence-2026aFor a nonnegative measurable map f, the superlevel sets {1/n ≤ f}, n a natural number, are the terms of a sequence in the σ-algebra.Darboux Sums Bound the Lebesgue Integral on a Closed Interval
lemmalem:darboux-bounds-lebesgue-integral-2026aA bounded Borel measurable function on a closed interval is Lebesgue integrable, and its Lebesgue integral lies between its lower and upper Darboux sums for every partition.Step Functions on a Partition of a Closed Interval as Simple Functions
helperhlp:partition-step-functions-2026aThe open cells of a partition of [a,b] cover the interval off the partition points; a function with prescribed values on the cells and on the partition points exists; and a nonnegative function constant on each cell is a nonnegative simple function whose simple integral is the su…Bounded Measurable Functions on a Finite Measure Space Are Integrable
lemmalem:bounded-measurable-finite-measure-2026aOn a finite measure space a bounded measurable real function is integrable, and adding its bound gives a nonnegative integrable function whose integral is the integral of the function plus the bound times the total mass.