Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite record bounds and the entire opposite half-line

Abstract

Finite record bounds and the entire opposite half-line

Definition 1.1 (The exact finite erased observation field).

Formalization. D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/Rectangles/OriginalRectangleHalfLines.recordField (✓ std3).

Source. Repository-derived.

Commentary.

For natural k and n, recordField(k,n) is the sigma-field on the original visible integer-time path generated by the chronological words X[-k,-1] and X[1,n]. The erased coordinate X0 is absent, and either observed word may be empty.

Theorem 1.2 (Two ordered limits preserve the same finite bound).

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/Rectangles/OriginalRectangleHalfLines.finite_record_bounds_to_half_lines (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fix any one probability measure P on the original visible integer-time path space, real-valued function Y, natural retained length j and real-valued bounds B_L and B_R. Suppose for every k,n with k>=j the absolute difference between the P conditional expectations of Y given recordField(k,n) and recordField(j,n) is at most B_L almost everywhere. Suppose also that for every k,n with n>=j the corresponding difference for recordField(k,n) and recordField(k,j) is at most B_R. Then the full exterior conditional expectation differs from the conditional expectation given (leftWord(j),after) by at most B_L almost everywhere, and from that given (before,rightWord(j)) by at most B_R almost everywhere. Here before and after are the entire infinite visible half-lines, and exterior is their pair. Both conclusions use the original P and exactly the original bound functions. The left argument first completes k and then n. The right argument first completes n and then k. Each passage uses almost-sure upward conditional-expectation convergence and closedness of the scalar inequality, on a common countable intersection of full-measure events. No L2 convergence claim is needed.

In the formulas, generatedField(f) means MeasurableSpace.comap(f) with the canonical product measurable space on the observation type. condExp(P,Y,m,z) is the value at z of the P conditional expectation of Y given m, and AE(P,(z maps to p)) means p holds P-almost everywhere. Int, Nat, Bool and Real denote the corresponding Lean types.

The finite fields split into the join of the left-word and right-word fields. The supremum of the chronological left-word fields is exactly the before field, and the supremum of the right-word fields is exactly the after field: each finite word is a measurable function of its half-line, while every half-line coordinate occurs in some finite word. Taking these joins proves all four supremum identities used by the two ordered limits. Thus no retained infinite half-line is replaced by a finite window at the last step, including j=0.

In rectangle smoothing, take Y=erasedBit and P to be the visible pushforward of the one native class-restricted original joint law. The intended bounds are rho raised to the left and right original visible success counts. The finite_record_smoothing_by_original_success_count supplier provides bounds for its finite recordPosterior ratios on positive records. Identifying those ratios with these conditional expectations, discarding zero record fibers only on their null sets, and matching the two count conventions are the finite adapters needed before the present limit theorem applies. The chronological_success_moment estimate then controls the squared count under the same original law. Squaring and integrating the resulting posterior bounds and summing the quotient groups gives the separate squared-defect and root-tail conclusions.

References