64. A valid density approximation with a resolution bound
On this page · Permalink · Source line 2504
Exact coarsening gives a finite event model. To compare complete continuous observation laws, lift that model back to a density on the same observation space. Assume all cells have positive reference mass and put
This uses the normalized reference measure inside each cell. It is an explicit density approximation, not an assertion that the original conditional density was constant there.
Proposition 58: Positive cell-average approximation
The family \(B_a^\Pi\) is cone preserving and mass conserving. It has exactly the same cell operators as \(B_a\). Let \(Y\) have a metric and suppose
in the induced base norm, with every cell of diameter at most \(h\). Then
For equal intervals of width \(h\) under the uniform measure on \([-1,1]\), the sharper bound is \(\epsilon_\Pi\leq Lh/3\).
Read proof · Recorded Lean scope · Visual guide: Integration retains a covariance term · Permalink · Source line 2514
Proof
Each cell average is a positive scalar multiple of a positive cell operator. Its integral over that cell is \(B_{a,j}\), proving both normalization and exact cell agreement. For \(y\in A_j\), subtract the cell average and use
because \(\|z\|_C=1\). Integrating over \(y\) proves the diameter bound. Two independent uniform points in an interval of width \(h\) have mean absolute separation \(h/3\), obtained by integrating over its two triangles. Applying this inside every equal interval gives the sharper bound. \(\square\)
The Lipschitz constant is a declared operator bound. It is not a fit residual inferred from adjacent samples. The comparison needs a common domain and a common reference measure. If two kernels are only close in Euclidean coefficient norm, the relevant norm-conversion constant must be included.
In the full \(2\times2\) symmetric-matrix example, the pullback base norm is
There \(\|K(u)\|_2\leq2\) and \(\|K(u)-K(v)\|_2\leq(3/2)|u-v|\). The identity
and \(\|AXB\|_1\leq\|A\|_2\|X\|_1\|B\|_2\) give \(L=6\). The rotated action uses an orthogonal matrix before this map and has the same bound. Equal bins therefore give \(\epsilon_\Pi\leq4/n\), capped by two for two valid instruments. The inequality is sufficient, not asserted sharp.