Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Conditional Expectation and Estimation Error of the Controlled State
lemmalem:controlled-state-conditional-expectation-2026bProbabilityConsider a linear-Gaussian state-observation model on , a control dimension , a control matrix assignment , an admissible control , and the controlled state , with notation and fixed versions as in those items. Let and be…Superposition Decomposition of the Controlled State and Observations
lemmalem:controlled-state-superposition-2026bProbabilityConsider a linear-Gaussian state-observation model on , a control dimension , a control matrix assignment , an admissible control , and the controlled state and observations , , with all notation and fixed versions as in those item…Controlled State and Controlled Observations in the Linear-Gaussian Model
definitiondef:controlled-linear-gaussian-dynamics-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. Consider a…Admissible Control for the Linear-Gaussian State-Observation Model
definitiondef:admissible-control-2026bProbabilityConsider a linear-Gaussian state-observation model on , with notation and fixed versions as there, and let be a natural number. An admissible control with values in for the model is a family , where each…Product Rule and Reflection for Indefinite Riemann Integrals
lemmalem:riemann-product-rule-reflection-2026bAnalysisLet be real numbers. All integrals below are Riemann integrals of continuous functions — each interval being regarded as a subset of the real line with the absolute value metric and carrying the same metric — which exist by claim 3 of…- A positive definite symmetric matrix is invertible, and its inverse is again symmetric and positive definite.
Expected Bilinear Forms: Trace Formula and Mean-Square Continuity
lemmalem:expected-quadratic-form-2026bProbabilityLet be a probability space let be the real numbers, and let be natural numbers. A real-valued function defined on a closed interval is called continuous on when it is continuous relative to …- The trace is linear and invariant under transposition, tr(UV) = tr(VU), and the entrywise sum of U_ij V_ij equals tr(U^T V) and tr(U V^T).
- The trace of a square real matrix is the sum of its diagonal entries.
Mean-Square Limits of Affine Combinations Adjoin to a Jointly Gaussian Family
lemmalem:gaussian-affine-span-closure-2026aProbabilityLet be a probability space, let be a jointly Gaussian family of random variables, and let be a family of square-integrable random variables such that every is a mean-square limit of finite affine combinations of mem…The Closed Mean-Square Span of a Family of Random Variables
lemmalem:mean-square-span-closure-2026aProbabilityLet be a probability space and let be a nonempty family of square-integrable random variables on it. Write , the closed mean-square span of , for the set of all square-integrable random variables fo…The Kalman-Bucy Filter Computes the Conditional Expectation in the Linear-Gaussian Model
theoremthm:kalman-bucy-conditional-expectation-2026bProbabilityConsider a linear-Gaussian state-observation model on , with notation and fixed versions as there, and let , , and the filter process be as in The Kalman-Bucy Filter Equation and Its Solution. Write (componentwise) for the…The Kalman-Bucy Filter Equation and Its Solution
theoremthm:kalman-bucy-filter-solution-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. Consider a…Integrals Against the Observation Process are Determined by the Observations
lemmalem:observation-stieltjes-adapted-2026bProbabilityConsider a linear-Gaussian state-observation model on , with notation and fixed versions as there. Throughout, a real-valued function on a subinterval of the real numbers is called continuous on when it is continuous relative to , both and the c…Gaussian and Span Structure of the Linear-Gaussian State-Observation Model
lemmalem:observation-process-properties-2026bProbabilityConsider a linear-Gaussian state-observation model on , with all notation and fixed versions as there. 1. (Regularity and span structure) Each component family is mean-square continuous and almost surely. Moreover, for every …Linear-Gaussian State-Observation Model
definitiondef:linear-gaussian-state-observation-model-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…Gaussian Structure and Moment Equations for Linear Stochastic Differential Equations
lemmalem:linear-sde-gaussian-covariance-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…Second-Moment Evolution for Processes of Integral Form
lemmalem:second-moment-evolution-2026cProbabilityThroughout, 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…Existence, Uniqueness, and Variation of Constants for Linear Stochastic Differential Equations
theoremthm:linear-sde-variation-of-constants-2026bProbabilityLet be a linear stochastic differential equation with additive Wiener noise on , with dimensions as there, and let and be the fundamental solution of on and its inverse from…Mean-Square Solution of a Linear Stochastic Differential Equation with Additive Wiener Noise
definitiondef:linear-sde-mean-square-solution-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…