Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Componentwise Estimates, Transpose Identities, and Indefinite Riemann Integrals
lemmalem:componentwise-calculus-toolkit-2026bAnalysisLinear AlgebraLet be natural numbers. For in the Euclidean space write with the Euclidean distance , so that ; for a real matrix write for the Euclidean norm of the tuple of its entries and…Continuity and Derivative of the Inverse of a Matrix-Valued Map
lemmalem:matrix-inverse-continuity-2026cAnalysisLinear AlgebraFor a map from an interval into invertible square matrices, the inverse map is continuous wherever the map is, preserves symmetric positive definiteness, and is differentiable wherever the map is, with derivative minus the inverse times the derivative times the inverse.The Filter Riccati Equation: Global Existence and Uniqueness, Symmetry, and the Lyapunov Bound
theoremthm:riccati-global-existence-2026cAnalysisLinear AlgebraFor continuous coefficients with symmetric positive semidefinite source and quadratic coefficient and a symmetric positive semidefinite initial value, the forward (filter) Riccati initial value problem has exactly one solution on the whole interval; it is symmetric, lies between…The Lyapunov Differential Equation: Well-Posedness, Representation, Symmetry, Positive Semidefiniteness, Comparison and the Backward Equation
lemmalem:lyapunov-equation-psd-2026cAnalysisLinear AlgebraThe forward Lyapunov equation P'=AP+PA^T+C, P(a)=P_0, and the backward equation Z'=-(A^TZ+ZA+Q), Z(b)=F, have exactly one solution each, given by state-transition-matrix formulas, which preserve symmetry, positive semidefiniteness and the semidefinite ordering of the data.- Let be a natural number and let be a positive semidefinite real matrix with entries . 1. for every , and for all , with the nonnegative square root,…
- Let be a natural number and let and be symmetric real matrices. We write if the difference , formed entrywise — which is itself symmetric, since with the…
Positive Semidefinite and Positive Definite Real Matrices
definitiondef:positive-semidefinite-matrix-2026dLinear AlgebraA symmetric real n x n matrix A is positive semidefinite if x·(Ax) is nonnegative for every x in R^n, and positive definite if x·(Ax) is positive for every nonzero x.Variation of Constants for Linear Systems
theoremthm:fundamental-solution-linear-ode-2026cAnalysisLinear AlgebraThe solution of the linear initial value problem x'=A(t)x+g(t), x(a)=ξ, on [a,b] is Φ(t,a)ξ plus the integral from a to t of Φ(t,r)g(r), with Φ the state-transition matrix of A; likewise for matrix-valued unknowns.A Priori Bounded Initial Value Problems with Locally Lipschitz Right-Hand Side Have Exactly One Solution on the Whole Interval
theoremthm:ode-a-priori-bound-global-2026cAnalysisIf the right-hand side is continuous and locally Lipschitz in the state, and every solution on every initial subinterval [a,c] is bounded in norm by a fixed ρ, then the initial value problem has exactly one solution on [a,b], bounded by ρ; for vectors and for matrices.The Picard–Lindelöf Theorem on a Closed Interval: Existence, Uniqueness and Continuous Dependence for Globally Lipschitz Systems
theoremthm:picard-lindelof-global-2026cAnalysisFor a continuous right-hand side that is globally Lipschitz in the state, the initial value problem on [a,b] has exactly one solution, for vectors and for matrices, and solutions depend on the initial value with the bound ‖ξ−η‖exp(L(t−a)).Completeness of the Space of Continuous Vector-Valued Functions under the Supremum Metric
lemmalem:continuous-vector-functions-complete-2026bAnalysisTopologyLet be real numbers and let be a natural number. Let denote the set of all functions (Euclidean space) whose component functions are continuous on , the interval being regarded as…Wiener Integrals Against a Vector Brownian Motion are Jointly Gaussian
theoremthm:vector-wiener-integral-gaussian-2026bProbabilityThroughout, a real-valued function on a subinterval of the real numbers is called continuous on when it is continuous relative to , both and the codomain carrying the metric of the real line. Let be a…Independent Jointly Gaussian Families are Jointly Gaussian
lemmalem:independent-gaussian-families-jointly-gaussian-2026aProbabilityLet be a probability space, let be a natural number, and for each let be a nonempty set and let be a jointly Gaussian family of random variables on . Suppose that the…- Let be a probability space and let be a natural number. An -dimensional Brownian motion on is a family of stochastic processes on such that:…
Integration by Parts for Wiener Integrals and Mean-Square Riemann Integrals
lemmalem:stochastic-integration-by-parts-2026bProbabilityThroughout, a real-valued function on a subinterval of the real numbers is called continuous on when it is continuous relative to , both and the codomain carrying the metric of the real line. Let be a…Mean-Square Riemann Integrals of a Jointly Gaussian Family are Jointly Gaussian
lemmalem:mean-square-riemann-integral-gaussian-2026aProbabilityLet be a probability space, let be real numbers, let be a set (possibly empty), and let be a family of random variables on . Let be a mean-square continuous family of square-integrable…Basic Properties of the Mean-Square Riemann Integral
lemmalem:mean-square-riemann-integral-properties-2026bProbabilityLet be a probability space, let be the real numbers, let be real numbers, and let and be mean-square continuous families of square-integrable random variables on , with…Existence and Uniqueness of the Mean-Square Riemann Integral for Mean-Square Continuous Families
lemmalem:mean-square-riemann-integral-existence-2026aProbabilityLet be a probability space and let be real numbers. 1. (Uniqueness) Let be any family of square-integrable random variables on . If and are both mean-square Riemann integrals of…Mean-Square Riemann Integral of a Family of Random Variables
definitiondef:mean-square-riemann-integral-2026aProbabilityLet be a probability space, let be real numbers, and let be a family of square-integrable random variables on , with the mean-square norm of that definition. Let…Wiener Integrals of Continuous Functions are Jointly Gaussian
theoremthm:wiener-integral-gaussian-2026bProbabilityThroughout, a real-valued function on a subinterval of the real numbers is called continuous on when it is continuous relative to , both and the codomain carrying the metric of the real line. Let be a…