claimroutineinferred_dep

Second channel, detector and reward comparisons

Second-channel, rank, detector and reward comparisons cost constant scale
remaining comparison cases without independence
Claim·§7.3 Mean comparisons and the cost of releasing a source·inside lemMean comparison scale factors and release cost

Statement (paper)

For the second raw channel, Jensen's inequality applies directly on Cxyu,t\mathcal C_{xy}^{u,t}: its integrated endpoint mask YtY_t is already contained in the preparatory norm's YaY_a domain, so there is no importance factor and no πa/πt\pi_a/\pi_t penalty, and the fixed scaling ζ\zeta does not increase the cost. A rank discrepancy is at most the supremum of its input discrepancies. For the detector trial, the power summed over Yf/fY_f/f is bounded by the score error summed over Xf/fX_f/f and YfY_f, with exactly matching rates. For rewards, the finite left-path count gives an ordinary product comparison, the same incoming cap eliminates old starts for a right-vector error, and source functions have bounded Lipschitz roots in their clipped detector inputs so their costs are the broad vertex costs already computed; none of these estimates uses independence of errors.

In plain English

For the second raw channel, Jensen's inequality gives the comparison directly with no importance factor and no πa/πt\pi_a/\pi_t penalty, and ranks, detector trials and rewards are compared at constant scale cost, with f/uf/u only where a source is released. None of these estimates needs independence of errors.

Why it's here

This claim finishes the parent lemma's cases beyond the first-channel mean: the second-channel, rank, detector and reward comparisons all cost only a constant scale factor. The f/uf/u term appears only where an old source is released, and it comes from the incoming-cap bound of the earlier claim, which handles old starts for a right-vector error. The other steps are Jensen on the already-contained mask YtY_t, a supremum bound for ranks, matching-rate sums for the detector, and Lipschitz roots for source functions.
Classified routine:
Case-by-case bookkeeping inside the parent lemma: it uses Jensen's inequality, a supremum bound for ranks, matching-rate sums and Lipschitz composition, and takes the source-release f/u cost from the incoming-cap claim (claim-lem-est-mean-comparison-2).

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:312
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Second channel, detector and reward comparisons" rests on claim-lem-est-mean-comparison-2