Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
A Composition of Maps Between Euclidean Open Sets is of Class
theoremthm:ck-composition-euclidean-2026aAnalysisMultivariable CalculusLet , and be natural numbers, let be the real numbers, let be an open subset of Euclidean space and let be an open subset of . Let satisfy for every , let…Constants, Coordinate Functions, Sums and Products of Functions on a Euclidean Open Set
lemmalem:ck-algebra-euclidean-2026aAnalysisMultivariable CalculusLet be a natural number, let be the real numbers, let be an open subset of Euclidean space , let , and let . Write , and for the pointwise sum, scalar multiple and product on , given by…Convolution with a Kernel is of Class
theoremthm:convolution-smooth-2026aAnalysisMultivariable CalculusLet , , , , , the set and the convolution be as in Convolution of a Continuous Function with a Compactly Supported Continuous Kernel. By claim 2 of Differentiating a Convolution through the Kernel the set is…Differentiating a Convolution through the Kernel
lemmalem:convolution-partial-derivative-2026aAnalysisMultivariable CalculusLet , , , , , the set and the convolution be as in Convolution of a Continuous Function with a Compactly Supported Continuous Kernel, let be the Euclidean norm on and let denote the…Partial Derivatives, Continuity and Regularity under a Scaling Substitution
lemmalem:partial-derivative-affine-substitution-2026aAnalysisMultivariable CalculusLet be natural numbers and let be the real numbers, with absolute value . Regard Euclidean space as a real vector space, and let be the Euclidean norm and the Euclidean distance, a metric on .…Progressive Measurability: Sections, Right-Continuous Adapted Processes, Arithmetic, and Indefinite Time Integrals
lemmalem:progressive-measurability-toolkit-2026aProbabilityLet be the real numbers, let be a probability space, let be real, and let be a filtration on with time index restricted to . Progressive measurability of a family…- Let be a probability space, let be a real number, and let be a filtration on with time index restricted to . For let be the trace Borel -algebra…
Arithmetic, Absolute Values, and Pointwise Limits of Measurable Real-Valued Functions
lemmalem:measurable-real-arithmetic-2026aAnalysisLet be the real numbers and let be a measurable space. A real-valued function on is called measurable when it is measurable with respect to and the Borel -algebra . Let and be measurable rea…Existence and Equality of the Reversed Mixed Second Partial Derivative
theoremthm:mixed-partials-symmetry-existence-2026aAnalysisMultivariable CalculusLet be a natural number, let be the real numbers, let be an open subset of Euclidean space , let , let , and let and satisfy and , index ranges using the order on the natural numbers…Multi-Index Partial Derivatives of a Map and of a Smooth Map
theoremthm:ck-multi-index-partials-2026aAnalysisMultivariable CalculusLet and be natural numbers, let be the real numbers, let be an open subset of Euclidean space , let have coordinate functions , and let be a multi-index of length , of…Coordinate Functions, the Hierarchy, and Partial Derivatives of a Smooth Map
lemmalem:ck-map-basic-properties-2026aAnalysisMultivariable CalculusLet and be natural numbers, let be the real numbers, let be an open subset of Euclidean space , let have coordinate functions , and let be a natural number. Index ranges such a…Peeling the Innermost Variable from a Multi-Index Partial Derivative
lemmalem:multi-index-partial-innermost-2026aAnalysisMultivariable CalculusLet be a natural number, let be the real numbers, let be an open subset of Euclidean space , and let . Let be a multi-index of length with , with the zero multi-index , t…Jacobian Determinant on a Euclidean Open Set
definitiondef:jacobian-determinant-euclidean-2026aAnalysisLinear AlgebraMultivariable CalculusLet be a natural number, let be the real numbers, let be an open subset of Euclidean space , let , and let . Suppose that the Jacobian matrix is defined; it is then a real matrix with rows and colu…Partial Derivative of a Multi-Index on a Euclidean Open Set
definitiondef:partial-derivative-multi-index-2026aAnalysisMultivariable CalculusLet and be natural numbers, let be the real numbers, let be an open subset of Euclidean space , and let be a multi-index of length , with the zero multi-index , the standard basis multi-indices…Smooth Map on a Euclidean Open Set
definitiondef:smooth-map-euclidean-2026bAnalysisMultivariable CalculusLet and be natural numbers, let be the real numbers, let be an open subset of Euclidean space , and let . We say that is smooth on if is of class on for every natural number . A function…A Map into a Euclidean Space is Differentiable at Every Point
corollarycor:c1-vector-differentiable-2026aAnalysisMultivariable CalculusLet and be natural numbers, let be an open subset of Euclidean space , let with coordinate functions , and let . Suppose that is of class on , in the sense of clause 1 of…Chain Rule for Differentiable Maps Between Euclidean Spaces
theoremthm:chain-rule-differentiable-euclidean-2026aAnalysisMultivariable CalculusLet , and be natural numbers, let be an open subset of Euclidean space , and let be an open subset of . Let satisfy for every , let , and let de…Linearity, Compatibility with the Matrix Product, and a Norm Bound for the Matrix-Vector Product
lemmalem:matrix-vector-product-properties-2026aAnalysisLinear AlgebraMultivariable CalculusLet , and be natural numbers and let be the real numbers, an ordered field with additive identity and order ; write for the absolute value of . Let be a real matrix with rows and columns, its entry in row and…Jacobian Matrix of a Local Smooth Extension on an Admissible Domain
lemmalem:smooth-extension-jacobian-2026aMultivariable CalculusLet and be natural numbers, let be an admissible domain in Euclidean space in the sense of Continuous n-Form, Support, and Zero Extension on a Euclidean or Half-Space Domain, and let . For a map into and…- Let be the real numbers, and let denote the absolute value on . Let and be intervals, let satisfy for every , and let . Let be the function…