58. An observation density is not a branch probability
On this page · Permalink · Source line 2278
Let \((Y,\mathcal Y)\) be a standard Borel observation space and let \(\mu\) be a fixed probability reference measure. Keep a finite action set. For each action \(a\), let \(B_a(y):E\to E\) be measurable and integrable in operator norm. Let \((C,\lambda)\) be a proper probability cone and mass functional as in Section 46. Assume that, outside one \(\mu\)-null set for each action,
The second identity is an equality of linear functionals. The first is a statement on the whole cone, not only on a finite selection of states.
Proposition 52: Continuous-observation instrument semantics
For \(z\in K=\{z\in C:\lambda z=1\}\),
define a probability kernel and, for \(\mu\)-almost every observation with positive denominator, a conditional state. They generate consistent finite record laws under any common measurable history-dependent policy. For prescribed actions, the joint observation density is
with respect to \(\mu^{\otimes T}\). Replacing the reference measure by \(\mu'=r\mu\), with \(r>0\) almost everywhere and \(\int r\,d\mu=1\), requires \(B'_a(y)=B_a(y)/r(y)\). Event probabilities and normalized states then remain unchanged.
Read proof · Recorded Lean scope · Permalink · Source line 2290
Proof
Cone positivity makes the density nonnegative and the integrated mass identity makes its integral one. A positive-density update lies in \(K\). Assign any fixed state of \(K\) on the common exceptional null set and at zero-density points to obtain a measurable version of the update. This arbitrary choice has no effect on the probability kernel. Repeated integration, or conditioning one step at a time, proves normalization and consistency of the finite laws. Measurable policy factors are nonnegative and sum to one at each history. The reference-measure transformation cancels \(r\) in each integral and cancels \(1/r\) in the normalized update. \(\square\)
When \(\mu\) has no atoms, an individual point has probability zero even when its density is positive. A density may exceed one. Neither fact is a numerical pathology. Flooring a vanishing denominator changes the model and is not part of this theorem.
A continuous density at an exact point is a version-dependent object on null sets. The update formula specifies a convenient version wherever its denominator is positive. Event probabilities are the invariant statistical objects. Comparing model densities requires a common measure or a declared change-of-measure calculation.
A representation that lacks an operator-norm integrable density needs a more general operator-valued measure. Such representations are not silently covered by the density hypothesis above.