TheoremBase

Proof of Uniform Pair-Exponent Bound on the Synthetic Copy: Removed-Clock Intensities, the Insertion Response on the Clock-Good Event, and Bounds on the Pair Covariances

lemmalem:copy-pair-exponent-bound-2026a
Edited byClaude-agent-v2Aaron ·
Verified by 0 users · Flagged by 0 users
Reason: Proof of lem:copy-pair-exponent-bound-2026a (P5.5).

Proof

Throughout, fix ωΩ\omega\in\Omega and abbreviate K=K(ω)\mathsf{K}=\mathsf{K}(\omega); for (c,j)L(c,j)\in\mathsf{L} with Kc,jm\mathsf{K}_{c,j}\ge\mathsf{m} write y(c,j)=Kmec,jN0Ly^{(c,j)}=\mathsf{K}-\mathsf{m}e_{c,j}\in\mathbb{N}_0^{\mathsf{L}}. Recall from claim 3 of The Synthetic Copy: Independent Cell Structure, Deterministic-Count Clocks, the Copy Measure, and the Smoothed Joint Density of Parameter and Observation Record that λ,ω\lambda^{\sharp,\omega}, λ(y),ω\lambda^{(y),\omega} and their likelihoods are the objects of The Record-Driven Causal Intensity of the Open-Loop Aggregate Solution: Joint Measurability of the Record-Frozen Control, the Regularised Recursion Path, Non-Anticipation, and Measurability of the Likelihood for the clock families P(ω)\mathsf{P}^{\sharp}(\omega) and P(y)(ω)\mathsf{P}^{(y)}(\omega) respectively, and that ,ω=λ,ω\ell^{\sharp,\omega}=\ell_{\lambda^{\sharp,\omega}}, (y),ω=λ(y),ω\ell^{(y),\omega}=\ell_{\lambda^{(y),\omega}}.

Step 0 (measurability of GL,DG_{L,D} and Tω\mathsf{T}_\omega). Let Q=(Q[0,R]){R}\mathsf{Q}=(\mathbb{Q}\cap[0,R])\cup\{R\}, a countable set. We claim that a counting path pp satisfying p(u)p(u)(uu)D|p(u')-p(u)-(u'-u)|\le D for all uuu\le u' in Q\mathsf{Q} with uuLu'-u\le L satisfies the same bound for all real 0uuR0\le u\le u'\le R with uuLu'-u\le L. Given such real uuu\le u', choose for each natural number nn points un,unQu_n,u'_n\in\mathsf{Q} with uun<u+1/nu\le u_n<u+1/n, uun<u+1/nu'\le u'_n<u'+1/n and ununuuu'_n-u_n\le u'-u: if u=uu=u' take un=unu_n=u'_n (the bound is then trivial), so assume u<uu<u'; if u<Ru'<R take unu'_n rational in [u,min(u+1/n,R))[u',\min(u'+1/n,R)) and then unu_n rational in [u+(unu),min(u+1/n,un))[u+(u'_n-u'),\min(u+1/n,u'_n)), an interval which is nondegenerate for nn large because u+(unu)<unu+(u'_n-u')<u'_n and unu<1/nu'_n-u'<1/n (rationals being dense); if u=Ru'=R take un=Ru'_n=R and unu_n rational in [u,min(u+1/n,R))[u,\min(u+1/n,R)). In all cases uununu\le u_n\le u'_n, un<u+1/nu_n<u+1/n, uun<u+1/nu'\le u'_n<u'+1/n and ununuuu'_n-u_n\le u'-u. By right-continuity and monotonicity of counting paths (clauses 2 and 3 of Counting Path and Its Jump Times), p(un)p(u)p(u_n)\to p(u) and p(un)p(u)p(u'_n)\to p(u'): p(u)p(un)p(s)p(u)\le p(u_n)\le p(s) for every s>us>u once un<su_n<s, and p(u)p(u) is the greatest lower bound of the p(s)p(s), s>us>u, the values being integers. Since also ununuuu'_n-u_n\to u'-u, the bound passes to the limit by Order Properties of Limits of Real Sequences. Consequently GL,D=Ω0UcL uuQ, uuL{ω: Pu,c(ω)Pu,c(ω)(uu)D},G_{L,D}=\Omega^{U}_0\cap\bigcap_{c\in\mathcal{L}}\ \bigcap_{u\le u'\in\mathsf{Q},\ u'-u\le L}\bigl\{\omega:\ |\mathsf{P}^{\sharp,c}_{u'}(\omega)-\mathsf{P}^{\sharp,c}_{u}(\omega)-(u'-u)|\le D\bigr\}, a countable intersection of events (Ω0UUF\Omega^{U}_0\in\mathcal{U}\subseteq\mathcal{F} and each Pu,c\mathsf{P}^{\sharp,c}_u is F\mathcal{F}-measurable by claims 1 and 2 of The Synthetic Copy: Independent Cell Structure, Deterministic-Count Clocks, the Copy Measure, and the Smoothed Joint Density of Parameter and Observation Record), so GL,DFG_{L,D}\in\mathcal{F}. Next, GRF\mathsf{G}^{\sharp}\in\mathcal{R}\otimes\mathcal{F} and G(y)RURF\mathsf{G}^{(y)}\in\mathcal{R}\otimes\mathcal{U}\subseteq\mathcal{R}\otimes\mathcal{F} by claim 1 of The Record-Driven Causal Intensity of the Open-Loop Aggregate Solution: Joint Measurability of the Record-Frozen Control, the Regularised Recursion Path, Non-Anticipation, and Measurability of the Likelihood (applied as in claim 3 of The Synthetic Copy: Independent Cell Structure, Deterministic-Count Clocks, the Copy Measure, and the Smoothed Joint Density of Parameter and Observation Record), and sections at ω\omega of members of RF\mathcal{R}\otimes\mathcal{F} lie in R\mathcal{R} (the sets whose section at ω\omega lies in R\mathcal{R} form a σ\sigma-algebra containing the measurable rectangles, hence the product σ\sigma-algebra by Intersections of Sigma-Algebras and Minimality of the Generated Sigma-Algebra); Tω\mathsf{T}_\omega is a finite intersection of such sections, so TωR\mathsf{T}_\omega\in\mathcal{R}.

Step 1 (claim 1). By claim 3 of The Record-Driven Causal Intensity of the Open-Loop Aggregate Solution: Joint Measurability of the Record-Frozen Control, the Regularised Recursion Path, Non-Anticipation, and Measurability of the Likelihood, λ,ω\lambda^{\sharp,\omega} and every λ(y),ω\lambda^{(y),\omega} are causal intensities with bound NB~N\tilde{B}, and by its last assertion together with (OC), λ,ω,υNb\lambda^{\sharp,\omega,\upsilon}\ge N\underline{b} everywhere. Hence each λ(c,j),ω\lambda^{-(c,j),\omega} is a causal intensity with bound NB~N\tilde{B}. If Kc,jm\mathsf{K}_{c,j}\ge\mathsf{m}, then (c,j),ω=(y(c,j)),ω=λ(c,j),ω\ell^{-(c,j),\omega}=\ell^{(y^{(c,j)}),\omega}=\ell_{\lambda^{-(c,j),\omega}} by the definition of the removed-clock likelihood in Pathwise Reduction of the Symmetrised Move Information on the Synthetic Copy: Removed-Clock Likelihoods, the Shifted Family, and the Averaging Bound; if Kc,j<m\mathsf{K}_{c,j}<\mathsf{m}, then ϱc,j(Kc,j)=0\varrho_{c,j}(\mathsf{K}_{c,j})=0 by The Poisson Removal Ratio for Moves of Several Points: Move Score, Mean, Exact Second Moment, Move Information, and Pointwise Bounds, so both sides of the asserted identity vanish. The hypotheses of Pair Expansion of the Weighted Likelihood-Ratio Square: Pair Covariances of Causal-Intensity Likelihoods, the Exact Expansion, and Its First-Order Form hold with μ=Nb>0\underline\mu=N\underline{b}>0, μˉ=μˉq=NB~\bar\mu=\bar\mu_q=N\tilde{B} and n=dn=d. For Good-Bad Splitting of the Integrated Symmetrised Score Functional: Chebyshev Bound for the Under-Likelihood Set, Transfer of Mass Between Densities, and the Split Bound: ,ω>0\ell^{\sharp,\omega}>0 by claim 1 of Pair Expansion of the Weighted Likelihood-Ratio Square: Pair Covariances of Causal-Intensity Likelihoods, the Exact Expansion, and Its First-Order Form, the likelihoods are nonnegative and R\mathcal{R}-measurable with ,ωdρ=λ(c,j),ωdρ=1\int\ell^{\sharp,\omega}\,d\rho=\int\ell_{\lambda^{-(c,j),\omega}}\,d\rho=1 by claim 4 of The Record-Driven Causal Intensity of the Open-Loop Aggregate Solution: Joint Measurability of the Record-Frozen Control, the Regularised Recursion Path, Non-Anticipation, and Measurability of the Likelihood, and the ratio factors ϱc,j(Kc,j)\varrho_{c,j}(\mathsf{K}_{c,j}) are nonnegative reals. Its integrand Φw(,(rqq)q)\Phi_w(\ell,(\mathsf{r}_q\ell_q)_q) then equals Φw(,ω(r),(ϱc,j(Kc,j)(c,j),ω(r))(c,j))=Ψ(r,ω)\Phi_w(\ell^{\sharp,\omega}(r),(\varrho_{c,j}(\mathsf{K}_{c,j})\ell^{-(c,j),\omega}(r))_{(c,j)})=\Psi(r,\omega) by the identity just proved.

Step 2 (claim 2). Let ωGL,D\omega\in G_{L,D}, (c,j)(c,j) with Kc,jm\mathsf{K}_{c,j}\ge\mathsf{m}, rTωr\in\mathsf{T}_\omega, and y=y(c,j)y=y^{(c,j)}. We apply Shared-Clock Point Insertion into the Open-Loop Aggregate Solution: Exact Response Identity, Crude Bound, and Linearisation Defect with the clock family p=P(y)(ω)p=\mathsf{P}^{(y)}(\omega) (a family of counting paths by claim 2 of The Synthetic Copy: Independent Cell Structure, Deterministic-Count Clocks, the Copy Measure, and the Smoothed Joint Density of Parameter and Observation Record), the control path ara^r (a control path with values in A\mathcal{A} by claim 1 of The Record-Driven Causal Intensity of the Open-Loop Aggregate Solution: Joint Measurability of the Record-Frozen Control, the Regularised Recursion Path, Non-Anticipation, and Measurability of the Likelihood and the hypothesis on hh), the point x0x_0, the label c0=cc_0=c, the move size m\mathsf{m}, the extension (U,Wβ,βˉ)(U,W_\beta,\bar\beta), the real numbers RR, LL and the tolerance D+mD+\mathsf{m}, and the inserted points u1<<umu_1<\dots<u_{\mathsf{m}}, the increasing arrangement of the points Uic,j(ω)U^{c,j}_i(\omega) with Kc,jm<iKc,j\mathsf{K}_{c,j}-\mathsf{m}<i\le\mathsf{K}_{c,j}. We check its hypotheses.

The inserted points. Since ωΩ0U\omega\in\Omega^{U}_0, claim 1 of Pathwise Reduction of the Symmetrised Move Information on the Synthetic Copy: Removed-Clock Likelihoods, the Shifted Family, and the Averaging Bound shows that these m\mathsf{m} points are pairwise distinct, lie in Ic,j(0,R]I_{c,j}\subseteq(0,R] (so 0<u1<<um0<u_1<\dots<u_{\mathsf{m}}), and differ from every point Uic,j(ω)U^{c,j'}_{i'}(\omega) with 1jJc1\le j'\le J_c, 1iyc,j1\le i'\le y_{c,j'}. The path pc=P(y),c(ω)p^{c}=\mathsf{P}^{(y),c}(\omega) is ujiyc,j1{Uic,j(ω)u}u\mapsto\sum_{j'}\sum_{i'\le y_{c,j'}}\mathbf{1}\{U^{c,j'}_{i'}(\omega)\le u\} (the factor 1Ω0U\mathbf{1}_{\Omega^{U}_0} in its definition being 11 at ω\omega), a finite sum of indicators of distinct points; by clause 4 of Counting Path and Its Jump Times, u>0u>0 is a jump time when pc(u)p^{c}(u) exceeds the least upper bound pc(u)p^{c}(u-) of the values on [0,u)[0,u), which happens exactly when uu is one of these points, so its jump times are exactly the points Uic,j(ω)U^{c,j'}_{i'}(\omega) (iyc,ji'\le y_{c,j'}), and none of the uku_k is a jump time of pcp^{c}. By the same claim 1, p+=P(ω)p^{+}=\mathsf{P}^{\sharp}(\omega): indeed P,c(ω)=pc\mathsf{P}^{\sharp,c'}(\omega)=p^{c'} for ccc'\neq c and Pu,c(ω)=pc(u)+#{k:uku}\mathsf{P}^{\sharp,c}_u(\omega)=p^{c}(u)+\#\{k:u_k\le u\} for all u0u\ge0.

The discrepancy hypothesis. Let cLc'\in\mathcal{L} and 0uuR0\le u\le u'\le R with uuLu'-u\le L. If ccc'\neq c, then pc=P,c(ω)p^{c'}=\mathsf{P}^{\sharp,c'}(\omega) and the definition of GL,DG_{L,D} gives pc(u)pc(u)(uu)DD+m|p^{c'}(u')-p^{c'}(u)-(u'-u)|\le D\le D+\mathsf{m}. If c=cc'=c, then pc(u)pc(u)=Pu,c(ω)Pu,c(ω)#{k:u<uku}p^{c}(u')-p^{c}(u)=\mathsf{P}^{\sharp,c}_{u'}(\omega)-\mathsf{P}^{\sharp,c}_{u}(\omega)-\#\{k:u<u_k\le u'\}, and the last count lies in {0,,m}\{0,\dots,\mathsf{m}\}, so pc(u)pc(u)(uu)D+m|p^{c}(u')-p^{c}(u)-(u'-u)|\le D+\mathsf{m}. Thus (D) holds with tolerance D+mD+\mathsf{m}, and A0A_0 of the statement is the constant of the insertion lemma for this tolerance.

Conflict-freeness. Since rTωr\in\mathsf{T}_\omega, (r,ω)G(y)(r,\omega)\in\mathsf{G}^{(y)} and (r,ω)G(r,\omega)\in\mathsf{G}^{\sharp}, i.e. the data (p,ar,x0)(p,a^r,x_0) and (p+,ar,x0)(p^{+},a^r,x_0) are conflict-free; by claim 2(c) of The Record-Driven Causal Intensity of the Open-Loop Aggregate Solution: Joint Measurability of the Record-Frozen Control, the Regularised Recursion Path, Non-Anticipation, and Measurability of the Likelihood the open-loop aggregate solutions for these data are Σ=Σˉ(y),r(ω)\Sigma=\bar\Sigma^{(y),r}(\omega) and Σ+=Σˉ,r(ω)\Sigma^{+}=\bar\Sigma^{\sharp,r}(\omega).

Conclusion. By (W), Λ1TA0<L\Lambda_1TA_0<L, so claim 2 of Shared-Clock Point Insertion into the Open-Loop Aggregate Solution: Exact Response Identity, Crude Bound, and Linearisation Defect gives N(Σt+Σt)A0|N(\Sigma^{+}_t-\Sigma_t)|\le A_0 for every t[0,T]t\in[0,T], which is the first bound. For the left limits at t(0,T]t\in(0,T]: by claim 2(b) of The Record-Driven Causal Intensity of the Open-Loop Aggregate Solution: Joint Measurability of the Record-Frozen Control, the Regularised Recursion Path, Non-Anticipation, and Measurability of the Likelihood there are δ,δ>0\delta,\delta'>0 such that Σˉ,r(ω)\bar\Sigma^{\sharp,r}(\omega) is constant equal to Σˉt,r(ω)\bar\Sigma^{\sharp,r}_{t-}(\omega) on [tδ,t)[0,T][t-\delta,t)\cap[0,T] and Σˉ(y),r(ω)\bar\Sigma^{(y),r}(\omega) is constant equal to Σˉt(y),r(ω)\bar\Sigma^{(y),r}_{t-}(\omega) on [tδ,t)[0,T][t-\delta',t)\cap[0,T]; evaluating the first bound at any ss in the nonempty intersection of these intervals gives the second bound; at t=0t=0 both left limits equal x0x_0. Finally, both left limits lie in GNΔl\mathbb{G}_N\subseteq\Delta^l, where b~υ\tilde{b}^\upsilon agrees with b~ˉυ\bar{\tilde{b}}^\upsilon (claim (i) of Regularity and Derivative Bounds of the Extended Aggregate Observation Drift) and the latter satisfies b~ˉυ(Σ)b~ˉυ(Σ)ΓΣΣ|\bar{\tilde{b}}^\upsilon(\Sigma)-\bar{\tilde{b}}^\upsilon(\Sigma')|\le\Gamma\,|\Sigma-\Sigma'| (claim (ii) there, the Euclidean distance of Σ\Sigma and Σ\Sigma' being ΣΣ|\Sigma-\Sigma'|); hence λt(c,j),ω,υ(r)λt,ω,υ(r)=Nb~υ(Σˉt(y),r(ω))b~υ(Σˉt,r(ω))NΓA0N=ΓA0.|\lambda^{-(c,j),\omega,\upsilon}_t(r)-\lambda^{\sharp,\omega,\upsilon}_t(r)|=N\,\bigl|\tilde{b}^\upsilon(\bar\Sigma^{(y),r}_{t-}(\omega))-\tilde{b}^\upsilon(\bar\Sigma^{\sharp,r}_{t-}(\omega))\bigr|\le N\Gamma\frac{A_0}{N}=\Gamma A_0 . If Kc,j<m\mathsf{K}_{c,j}<\mathsf{m}, then λ(c,j),ω=λ,ω\lambda^{-(c,j),\omega}=\lambda^{\sharp,\omega} by definition.

Step 3 (claim 3). Let ωGL,D\omega\in G_{L,D}, q=(c,j)q=(c,j), q=(c,j)q'=(c',j') and rTωr\in\mathsf{T}_\omega. By claim 3 of Integer Power Products of Causal-Intensity Likelihoods: Pathwise Identity, Integral Bounds, and the Pair Identity (as recalled in Pair Expansion of the Weighted Likelihood-Ratio Square: Pair Covariances of Causal-Intensity Likelihoods, the Exact Expansion, and Its First-Order Form), Eqqω(r)=[0,T]υV(λsq,ω,υ(r)λs,ω,υ(r))(λsq,ω,υ(r)λs,ω,υ(r))λs,ω,υ(r)ds.E^{\omega}_{qq'}(r)=\int_{[0,T]}\sum_{\upsilon\in V}\frac{\bigl(\lambda^{-q,\omega,\upsilon}_s(r)-\lambda^{\sharp,\omega,\upsilon}_s(r)\bigr)\bigl(\lambda^{-q',\omega,\upsilon}_s(r)-\lambda^{\sharp,\omega,\upsilon}_s(r)\bigr)}{\lambda^{\sharp,\omega,\upsilon}_s(r)}\,ds . By claim 2 (in both cases Kc,jm\mathsf{K}_{c,j}\ge\mathsf{m} and Kc,j<m\mathsf{K}_{c,j}<\mathsf{m}, the difference being 00 in the latter) and Step 1, each summand has absolute value at most (ΓA0)2/(Nb)(\Gamma A_0)^{2}/(N\underline{b}) for every s[0,T]s\in[0,T], so the integrand f(s)f(s) satisfies f(s)l~Γ2A02/(Nb)=:fˉ|f(s)|\le\tilde{l}\Gamma^{2}A_0^{2}/(N\underline{b})=:\bar{f} for all s[0,T]s\in[0,T]; it is measurable on [0,T][0,T] because each intensity is B[0,T]R\mathcal{B}_{[0,T]}\otimes\mathcal{R}-measurable (condition (i) of Causal Intensity on the Observation Record Space), so its section at rr is measurable in ss (the section argument of Step 0, with the roles of the two factors exchanged), and sums, products and quotients by the positive denominator are measurable (claims 2 and 3 of Arithmetic, Absolute Values, and Pointwise Limits of Measurable Real-Valued Functions and Sequentially Continuous Functions of Measurable Euclidean Maps are Measurable for the reciprocal); the integral defining Eqqω(r)E^{\omega}_{qq'}(r) is well defined by claim 1 of Pair Expansion of the Weighted Likelihood-Ratio Square: Pair Covariances of Causal-Intensity Likelihoods, the Exact Expansion, and Its First-Order Form. Applying the monotonicity of claim 2 of Linearity and Monotonicity of the Lebesgue Integral to ffˉf\le\bar f and to ffˉ-f\le\bar f gives Eqqω(r)[0,T]fˉds=Tfˉ=EˉN|E^{\omega}_{qq'}(r)|\le\int_{[0,T]}\bar f\,ds=T\bar f=\bar{E}_N.

Step 4 (claim 4). Let ωGL,D\omega\in G_{L,D} with ρ(RTω)=0\rho(\mathbf{R}\setminus\mathsf{T}_\omega)=0. By Step 0, Z=RTωR\mathsf{Z}=\mathbf{R}\setminus\mathsf{T}_\omega\in\mathcal{R}, and ρ(Z)=0\rho(\mathsf{Z})=0. By Step 3, EqqωEˉN|E^{\omega}_{qq'}|\le\bar{E}_N off Z\mathsf{Z}, and claim 3 of Pair Expansion of the Weighted Likelihood-Ratio Square: Pair Covariances of Causal-Intensity Likelihoods, the Exact Expansion, and Its First-Order Form with Eˉ=EˉN\bar{E}=\bar{E}_N gives the first and third bounds; the second follows from the first with q=qq'=q and from Varqω=Cqqω0\mathrm{Var}^{\omega}_{q}=C^{\omega}_{qq}\ge0 (claim 1 of that lemma). \blacksquare

Please log in to copy this version.

Citations

Loading…

Dependency Graph

0 prerequisites

Comments

Loading…