lemmaroutine

True tables yield prescribed sample means

Estimator equations on true tables return the prescribed sample-term means

noise-free baseline for the sampled estimator

Lemma·lem:est-true-means·§7.2 Raw sample terms

Statement (paper)

Using true stochastic tables in Equations -- gives, after the indicated conditional averages, the prescribed raw inputs and vector values on their conditioning slices, with the stated zero extensions. In particular, the first row channel has target

d_y=G(x,y)/a

and the second has target

\zeta q_y\mathbf1_{Y_t(y)}

In plain English

If the estimator equations for the raw sample terms are evaluated with true stochastic tables, then after the indicated conditional averaging they return the prescribed raw inputs and vector values on their conditioning slices, extended by zero elsewhere. In particular, the first row channel has target

d_y=G(x,y)/a

and the second has target

\zeta q_y\mathbf1_{Y_t(y)}

Why it's here

This lemma checks that the raw sample-term construction is correct when the tables are exact, so the targets of the two row channels are known. It is the idealized, noise-free baseline against which the sampled version is compared, relying on the retention estimates of the rank-channel lemma.

Classified routine:

A direct verification that the paper's estimator equations are unbiased when evaluated on exact stochastic tables. It follows by conditional-expectation bookkeeping from the rank-channel retention estimates (lem-env-ranks).

Uses

lemRank channel retention estimates

Used by

Nothing in the paper

Sources

PaperOpen

Section: §7.2 Raw sample terms
Page: —
Label: lem:est-true-means
Line: sections/estimation.tex:126

Leannot aligned

Phase 2 aligns this node to a Lean declaration.