TheoremBase

Progressive Measurability of the Realized Control with Respect to the Observation Filtration

Statement

Adopt the setting, hypotheses and notation of the realized-control lemma: natural numbers N≥1N\ge1, l≥2l\ge2, l~≥1\tilde{l}\ge1, m≥1m\ge1; a nonempty convex subset A\mathcal{A} of Euclidean space Rm\mathbb{R}^m which is compact for the topology determined by the Euclidean distance, with a real R≥0R\ge0 such that ∣a∣≤R|a|\le R for every a∈Aa\in\mathcal{A}, where ∣⋅∣|\cdot| is the Euclidean norm; a transition-rate family β\beta with control set A\mathcal{A}; an observation-rate family β~\tilde{\beta} with l~\tilde{l} channels; a horizon T>0T>0; an NN-agent driving system (Ω,F,P)(\Omega,\mathcal{F},P); an A\mathcal{A}-valued observation-driven control policy h=(hk)k≥0h=(h_k)_{k\ge0} with record spaces Rk(T)R_k(T) (a notation of the policy definition, unrelated to the bound RR); a solution (σi,Υυ,α)(\sigma^i,\Upsilon^\upsilon,\alpha) on [0,T][0,T] with regular event Ω0\Omega_0, observation counters N~i,υ\tilde{N}^{i,\upsilon} indexed by agents i∈{1,…,N}i\in\{1,\dots,N\} and channels υ∈{1,…,l~}\upsilon\in\{1,\dots,\tilde{l}\}, observation total c~=(c~t)t∈[0,T]\tilde{c}=(\tilde{c}_t)_{t\in[0,T]}, observation-event count Kt=c~tK_t=\tilde{c}_t, observation filtration (Gt)t∈[0,T](\mathcal{G}_t)_{t\in[0,T]} and system filtration (Ftsys)t∈[0,T](\mathcal{F}^{\mathrm{sys}}_t)_{t\in[0,T]}, both filtrations with time index restricted to [0,T][0,T] by clause (vii)(e) of the existence and uniqueness theorem; the event times τj\tau_j and channels υj\upsilon_j (j≥1j\ge1) of claim 1 of the realized-control lemma; the fixed point a0∈Aa_0\in\mathcal{A}; the realized control α^:[0,T]×Ω→A\hat{\alpha}:[0,T]\times\Omega\to\mathcal{A} of claim 2 there; the set UA\mathcal{U}_{\mathcal{A}} of A\mathcal{A}-valued controls with the metric ρ\rho of the weak metrizability and compactness theorem, formed from the sequence (wr)r∈N(w_r)_{r\in\mathbb{N}} fixed in the realized-control lemma; and the convention of claim 3 there by which α^(ω)\hat{\alpha}(\omega) denotes both the path s↦α^(s,ω)s\mapsto\hat{\alpha}(s,\omega) and the element of UA\mathcal{U}_{\mathcal{A}} it represents. For t∈[0,T]t\in[0,T] let B[0,t]\mathcal{B}_{[0,t]} be the trace Borel σ\sigma-algebra on [0,t][0,t] (for t=0t=0 the σ\sigma-algebra {∅,{0}}\{\emptyset,\{0\}\}), let B[0,t]⊗Gt\mathcal{B}_{[0,t]}\otimes\mathcal{G}_t be the product σ\sigma-algebra on [0,t]×Ω[0,t]\times\Omega, and write ∫[0,t]⋅ ds\int_{[0,t]}\cdot\,ds for the Lebesgue integral over the compact interval [0,t][0,t], taken to be 00 for t=0t=0. A real-valued function on Ω\Omega is called Gt\mathcal{G}_t-measurable when it is measurable with respect to Gt\mathcal{G}_t and the Borel σ\sigma-algebra of the real line; progressive measurability and stopping times refer to (Gt)t∈[0,T](\mathcal{G}_t)_{t\in[0,T]} unless another filtration is named; and for a function θ:Ω→R\theta:\Omega\to\mathbb{R} and a real qq we write {θ≤q}\{\theta\le q\} for {ω∈Ω:θ(ω)≤q}\{\omega\in\Omega:\theta(\omega)\le q\}.

Then the following hold.

1. (Null events.) For every t∈[0,T]t\in[0,T]: Gt⊆Ftsys\mathcal{G}_t\subseteq\mathcal{F}^{\mathrm{sys}}_t; every event of F\mathcal{F} of probability zero, and in particular Ω∖Ω0\Omega\setminus\Omega_0, belongs to Gt\mathcal{G}_t; and if XX is a random variable on (Ω,F,P)(\Omega,\mathcal{F},P) and X′X' is a Gt\mathcal{G}_t-measurable random variable with X(ω)=X′(ω)X(\omega)=X'(\omega) for every ω\omega outside some event of F\mathcal{F} of probability zero, then XX is Gt\mathcal{G}_t-measurable.

2. (Event times and channels.) For every j≥1j\ge1 and every q∈[0,T]q\in[0,T] one has {τj≤q}∈Gq\{\tau_j\le q\}\in\mathcal{G}_q. Consequently the function ω↦min⁡(τj(ω),T)\omega\mapsto\min(\tau_j(\omega),T) is a stopping time of (Gt)t∈[0,T](\mathcal{G}_t)_{t\in[0,T]}. Moreover, for every t∈[0,T]t\in[0,T], every j≥1j\ge1 and every channel υ∈{1,…,l~}\upsilon\in\{1,\dots,\tilde{l}\},

{τj≤t}∩{υj=υ}∈Gt.\{\tau_j\le t\}\cap\{\upsilon_j=\upsilon\}\in\mathcal{G}_t .

3. (Progressive measurability of the realized control.) Every component α^κ\hat{\alpha}^\kappa (κ∈{1,…,m}\kappa\in\{1,\dots,m\}) of the realized control is progressively measurable with respect to (Gt)t∈[0,T](\mathcal{G}_t)_{t\in[0,T]}, hence also with respect to (Ftsys)t∈[0,T](\mathcal{F}^{\mathrm{sys}}_t)_{t\in[0,T]}; in particular, for every t∈[0,T]t\in[0,T], the restriction of α^κ\hat{\alpha}^\kappa to [0,t]×Ω[0,t]\times\Omega is measurable with respect to B[0,t]⊗Gt\mathcal{B}_{[0,t]}\otimes\mathcal{G}_t and the Borel σ\sigma-algebra of the real line, and α^κ(t,⋅)\hat{\alpha}^\kappa(t,\cdot) is Gt\mathcal{G}_t-measurable.

4. (Truncated realized controls.) For t∈[0,T]t\in[0,T] define α^(t):[0,T]×Ω→A\hat{\alpha}^{(t)}:[0,T]\times\Omega\to\mathcal{A} by α^(t)(s,ω)=α^(s,ω)\hat{\alpha}^{(t)}(s,\omega)=\hat{\alpha}(s,\omega) for s≤ts\le t and α^(t)(s,ω)=a0\hat{\alpha}^{(t)}(s,\omega)=a_0 for s>ts>t. Then for every ω∈Ω\omega\in\Omega the path s↦α^(t)(s,ω)s\mapsto\hat{\alpha}^{(t)}(s,\omega) is an admissible representative, in the sense of claim 2 of the flow stability lemma, of an element of UA\mathcal{U}_{\mathcal{A}}, also written α^(t)(ω)\hat{\alpha}^{(t)}(\omega), and the paths α^(t)(ω)\hat{\alpha}^{(t)}(\omega) and α^(ω)\hat{\alpha}(\omega) agree at every s∈[0,t]s\in[0,t]; for every ζ∈UA\zeta\in\mathcal{U}_{\mathcal{A}} the map ω↦ρ(α^(t)(ω),ζ)\omega\mapsto\rho\bigl(\hat{\alpha}^{(t)}(\omega),\zeta\bigr) is Gt\mathcal{G}_t-measurable; and the map ω↦α^(t)(ω)\omega\mapsto\hat{\alpha}^{(t)}(\omega) is measurable with respect to Gt\mathcal{G}_t and the Borel σ\sigma-algebra of the metric space (UA,ρ)(\mathcal{U}_{\mathcal{A}},\rho).

5. (The control energy process.) Let A:[0,T]→AA:[0,T]\to\mathcal{A} be a map each of whose components is measurable with respect to B[0,T]\mathcal{B}_{[0,T]} and the Borel σ\sigma-algebra of the real line. Then the family (∣α^(s,⋅)−As∣2)s∈[0,T]\bigl(|\hat{\alpha}(s,\cdot)-A_s|^2\bigr)_{s\in[0,T]} is progressively measurable and bounded by 4R24R^2, and

Et(ω)=∫[0,t]∣α^(s,ω)−As∣2 ds(t∈[0,T], ω∈Ω)\mathcal{E}_t(\omega)=\int_{[0,t]}\bigl|\hat{\alpha}(s,\omega)-A_s\bigr|^2\,ds\qquad(t\in[0,T],\ \omega\in\Omega)

defines a family E=(Et)t∈[0,T]\mathcal{E}=(\mathcal{E}_t)_{t\in[0,T]} of [0,4R2T][0,4R^2T]-valued functions on Ω\Omega which is progressively measurable with respect to (Gt)t∈[0,T](\mathcal{G}_t)_{t\in[0,T]}, with Et\mathcal{E}_t Gt\mathcal{G}_t-measurable for every tt, and such that 0≤Et(ω)−Et0(ω)≤4R2(t−t0)0\le\mathcal{E}_t(\omega)-\mathcal{E}_{t_0}(\omega)\le4R^2(t-t_0) for all 0≤t0≤t≤T0\le t_0\le t\le T and every ω∈Ω\omega\in\Omega; in particular every path t↦Et(ω)t\mapsto\mathcal{E}_t(\omega) is nondecreasing and continuous on [0,T][0,T], the interval and the real line carrying the metric of the real line.

Proofs

Log in to submit a proof.

Loading...

Citations

Loading…

Dependencies

Loading…

Related

0 relations

Curated associations between results. These are editable and subjective — they do not replace the dependency graph, which is derived from the references in the text.

No relations recorded yet.

Comments

Log in to comment.

Loading…