Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- The reflection u maps to a+b-u of a closed interval [a,b] into itself is a well-defined involutive isometry, continuous, and differentiable with derivative -1.
Continuity of Projections, Negatives and Differences, and Derivatives on Subintervals
lemmalem:continuity-projections-restrictions-2026aAnalysisLinear AlgebraThe coordinate projections of a product metric space are continuous on every subset, and so is a continuous map of the first coordinate; negatives and differences of continuous vector- and matrix-valued maps are continuous; and a differentiable vector- or matrix-valued map on [a,…Integrals Preserve Order, Symmetry and Positive Semidefiniteness
lemmalem:matrix-integral-order-2026aAnalysisLinear AlgebraOriented integrals of real maps with ordered bounds are monotone in the integrand; the integral of a continuous map with symmetric matrix values is symmetric, positive semidefinite when the integrand is and the bounds are in order, and integration preserves the semidefinite order…Maps Formed Pointwise from Vector and Matrix Operations
helperhlp:pointwise-matrix-maps-2026aAnalysisLinear AlgebraSums, scalar multiples, negatives, differences, products, matrix-vector products, transposes and inverses of matrix- and vector-valued maps on a set, taken pointwise, are well-defined maps.Ordinary Differential Equations on a Compact Interval: Standing Notation
settingset:ode-2026aAnalysisCollects, by reference, the calculus of vector- and matrix-valued maps on [a,b], the initial value problem and its solutions, the state-transition matrix, the matrix exponential, and the Lyapunov and Riccati equations, with their background results.Time Reversal: Terminal Value Problems as Initial Value Problems
lemmalem:time-reversal-2026aAnalysisReversing time by u ↦ a+b-u turns the terminal value problem x' = F(t,x), x(b) = ξ on [a,b] into the initial value problem y' = -F(a+b-u,y), y(a) = ξ, for vectors and matrices, so that a continuous globally Lipschitz F gives exactly one solution of the terminal value problem.The Riccati Differential Equations of Filtering and Control
equationeq:riccati-equation-2026aAnalysisNames the filter Riccati equation P' = AP + PAᵀ - PDP + C with P(a) = P₀, as a matrix initial value problem on [a,b], and the control Riccati equation Z' = -(AᵀZ + ZA - (ZB+V)R⁻¹(ZB+V)ᵀ + Q) with terminal value Z(b) = F.- Names the Lyapunov differential equation P' = AP + PAᵀ + C with initial value P(a) = P₀, as a matrix initial value problem on [a,b], and its backward form Z' = -(AᵀZ + ZA + Q) with terminal value Z(b) = F.
Additive Laws for Vectors in and for Real Matrices: Group Laws and Rules for Differences
helperhlp:additive-laws-vectors-matrices-2026aLinear AlgebraVectors in R^q and real p x q matrices form an abelian group under addition, and their differences obey the usual rearrangement rules.Shifted Power Maps, and Integrating a Power Bound on the Derivative of a Matrix-Valued Map
lemmalem:integrated-power-bound-2026aAnalysisThe maps r -> (r-s)^N/N! on [a,b] are differentiable, each the derivative of the next; and a matrix-valued map vanishing at s whose continuous derivative is bounded in norm by c|r-s|^N/N! is bounded in norm by c|t-s|^(N+1)/(N+1)!.Products of Real Matrices with Zero Matrices, Negatives and Differences
lemmalem:matrix-product-differences-2026aLinear AlgebraMatrix products and matrix-vector products vanish when a factor is zero, commute with negation, and distribute over differences.- The matrix exponential maps the zero matrix to the identity, commutes with transposition and with matrices commuting with the exponent, satisfies e^{(s+t)M} = e^{sM} e^{tM}, is invertible with inverse e^{-M}, has derivative M e^{tM} in t, and satisfies e^{A+B} = e^A e^B for commu…
The State-Transition Matrix of a Constant Coefficient Matrix Is a Matrix Exponential
lemmalem:matrix-exponential-transition-2026aAnalysisFor the constant coefficient map t -> M on [a,b], the state-transition matrix is Phi(t,s) = e^{(t-s)M} for all s and t in [a,b].- The exponential e^M of a real square matrix M is the matrix whose entries are the sums of the series of (M^k)_ij/k!; it is the limit of the partial sums of M^k/k! and has norm at most exp of the norm of M.
The Exponential Series of a Real Square Matrix: Convergence, a Norm Bound and the Exponential Map
lemmalem:matrix-exponential-series-2026aAnalysisFor a real square matrix M, each entry series of the sum of M^k/k! converges absolutely, the partial sums converge in the operator-norm distance to the matrix of entry sums, whose norm is at most exp of the norm of M, and the limit depends on M through a map.- Powers of a real square matrix satisfy the recursion, add exponents, commute with matrices commuting with the base, pull out scalars, commute with transposition, and have norm at most the corresponding power of the norm.
Basic Properties of the State-Transition Matrix
lemmalem:state-transition-matrix-properties-2026aAnalysisThe state-transition matrix Φ of a continuous A gives all solutions of x'=A(t)x through Φ(t,s)ξ, satisfies Φ(t,r)Φ(r,s)=Φ(t,s) and Φ(t,s)^{-1}=Φ(s,t), is jointly continuous, has s-derivative -Φ(t,s)A(s), is bounded by exp(K|t-s|), transposes to the transition matrix of -Aᵀ and re…- Names Φ_A, the unique map on [a,b]×[a,b] with ∂Φ_A(t,s)/∂t=A(t)Φ_A(t,s) and Φ_A(s,s)=I_n, the state-transition matrix of a continuous A on [a,b].
Existence and Uniqueness of the State-Transition Matrix of a Linear System
lemmalem:state-transition-matrix-existence-2026aAnalysisFor a continuous A on [a,b], a solution of X'=A(t)X vanishing at one point vanishes everywhere, and there is exactly one map Φ on [a,b]×[a,b] with ∂Φ(t,s)/∂t=A(t)Φ(t,s) and Φ(s,s)=I_n.Linear Systems with Continuous Coefficients: Continuity, Global Lipschitz Bound and Well-Posedness of the Initial Value Problem
lemmalem:linear-system-well-posed-2026aAnalysisFor continuous coefficients on [a,b], the linear right-hand sides A(t)x+g(t) and A(t)X+XB(t)+G(t) are continuous, globally Lipschitz in the state with constant a bound of the coefficient norms, and their initial value problems have exactly one solution.