73. Keep approximation bias separate from coefficient error
On this page · Permalink · Source line 2997
The positive approximation theorem assumes access to exact integral coefficients. A fitted model introduces another discrepancy. Its coefficient estimates need their own validity constraints.
Proposition 65: Certified coefficient error and approximation bias
Suppose every fitted coefficient \(\widetilde C_{a,n,k}\) preserves the same cone \(C\), and
Then \(\widetilde B_a^{[n]}(x)=\sum_k b_{n,k}(x)\widetilde C_{a,n,k}\) is internally valid. If
its integrated discrepancy from the original Lipschitz density is at most
A known additional model-correction discrepancy is added to this budget, not absorbed into the approximation term.
Read proof · Recorded Lean scope · Permalink · Source line 3001
Proof
Nonnegative Bernstein weights preserve cone positivity, and their integrals prove normalization. For any \(z\in K\), the triangle inequality gives
Add the approximation error from Proposition 64. A separate correction is handled by another application of the triangle inequality. \(\square\)
This is a conditional approximation-and-estimation theorem, not a claim that more coefficients always improve a finite-data estimator. Increasing \(n\) reduces the stated bias bound while changing the number and conditioning of the quantities to be estimated. A cone witness proves that the resulting object is a probability model. It does not prove that the coefficient error budgets cover the generating process.
The moments needed for \(C_{a,n,k}\) are bounded Bernstein-weighted experiments. Their interpretation as full operator coefficients still requires suitable predictive-state coverage or a justified observable core. The next section provides sequential evidence for conditional experiments, not an automatic replacement for those identification assumptions.