lemmaroutine

Mean comparison scale factors and release cost

Mean-term comparison costs

O(b/a)

O((b/a)^{s-1})

, plus

f/u

on release

cites scale and release costs in prefix and raw-difference bounds

Lemma·lem:est-mean-comparison·§7.3 Mean comparisons and the cost of releasing a source

Statement (paper)

Compare a budget-

m

sample term with the same term using true stochastic inputs. For a first-channel mean contribution use its clipped relative error against

1+d_y

. In the bound for its

s

th-power norm, the scale factor multiplying a child root-discrepancy power is, up to fixed constants,

\begin{cases} b/a,&b\ge a,\\ (b/a)^{s-1},&b<a. \end{cases}

A child that releases the old source and restarts on a stage-rate

f

domain costs in addition at most

f/u

in norm power. Direct children retaining that source have no such factor. The same-scale vector and second-channel comparisons have constant scale cost, with

f/u

only where a source is released. No independence of estimated factors is required.

In plain English

Comparing a budget-

m

sample term with the same term on true stochastic inputs, the bound on the

s

th-power norm of a first-channel mean contribution (its clipped relative error against

1+d_y

) multiplies each child root-discrepancy power by

O(b/a)

b e<a

is replaced correctly: by

O(b/a)

when

b\ge a

and

O((b/a)^{s-1})

when

b<a

. A child that releases the old source and restarts on a stage-rate

f

domain adds at most

f/u

in norm power, while same-scale vector and second-channel comparisons cost only a constant scale factor, plus

f/u

where a source is released, and no independence of estimated factors is needed.

Why it's here

This lemma bundles the scale-factor cases (coarse bin, fine bin), the

f/u

source-release cost via the incoming cap, and the second-channel, rank, detector and reward comparisons into one statement, so later mean-prefix and raw-difference bounds can cite a single comparison with explicit costs. The key point is that all costs are controlled by scale ratios and

f/u

alone, without assuming independence of the estimated factors.

Classified routine:

A bookkeeping lemma that collects scale-ratio factors (b/a or (b/a)^{s-1}) and the f/u source-release cost. These follow from the comparability and contraction properties of the estimation loss (lem-est-loss) by a standard norm-power calculation, not from a new idea.

Uses

lemProperties of the estimation loss

Used by

lemMean prefixes are small against targetslemRaw difference bounds at slack-d groups

Inside the proof

claimCoarse bin scale factor b/aclaimSource-release cost f/u via incoming capclaimFine bin scale cost by early reconditioningclaimSecond channel, detector and reward comparisons

Sources

PaperOpen

Section: §7.3 Mean comparisons and the cost of releasing a source
Page: —
Label: lem:est-mean-comparison
Line: sections/estimation.tex:230

Leannot aligned

Phase 2 aligns this node to a Lean declaration.