claimroutineinferred_dep

Source-release cost f/u via incoming cap

Releasing a source costs Kc(f/u)∥e∥sK_c(f/u)\|e\|^s by the incoming cap
source-release cost f/uf/u in the comparison
Claim·§7.3 Mean comparisons and the cost of releasing a source·inside lemMean comparison scale factors and release cost

Statement (paper)

Let P\mathcal P be a left support relation with incoming degree at most KcK_c, and let e(z,y)e(z,y) be a common right discrepancy. Then 1NE∑xXu(x)u∑z:(x,z)∈PZf(z)∑y:Yb(y)=1∣e(z,y)∣s≤KcNuE∑zZf(z)∑y:Yb(y)=1∣e(z,y)∣s=Kcfu ∥e∥f,b;ss,\frac1N\mathbb E\sum_x\frac{X_u(x)}u\sum_{z:(x,z)\in\mathcal P}Z_f(z)\sum_{y:Y_b(y)=1}|e(z,y)|^s\le \frac{K_c}{Nu}\mathbb E\sum_z Z_f(z)\sum_{y:Y_b(y)=1}|e(z,y)|^s=K_c\frac fu\,\|e\|_{f,b;s}^s, where the source channel in the last norm is ZZ. Hence, when a source is released, the second root-discrepancy sum, after eliminating xx by the left incoming cap and using Ya≤YbY_a\le Y_b, costs O(f/u)O(f/u), while the first sum costs only a constant factor via the right row cap. A projected term costs O(fpar/u)O(f_{\rm par}/u).

In plain English

If a left support relation P\mathcal P has incoming degree at most KcK_c and e(z,y)e(z,y) is a common right discrepancy, then summing over xx with weight Xu(x)/uX_u(x)/u and over zz with (x,z)∈P(x,z)\in\mathcal P is bounded by Kc(f/u) ∥e∥f,b;ssK_c (f/u)\,\|e\|_{f,b;s}^s, with source channel ZZ. So releasing a source costs only O(f/u)O(f/u) in norm power.

Why it's here

Each zz is counted by at most KcK_c values of xx, so the xx-sum collapses to a factor KcK_c and the weights change from 1/u1/u to f/uf/u relative to the ZfZ_f norm. This gives the f/uf/u release cost in the parent lemma, applied to the second root-discrepancy sum, while the first sum needs only a constant factor from the right row cap. The bound adds to the scale-factor bounds of the sibling claims and needs no independence.
Classified routine:
A direct double-counting bound: since each z has at most K_c incoming x, the x-sum is bounded using X_u\le 1, and the remaining step is unfolding the definition of the weighted norm with weight f. This is bookkeeping inside the parent mean-comparison lemma.

Uses

claimCoarse bin scale factor b/a

Used by

claimFine 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
—
Line
sections/estimation.tex:258
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Source-release cost f/u via incoming cap" rests on claim-lem-est-mean-comparison-1