62. Exact observation bins preserve their own event law
On this page · Permalink · Source line 2453
Let \(A_1,\ldots,A_n\) be a measurable partition of \(Y\). Define the cell operators
Their role is to represent observed events. They are not point samples of the original density.
Proposition 56: Exact bin coarsening and its posterior
Every \(B_{a,j}\) preserves the probability cone, and \(\lambda\sum_jB_{a,j}=\lambda\). For a policy measurable with respect to bin histories, the finite model \(\{B_{a,j}\}\) reproduces exactly the binned observation law of the continuous model at every finite horizon. On an observed cell with \(p_j=\lambda B_{a,j}z>0\),
Read proof · Recorded Lean scope · Visual guide: Integration retains a covariance term · Permalink · Source line 2463
Proof
Integrals of vectors in a closed convex cone remain in the cone. Summing over a partition gives the original mass identity. For a fixed bin history, its policy factors are constant across the corresponding cells. Successive integration of the operator product therefore gives the product of the cell operators, in the original temporal order. This establishes every finite binned record probability. In the posterior identity, substitute \(z^+(y)\lambda B_a(y)z=B_a(y)z\) on the positive-density set. The remaining outputs are zero because they lie in the cone and have zero mass. \(\square\)
The coarsened posterior is a conditional average, not the posterior at a representative observation value. It preserves exactly the information retained by the event history. An arbitrary policy that reacts differently to two observations inside the same cell is not bin-measurable, so the preceding exact-policy conclusion does not apply to it.
Cell refinement is compatible with this semantics: a parent operator is the sum of its children. In this setting those cell operators are positive probability branches. This positivity is an extra property of event integration, not a property of every signed spectral packet in the signal archive.