lemmaroutine

Mean prefixes small, noise prefixes tiny

Prefixes split into mean part ≤

c_*2^{-p+B_1d_j}

and noise ≤

c_*2^{-p-K_nd_j}

mean/noise split used by clean-block estimates

Lemma·lem:est-prefix·§7.6 Absolute difference bounds and averaging noise

Statement (paper)

Assume exact local grouping, the earlier task error bounds, and that the sample functions depend only on variables varied by the conditional walk. Their uniform slice means are then deterministic at each indicated pair or vertex. Write

S_j^{\rm mean}

for a mean prefix and

S_j^{\rm noise}=S_j-S_j^{\rm mean}

for its noise. There are fixed

B_1

and arbitrarily large prescribed

K_n

such that

\begin{aligned} \left\|\min\left(1, \frac{|S_j^{1,\rm mean}-d|}{1+d}\right)\right\|_{u,a;s} &\le c_*2^{-p+B_1d_j}, \\ \|S_j^{\rm noise}\|_{u,a;s} &\le c_*2^{-p-K_nd_j}. \end{aligned}

The second-channel mean uses its ordinary absolute norm, extended by zero off its usage domain, and satisfies the first bound. Vector means and noises satisfy the corresponding vertex bounds. The coefficient

c_*

can be chosen as small as needed by task separation and walk constants.

In plain English

Under exact local grouping and the earlier task error bounds, each prefix

S_j

splits into a deterministic mean part and a noise part. The clipped relative discrepancy of the first-channel mean from its target

d

is at most

c_*2^{-p+B_1d_j}

, and the noise has norm at most

c_*2^{-p-K_nd_j}

for any prescribed large

K_n

. The second-channel and vector versions satisfy the corresponding bounds.

Why it's here

The mean bound is the mean-prefix estimate restated at the level of slice means. The noise bound uses the conditional walk's exponential mixing and the raw difference bounds to show that averaging over the varied variables makes the fluctuation part far smaller than the precision scale. Together they give the mean/noise split that later prefix and clean-block arguments cite, with

c_*

still freely shrinkable.

Classified routine:

Direct combination of earlier nodes: the mean bound restates lem-est-mean-prefix at the level of slice means, and the noise bound follows from the exponential mixing of the conditional walk (lem-env-gap) applied to the raw difference bounds (lem-est-raw-difference) by a standard averaging argument.

Uses

lemMean prefixes are small against targetslemExponentially mixing averaging operator on conditional spacelemRaw difference bounds at slack-d groups

Used by

propError reserve after compression and clampingclaimClean active tasks meet target bounds

Sources

PaperOpen

Section: §7.6 Absolute difference bounds and averaging noise
Page: —
Label: lem:est-prefix
Line: sections/estimation.tex:656

Leannot aligned

Phase 2 aligns this node to a Lean declaration.