Reason: Carried onto lem:closed-loop-feedback-control-2026b. References bumped to standing successors; metric continuity convention stated inline; entry bounds rerouted to thm:extreme-value-closed-interval-2026a and the uniqueness argument to lem:gronwall-integral-inequality-2026b. No mathematical change.
Proof
Throughout, a real-valued function on a subinterval I of the real numbersR is called continuous on I when it is continuous relative to I, both I and the codomain R carrying the metric of the real line.
Claim 1: existence. Define y(0):=mf and y(n+1):=Ty(n). Let dnβ(t):=βiββ₯yt(n+1),iββyt(n),iββ₯2β and D0β:=maxtβd0β(t) (finite by continuity and Extreme Value Theorem on a Closed Real Interval). By (β) and induction, dnβ(t)β€D0βCntn/n! for all n,t: the case n=0 is the definition, and dn+1β(t)β€Cβ«0tβdnβ(r)drβ€D0βCn+1tn+1/(n+1)! by monotonicity of the integral. Since βnβD0βCnTn/n! converges (it is dominated by the exponential series, cf. Basic Properties of the Exponential Function), for each fixed t and i the sequence (yt(n),iβ)nβ is Cauchy in mean square, hence converges to a square-integrable random variable (Xtββ)i by Mean-Square Completeness of Square-Integrable Random Variables (Riesz-Fischer); fix such versions. The convergence is uniform in t: suptββiββ₯yt(n),iββ(Xtββ)iβ₯2ββ€βnβ²β₯nβsuptβdnβ²β(t)β0. A uniform mean-square limit of componentwise mean-square continuous families is componentwise mean-square continuous, by the standard three-term estimate β₯(Xtββ)iβ(Xsββ)iβ₯2ββ€2suprββ₯yr(n),iββ(Xrββ)iβ₯2β+β₯yt(n),iββys(n),iββ₯2β with the triangle inequality of Cauchy-Schwarz and Triangle Inequalities for the Mean-Square Norm. Passing to the limit in y(n+1)=Ty(n): by (β) applied to y(n) and Xβ, (Ty(n))tββ(TXβ)tβ in mean square componentwise, while yt(n+1)ββXtββ; mean-square limits agree almost surely, so Xtββ=(TXβ)tβ componentwise almost surely, which is the asserted fixed-point identity.
Uniqueness. If y and yβ² both have mean-square continuous components and satisfy the identity, then Ξ΄(t)β€Cβ«0tβΞ΄(r)dr with Ξ΄ continuous as above (families satisfying the identity may be replaced, time by time, by the almost surely equal right-hand sides without changing Ξ΄), so Ξ΄β‘0: since T>0 by the standing hypothesis of Linear-Gaussian State-Observation Model, Gronwall's Lemma (Integral Form) applies to the continuous function Ξ΄ on [0,T] with a=0 and b=Cβ₯0, giving Ξ΄(t)β€0β exp(Ct)=0, while Ξ΄β₯0. Hence the families agree almost surely at each time.
the last equality being the definition of the controlled observation integral in Integrals Against the Controlled Observations and the Controlled Filter Equation with f=Ξ¨ΛK (continuous entries). Let Stββ denote the closed mean-square span of {1}βͺ{uqΞ±β,jβ:0β€qβ€t}. By claim 2 of Integrals Against the Controlled Observations and the Controlled Filter Equation, each component of β«0tβΞ¨ΛKdurΞ±ββ is a mean-square limit of finite linear combinations of values of uΞ±β up to time t, hence lies in Stββ; adding the constant tuple E[ΞΎ] (a multiple of 1) and applying Ξ¦Λ(t) keeps us in Stββ (claim 1 of The Closed Mean-Square Span of a Family of Random Variables, and membership is preserved under almost sure equality since approximating combinations converge to any almost surely equal variable as well). Hence (Xtββ)iβStββ, and therefore also Ξ±tβΞΊβ=βiβΞΞΊiβ(t)(Xtββ)iβStββ.
Next, with c and Ξ³ the correction processes for Ξ±β: as in claim 2, ctβ=Ξ¦(t)β«0tβΞ¨BΞXrββdr almost surely, and the Riemann-sum argument of claim 1, now run in Stββ, shows ctiββStββ; the same argument applied to Ξ³tβ=β«0tβE~(r)crβdr gives Ξ³tjββStββ for every j (using criββSrβββStββ). By claim 4 of Superposition Decomposition of the Controlled State and Observations, urjβ=urΞ±β,jββΞ³rjβ almost surely for rβ€t, and the right-hand side lies in Stββ; membership passes to almost surely equal variables, so urjββStββ. Finally, the generators 1 and uqΞ±β,jβ of Stββ are GtΞ±ββ-measurable and square-integrable, so by claim 2 of The Closed Mean-Square Span of a Family of Random Variables every member of Stββ is almost surely equal to a GtΞ±ββ-measurable random variable. This proves all assertions of claim 3. β‘