Reason: Proof of P8.4a: flow restriction via the generalized-pair definition and uniqueness, two-horizon identification of the realized control, measurable representation, and transport of the joint law by the copy law identity at horizon s. Two internal review passes; strict validation clean.
Proof
Throughout, the composition g∘f of a map f measurable with respect to F1 and F2 and a map g measurable with respect to F2 and F3 is measurable with respect to F1 and F3, since (g∘f)−1(E)=f−1(g−1(E)) for every set E and measurability is the requirement that preimages of measurable sets be measurable; we use this without further comment. For a map f on [0,T] we write f∣[0,s] for its restriction to [0,s].
Consequently: α^(s) is the map of claim 2 of the realized-control lemma with horizon s, defined from a family furnished by its claim 1; the paths a(s),r are defined by The Record-Frozen Control Path and Record-Frozen Policy for the policy h(s); UA(s) and S(s) are furnished by claim 2 of the flow stability lemma with horizon s; each a(s),r represents an element of UA(s) by claim 1 of the record-frozen control lemma, so that Φt(s),r=St(s)(z0,a(s),r) is the record-frozen flow of its claim 4 with base point z0; α^(s)(ω)∈UA(s) for every ω by claim 3 of the realized-control lemma with horizon s, so that Φt(s)(ω) is defined; the map r↦Φt(s),r,γ is Rs-measurable by claim 5 of the record-frozen control lemma; and W(s) is measurable with respect to F and Rs by claim 1 of The Observation Filtration of a Solution of the Controlled N-Agent Dynamics is Generated, up to Null Sets, by the Observation Record up to that Time.
Claim 2.Measurability of the restriction. Let γ∈{1,…,m} and let E be a Borel subset of the real line. Since uγ is measurable with respect to B[0,T], the set (uγ)−1(E) belongs to B[0,T], so by the definition of B[0,T] in Restricted Lebesgue Measure and Integral Toolkit on a Compact Interval it equals S∩[0,T] for some Borel set S⊆R. Then (uγ∣[0,s])−1(E)=(uγ)−1(E)∩[0,s]=S∩[0,s], which belongs to B[0,s] by the same definition. Hence the components of u∣[0,s] are B[0,s]-measurable, and u∣[0,s] takes its values in A; so claim 1 of Existence and Uniqueness of the Generalized Mean-Field Trajectory for a Measurable Control applies to the horizon s, the initial value x and the control u∣[0,s], and S(s),u∣[0,s] is defined.
The restriction of Su solves the horizon-s equation. Write y=Su∣[0,s]. By claim 1 of the existence theorem, (Su,u) is a generalized mean-field trajectory pair for (β0,β1) with horizon T, with Svu∈Δl for every v and S0u=x. By condition 1 of that definition each component Su,γ is continuous on [0,T], the interval and the real line carrying the metric of the real line; hence each yγ is continuous on [0,s]: given t0∈[0,s] and ε>0, a δ>0 with ∣Stu,γ−St0u,γ∣<ε for all t∈[0,T] with ∣t−t0∣<δ serves in particular for all such t∈[0,s], which is the requirement of continuity of yγ at t0 relative to [0,s]. For every γ∈{1,…,l}, condition 2 of that definition gives, with f(v)=bγ(Svu,uv) for v∈[0,T],
the integral being the Lebesgue integral over the compact interval[0,t]; as recorded in that definition, f is measurable with respect to B[0,T] and bounded in absolute value by Kb=2l(l−1)B (the Euclidean norm bound ∣b∣≤Kb of claim 4 of The Transition-Rate Family and Aggregate Drift of Affine-Controlled Data with the coordinate bound of claim 4 of Elementary Properties of the Euclidean Norm on Rn). Fix t∈(0,s] and γ. The function f1[0,t] on [0,T] is B[0,T]-measurable (claims 1 and 3 of Arithmetic, Absolute Values, and Pointwise Limits of Measurable Real-Valued Functions, [0,t]∈B[0,T]) and integrable with respect to λ[0,T]: ∣f1[0,t]∣≤Kb, the constant Kb has the finite integral Kbλ[0,T]([0,T])=KbT (The Integral of an Indicator Function is the Measure of the Set, positive homogeneity in Linearity and Monotonicity of the Lebesgue Integral, claim 1 of the toolkit), so ∣f1[0,t]∣ has finite integral by monotonicity of the integral, which is integrability. Let g:R→R be the function equal to f on [0,t] and to 0 elsewhere. Then g is the zero extension of each of the three functions f1[0,t] on [0,T], f∣[0,s]1[0,t] on [0,s] and f∣[0,t] on [0,t], because [0,t]⊆[0,s]⊆[0,T]. By claim 2 of the toolkit applied on [0,T], g is Borel measurable and integrable with respect to Lebesgue measure λ, with ∫[0,T]f1[0,t]dλ[0,T]=∫Rgdλ; by the same claim applied on [0,s] and on [0,t] in the converse direction, f∣[0,s]1[0,t] is B[0,s]-measurable and integrable with respect to λ[0,s], f∣[0,t] is B[0,t]-measurable and integrable with respect to λ[0,t], and
(This chain shows that the three readings of an integral over [0,t] --- as an integral of the restriction with respect to λ[0,t], or of the integrand multiplied by the indicator of [0,t] with respect to λ[0,s] or to λ[0,T] --- agree, so the identity below does not depend on which reading of condition 2 is adopted.) Since f(v)=bγ(yv,u∣[0,s](v)) for v∈[0,s], the restriction to [0,t] of the map v↦bγ(yv,u∣[0,s](v)) on [0,s] is f∣[0,t], and the display for Stu,γ shows
ytγ=xγ+∫[0,t](v↦bγ(yv,u∣[0,s](v)))[0,t]dλ[0,t]for all t∈(0,s],γ∈{1,…,l},
the right-hand side being the Lebesgue integral over the compact interval [0,t] of the integrand required in condition 2 of the definition of a generalized mean-field trajectory pair with horizon s (for t=0, where that condition reads y0γ=xγ by its convention that the integral is 0, it holds because y0=S0u=x). Together with the continuity of the components of y, its values in Δl, and the B[0,s]-measurability and A-valuedness of u∣[0,s] (first paragraph), this shows that (y,u∣[0,s]) is a generalized mean-field trajectory pair for (β0,β1) with horizon s whose value at t=0 is x. By claim 2 (uniqueness) of the existence theorem with horizon s, applied to the control u∣[0,s] and the initial value x, y=S(s),u∣[0,s]; that is, St(s),u∣[0,s]=Stu for every t∈[0,s].
The class of the restriction. Let ξ∈UA and let u be an admissible representative of ξ: by claim 2 of the flow stability lemma, u is a representative of ξ (hence a square-integrable map [0,T]→Rm in the sense of claim 1 of The Lebesgue Space of Square-Integrable Vector-Valued Functions on a Compact Interval, whose components are therefore B[0,T]-measurable) with u(t)∈A for every t∈[0,T]. By the first paragraph the components of u∣[0,s] are B[0,s]-measurable. Write us=u∣[0,s]. Then ∣us(v)∣≤RA for every v∈[0,s], so the nonnegative B[0,s]-measurable function ∣us∣2 (measurable by claims 3 and 2 of Arithmetic, Absolute Values, and Pointwise Limits of Measurable Real-Valued Functions, being the sum of the squares of the components) is bounded by the constant (RA)2, whose integral with respect to λ[0,s] is (RA)2λ[0,s]([0,s])=(RA)2s by The Integral of an Indicator Function is the Measure of the Set, positive homogeneity of the integral (Linearity and Monotonicity of the Lebesgue Integral) and claim 1 of the toolkit; by monotonicity of the integral∫[0,s]∣us∣2dλ[0,s]≤(RA)2s<∞. Hence us=u∣[0,s] is square-integrable on [0,s]; its values lie in A at every point, so its class [u∣[0,s]] belongs to UA(s) by The Set of Controls with Values in a Prescribed Subset of Euclidean Space (with the empty null set), and u∣[0,s] is an admissible representative of it. By claim 2 of the flow stability lemma with horizon s, S(s)(x,[u∣[0,s]]) is the map S(s),u∣[0,s], and with horizon T, S(x,ξ) is the map Su; the identity St(s)(x,[u∣[0,s]])=St(x,ξ) for t∈[0,s] is therefore the identity just proved.
Claim 3.The realized controls. Let ω∈Ω and t∈[0,s]. If ω∈/Ω0, then α^(t,ω)=a0=α^(s)(t,ω) by the definition in claim 2 of the realized-control lemma at both horizons, the regular event of the restricted solution being Ω0 (claim 2 of Restriction of a Solution of the Controlled N-Agent Dynamics to a Shorter Horizon: the Truncated Policy, the Restricted Solution, Its Filtrations, and Its Record as the Prefix of the Record, or by definition when s=T). If ω∈Ω0, then by claim 2 of the realized-control lemma α^(t,ω)=αt(ω), the value at (t,ω) of the control process of the given solution, and α^(s)(t,ω)=αt(ω), the value of the control process of the restricted solution, which is (αt)t∈[0,s]. Hence α^(s)(t,ω)=α^(t,ω) for all ω∈Ω and t∈[0,s]; that is, the path α^(s)(ω) is the restriction α^(ω)∣[0,s].
The realized flows. Fix ω∈Ω. By claim 3 of the realized-control lemma the path α^(ω) is an admissible representative of the element α^(ω)∈UA, and Φt(ω)=St(z0,α^(ω)). By claim 2 applied to x=z0, ξ=α^(ω) and this representative, St(s)(z0,[α^(ω)∣[0,s]])=Φt(ω) for t∈[0,s]. By the previous paragraph α^(ω)∣[0,s] is the path α^(s)(ω), whose class is the element α^(s)(ω) of UA(s) (claim 3 of the realized-control lemma with horizon s); hence Φt(s)(ω)=St(s)(z0,α^(s)(ω))=Φt(ω) for every t∈[0,s].
The record prefix. Let ω∈Ω0 and t∈[0,s]. Claim 1 of The Realized Control as the Record-Frozen Control at the Observation Record, and Measurability of the Path-and-Record Closeness Set, applied with horizon s (its hypotheses hold by claim 1), to the restricted solution, whose observation record is W(s), gives α^(s)(t,ω)=a(s),W(s)(ω)(t). Since this holds for every t∈[0,s], the path α^(s)(ω) and the path a(s),W(s)(ω) coincide, so they represent the same element of L2([0,s];Rm); therefore Φt(s)(ω)=St(s)(z0,a(s),W(s)(ω))=Φt(s),W(s)(ω), and by the previous paragraph Φt(ω)=Φt(s),W(s)(ω).
Claim 4.Values in the lattice, and the diameter of the simplex. By the derived notation of Solution of the Controlled N-Agent Dynamics, Σtγ(ω)=N1∑i=1Nηti,γ(ω) with each ηti,γ(ω)∈{0,1}, and Σt(ω)∈Δl; thus NΣtγ(ω) is the number of agents i with σti(ω)=γ, which is 0 or a natural number, so Σt(ω)∈GN by the definition of the aggregate lattice, for every ω∈Ω and t∈[0,T]. For x∈Δl one has xγ≥0 and ∑γxγ=1, so ∣x∣2=∑γ(xγ)2≤(∑γxγ)2=1 (claim 1 of Elementary Properties of the Euclidean Norm on Rn; the inequality because the square of a sum of nonnegative numbers is the sum of their squares plus the nonnegative cross terms), hence ∣x∣≤1, and for x,y∈Δl the triangle inequality (claim 6 there, applied to x−y=x+(−y), with ∣−y∣=∣y∣ by claim 5) gives ∣x−y∣≤∣x∣+∣y∣≤2.
The representation. For ω∈Ω0 and t∈[0,s], claim 3 gives Φt(ω)=Φt(s),W(s)(ω), so Xt′(ω)=N(Σt(ω)−Φt(s),W(s)(ω))=Ψt(Σt(ω),W(s)(ω)), where Σt(ω)∈GN by the first paragraph.
Joint measurability with the record prefix. Let t∈[0,s] and c∈Rl. The product σ-algebra B(R)⊗Rs is generated by the rectangles E×A with E∈B(R) and A∈Rs (Product Sigma-Algebra), and the preimage of such a rectangle under ω↦(c⋅Xt′(ω),W(s)(ω)) is (c⋅Xt′)−1(E)∩(W(s))−1(A)∈F, both sets belonging to F by the preceding paragraphs and claim 1. By claim 2 of Generator Criterion for Measurability the map is measurable with respect to F and B(R)⊗Rs.
Claim 5.Preliminaries. Under the additional assumptions, the setting of Law Identity between the N-Agent Aggregate Path with Its Observation Record and the Synthetic Copy's Regularised Path with Its Record is instantiated with horizon s; its objects are the synthetic copy with Ω♯=Ω♭×Rd×Rs, its record D, the path space Path=Path(GN,s) with its σ-algebra C generated by the sets {p:p(v)=y} (v∈[0,s], y∈GN), the maps Π on Ω and Π♯ on Ω♯ with Π♯(ω♭,θ,r)(v)=Σˉv♯,r(ω♭), and the set D0={Σ0=x0}. By claim 1 of that lemma, D0∈F (so that P(D0)=1 by assumption), Π♯ takes its values in Path and is measurable with respect to F♯ and C, and D is measurable with respect to F♯ and Rs. Since Σˉs♯,D(ω♭,θ,r)=Σˉs♯,r(ω♭)=Π♯(ω♭,θ,r)(s) and every path in Path takes its values in GN (The Space of Piecewise Constant Paths in a Finite Set: Measurability of Evaluations, Restrictions, Left Limits, and Occupation Integrals), Σˉs♯,D takes its values in GN; and for every y∈GN the set {Σˉs♯,D=y}=(Π♯)−1({p:p(s)=y}) belongs to F♯, so that {Σˉs♯,D∈A}=⋃y∈A{Σˉs♯,D=y}∈F♯ for every A⊆GN, the union being finite because GN⊆{x∈Rl:Nxγ∈{0,1,…,N} for all γ} is finite (each Nxγ is a nonnegative integer at most N because 0≤xγ≤1 on Δl). Thus Σˉs♯,D is measurable with respect to F♯ and P(GN), and the pair (Σˉs♯,D,D) is measurable with respect to F♯ and P(GN)⊗Rs by the rectangle argument of the last paragraph of claim 4 (the preimage of A×A′ being {Σˉs♯,D∈A}∩D−1(A′)). Likewise the pair (Σs,W(s)) is measurable with respect to F and P(GN)⊗Rs: {Σs∈A}=⋃y∈A⋂γ{Σsγ=yγ}∈F for A⊆GN, each Σsγ being a random variable (claim 4), and W(s) is measurable by claim 1.
the record of the restricted solution being W(s). Here F′(Σˉs♯,D,D) is the indicator of {(c⋅Xs′′,D)∈E}, so the right-hand side equals μ♯({(c⋅Xs′′,D)∈E}) by The Integral of an Indicator Function is the Measure of the Set and P(D0)=1. On the left, F′(Σs,W(s)) is the indicator of {(c⋅Ψs(Σs,W(s)),W(s))∈E}; by claim 4 this set differs from {(c⋅Xs′,W(s))∈E} at most by points outside Ω0, and both sets belong to F (the first as the preimage of Ξ−1(E) under the measurable pair (Σs,W(s)), the second by claim 4). Now P(Ω0)=1, the regular event of a solution having probability one by Solution of the Controlled N-Agent Dynamics, and P(D0)=1 by assumption, so P(Ω∖Ω0)=0 and P(Ω∖D0)=0 by the additivity of the measureP. For events A, A′ that agree outside an event N with P(N)=0 one has A∖N=A′∖N and, by additivity and monotonicity of P, P(A)=P(A∖N)+P(A∩N)=P(A∖N), since 0≤P(A∩N)≤P(N)=0; hence P(A)=P(A∖N)=P(A′∖N)=P(A′). Applying this with N=Ω∖Ω0 to the two events above, and noting that E[1D01A]=P(A∩D0) by The Integral of an Indicator Function is the Measure of the Set and P(A∩D0)=P(A) by the same argument with N=Ω∖D0, the left-hand side equals P({(c⋅Xs′,W(s))∈E}). Hence
P({(c⋅Xs′,W(s))∈E})=μ♯({(c⋅Xs′′,D)∈E})for every E∈B(R)⊗Rs,
The integral identity. Let F:R×Rs→[0,∞] be measurable with respect to B(R)⊗Rs, and write ν for the common image measure. By claim 2 of Image Measures, Measures with Densities, and Change of Variables applied to P and the map (c⋅Xs′,W(s)), and then to μ♯ and the map (c⋅Xs′′,D),