Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- Let be the set of real numbers. A function is a counting path if: 1. (Integer values.) and, for every , is either or a natural number. 2. (Monotonicity.) whenever .…
- Let and be natural numbers with and , let be the probability simplex, and let denote Euclidean space. Population cost data on states with control dimension is a pair of functions…
- Let and be natural numbers with and , let be the probability simplex, and let be a nonnegative real number. An observation-rate family on states with observation channels and rate…
- Let and be natural numbers with and , let be the probability simplex, let be a nonempty subset of Euclidean space , called the control set, and let be a nonnegative real number. A…
- Let be a natural number with , and let denote Euclidean space. The probability simplex is the set…
The Separation Theorem over Extended Admissible Controls
theoremthm:lqg-separation-extended-2026bProbabilityConsider a linear-Gaussian state-observation model on , a control dimension , a control matrix assignment , and cost data with every positive definite. Suppose is a symmetric continuous solution of the backward Riccati equation, and let…Conditional Expectation and Estimation Error of the Extended Controlled State
lemmalem:extended-controlled-state-conditional-expectation-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…The Linear-Quadratic-Gaussian Cost of an Extended Admissible Control
definitiondef:extended-lqg-cost-2026bProbabilityConsider a linear-Gaussian state-observation model on , a control dimension , a control matrix assignment , cost data , and an extended admissible control with values in . The linear-quadratic-Gaussian cost of is the re…Controlled State of an Extended Admissible Control
definitiondef:extended-controlled-state-2026bProbabilityConsider a linear-Gaussian state-observation model on with state , a control dimension , a control matrix assignment as in Controlled State and Controlled Observations in the Linear-Gaussian Model, and an extended admissible control with values in…Convergence of Corrections and Costs along Approximating Sequences of an Extended Admissible Control
lemmalem:extended-control-convergence-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…Extended Admissible Control for the Linear-Gaussian State-Observation Model
definitiondef:extended-admissible-control-2026bProbabilityConsider a linear-Gaussian state-observation model on , with notation and fixed versions as there, and let be a natural number. Adopt the notation , of the restricted Lebesgue measure on , and the distance between…Almost-Everywhere Mean-Square Limits of Cauchy Sequences of Admissible Controls
lemmalem:control-sequence-mean-square-limit-2026bProbabilityConsider a linear-Gaussian state-observation model on with observation -algebras , let be a natural number, and let be a sequence of admissible controls with values in for the model. Through…Restricted Lebesgue Measure and Integral Toolkit on a Compact Interval
lemmalem:interval-lebesgue-toolkit-2026bAnalysisProbabilityLet be real numbers, let be the Borel -algebra on , and let be Lebesgue measure, whose domain is by claim 3 of Existence of Lebesgue Measure on the Real Line. Define…The Separation Theorem for Partial-Information Linear-Quadratic-Gaussian Control
theoremthm:lqg-separation-theorem-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…Existence and Self-Consistency of the Closed-Loop Feedback Control
lemmalem:closed-loop-feedback-control-2026bProbabilityConsider the setting of Completion of Squares for the Linear-Quadratic-Gaussian Cost: a linear-Gaussian state-observation model on , a control dimension , a control matrix assignment , cost data with every positive definite, a symmetric continuou…Completion of Squares for the Linear-Quadratic-Gaussian Cost
theoremthm:lqg-completion-of-squares-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 Controlled Observations and the Controlled Filter Equation
lemmalem:controlled-observation-integrals-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…Orthogonal Decomposition of Expected Quadratic Forms under Independence
lemmalem:quadratic-form-independent-decomposition-2026aProbabilityLet be a probability space, let be a natural number, and let be a sub--algebra of . Let and be tuples of square-integrable random variables suc…Brownian Increments After a Time are Independent of the Model Past
lemmalem:brownian-increments-independent-model-past-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…- 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 codomain carrying the metric of the real line. Consider a…