68. The combined continuous polynomial sector
On this page · Permalink · Source line 2748
Proposition 61: Conditional continuous realization with a finite domain certificate
Assume a controlled continuous-observation process has the declared finite predictive dimension and polynomial operator-density degree, a fixed uniform reference measure on \([-1,1]\), and an invertible complete event-test core. Exact moment tables identify its operator density in test coordinates by Proposition 54.
If the fitted family and initial state admit a checked matrix/Gram certificate of Proposition 53, the supplied realization is internally valid at every observation value and finite horizon. A successful invertible fixed-template recognition is one sufficient way to construct such a certificate. Exact coordinate transport and complete packet synthesis preserve the represented event probabilities. Individual signed state packets still need the separate positivity condition before probabilistic interpretation.
Exact observation-cell integration gives the precise finite event model for bin-measurable policies. Positive cell-average density approximations have the resolution bound of Proposition 58. Two certified models on a common cone and common reference measure satisfy Proposition 59's full-law bound whenever the declared instrument discrepancy is controlled.
Read proof · Recorded Lean scope · Permalink · Source line 2750
Proof
Moment identification uses the true dimension and degree hypotheses to apply Proposition 54. The independent Gram identity establishes positivity on the whole declared interval, while the exact integral mass identity supplies normalization through Proposition 52. Proposition 60 supplies a transported witness in the template case. Coordinate cancellation and full packet synthesis are exact identities. Proposition 56 proves the cell-model statement. Propositions 58 and 59 provide the two approximation conclusions with their common-domain and common-policy assumptions unchanged. \(\square\)
For a noisy fitted model, the certificate alone proves only internal validity. A guarantee about the generating process requires a valid uncertainty set covering it. A common-domain certificate over a convex uncertainty family can be checked at complete-family vertices with the same embedding, because the operator identities, Gram positivity and mass constraints survive convex combination. This does not justify an uncertainty set that excludes the true degree, rank or dynamics.
The construction leaves visible what is often collapsed into the phrase signal model: a represented state, an operator-valued observation density, a reference measure, a valid probability domain, an observation protocol and an approximation budget. Each is needed for a different reason.