lemmaroutine

Dense-bin atom table is bounded and unbiased

Dense-bin atom table is bounded with conditional mean

G\omega_k(G)

unbiased atom estimator behind the correction atom

Lemma·lem:atom-dense·§5.2 Dense bins and preparatory normalization

Statement (paper)

For sufficiently large fixed

K

, the table

\mathcal B_a(x,y)= \mathbf1_{\{Y_t(y)=1\}}\frac{k_a(d_y)R}{c(q_y)}

on retained starts has bounded values and row support. On the slice

X_u(x)=Y_t(y)=1

its conditional expectation times

a

equals

G(x,y)\omega_k(G(x,y))

. The same assertion holds for

\mathcal B_a^{(j)}

with the routing fraction included. Apart from its start membership, its true value uses only the terminal channel.

In plain English

For large enough fixed

K

, the table

\mathcal B_a(x,y)=\mathbf1_{\{Y_t(y)=1\}}k_a(d_y)R/c(q_y)

on retained starts has bounded values and bounded row support. On the slice

X_u(x)=Y_t(y)=1

, its conditional expectation times

a

equals

G(x,y)\omega_k(G(x,y))

. The same holds for

\mathcal B_a^{(j)}

with the routing fraction included, and apart from start membership its true value depends only on the terminal channel.

Why it's here

This is the basic atom identity for dense bins: it shows the sampled table is a bounded, unbiased estimator of

G\omega_k(G)

, so later sample-mean arguments can use it. The retention estimates from the rank-channel lemma control the conditioning on the slice. The terminal-channel-only dependence of the true value lets the correction atom lemma and other later steps reuse it.

Classified routine:

A direct unbiasedness and boundedness check for an importance-weighted indicator estimator. It follows by conditioning on the slice and applying the rank-channel retention estimates (lem-env-ranks) to the normalization

c(q_y)

Uses

lemRank channel retention estimates

Used by

lemAtom correction is exact with bounded gate

Sources

PaperOpen

Section: §5.2 Dense bins and preparatory normalization
Page: —
Label: lem:atom-dense
Line: sections/atoms.tex:224

Leannot aligned

Phase 2 aligns this node to a Lean declaration.