lemmaroutineinferred_dep

Mean prefixes are small against targets

Mean prefixes lie within c∗2−p+B1djc_*2^{-p+B_1d_j} of their targets
mean half of the prefix estimate
Lemma·lem:est-mean-prefix·§7.5 The additive schedule

Statement (paper)

Assume all earlier table and vector bounds with coefficient CbC_b. For an active task there is a fixed B1B_1, independent of the later choice of A∗A_*, such that every mean prefix has norm at most c∗2−p+B1djc_*2^{-p+B_1d_j} against its target. For the first channel the norm uses clipped relative discrepancy; for the second and for vectors it uses ordinary absolute discrepancy. The coefficient c∗c_* can be made arbitrarily small by increasing A∗A_*.

In plain English

For an active task, there is a fixed B1B_1, independent of the later choice of A∗A_*, such that every mean prefix is within norm c∗2−p+B1djc_*2^{-p+B_1d_j} of its target. The norm is clipped relative discrepancy for the first channel and ordinary absolute discrepancy for the second channel and for vectors, and c∗c_* can be made arbitrarily small by increasing A∗A_*.

Why it's here

This packages the per-bin omission cost and the mean-comparison scale and release costs into a single bound on how far any prefix of the mean can stray from its target. The point is that the exponent constant B1B_1 is fixed before A∗A_* is chosen, so the leading factor c∗c_* can be shrunk freely, which later prefix and conditional bounds rely on.
Classified routine:
Bookkeeping that combines the per-bin omission bound (lem-est-omission) with the mean-comparison scale and release costs (lem-est-mean-comparison) into one prefix bound. The constant B1B_1 is tracked so it is fixed before A∗A_* is chosen.

Uses

lemOmitting one fine bin costs littlelemMean comparison scale factors and release cost

Used by

lemMean prefixes small, noise prefixes tiny

Sources

PaperOpen
Section
§7.5 The additive schedule
Page
—
Label
lem:est-mean-prefix
Line
sections/estimation.tex:538
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    "the child bound remains valid" / "Equation  is then bounded by" uses the mean-comparison bound for a budget-m sample term against true stochastic inputs