claimroutineinferred_dep

Fine bin scale cost by early reconditioning

For b<ab<a the scale factor is O((b/a)s−1)O((b/a)^{s-1}) by early reconditioning
fine-bin case of the scale factor
Claim·§7.3 Mean comparisons and the cost of releasing a source·inside lemMean comparison scale factors and release cost

Statement (paper)

In the case b<ab<a, the scale factor multiplying a child root-discrepancy power in the bound for the ssth-power norm of the first-channel mean contribution is O((b/a)s−1)O((b/a)^{s-1}). This holds after changing the terminal conditioning to YbY_b before taking a power, so the normalized coefficient is b/ab/a, and the integrated change from YaY_a to YbY_b contributes (b/a)sπa/πb=O((b/a)s−1)(b/a)^s\pi_a/\pi_b=O((b/a)^{s-1}).

In plain English

When b<ab<a, the scale factor on a child root-discrepancy power in the ssth-power norm bound for the first-channel mean contribution is O((b/a)s−1)O((b/a)^{s-1}). This follows by reconditioning the terminal state to YbY_b before taking the power, so the normalized coefficient is b/ab/a, and the change from YaY_a to YbY_b contributes (b/a)sπa/πb=O((b/a)s−1)(b/a)^s\pi_a/\pi_b=O((b/a)^{s-1}).

Why it's here

This is the b<ab<a case of the parent lemma's scale-factor bound. Conditioning on the finer YbY_b before the power keeps the coefficient at b/ab/a, so the cost is (b/a)s−1(b/a)^{s-1}, and the cost of moving between YaY_a and YbY_b is of the same order.
Classified routine:
This is a case-specific scale bookkeeping step inside the parent mean-comparison lemma. It reconditions to the finer terminal YbY_b and uses the ratio πa/πb=O(a/b)\pi_a/\pi_b=O(a/b) together with the earlier release-cost claim, which is a direct calculation.

Uses

claimSource-release cost f/u via incoming cap

Used by

Nothing in the paper

Sources

PaperOpen
Section
§7.3 Mean comparisons and the cost of releasing a source
Page
—
Label
—
Line
sections/estimation.tex:297
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Fine bin cost (b/a)^{s-1} by early reconditioning" rests on claim-lem-est-mean-comparison-2