lemmaroutine

Transfer from sampled histories to actual point

Lemma·com:transfer·§6.1 From sampled histories to the actual point

Statement (paper)

Fix a level and the joint edge--template law P(p,q,θ)=PE(p,q)P(θ∣q). \Prob(p,q,\theta)=\Prob_E(p,q)\Prob(\theta\mid q). Let 0<η<1/20<\eta<1/2. As a function of (q,θ)(q,\theta), select a support U(q,θ)U(q,\theta) that is a row, a column, or a set of at most two states. On an event GG determined by (q,θ)(q,\theta), suppose ν~q(U(q,θ))≥1−3η2. \widetilde\nu_q(U(q,\theta))\ge1-3\eta^2. Then the actual point state X(p)X(p) satisfies P(G, X(p)∉U(q,θ))≤8η. \Prob\bigl(G,\ X(p)\notin U(q,\theta)\bigr)\le8\eta. The support type and its coordinates may depend on both qq and θ\theta.

In plain English

Under the joint edge–template law, if on an event GG determined by (q,θ)(q,\theta) the measure ν~q\widetilde\nu_q puts mass at least 1−3η21-3\eta^2 on a support U(q,θ)U(q,\theta) (a row, a column, or at most two states), then the probability that GG holds and the actual point state X(p)X(p) lies outside U(q,θ)U(q,\theta) is at most 8η8\eta.

Why it's here

This lemma lets a concentration statement about the sampled-history measure ν~q\widetilde\nu_q be turned into a statement about the actual point state X(p)X(p), with a loss of only O(η)O(\eta). The support may be chosen adaptively, with its type and coordinates depending on both qq and θ\theta. The common-variation proposition and its claims rely on this to locate the true point inside the selected support.
Classified routine:
A Markov/averaging transfer from the sampled-history measure to the actual point state, of the kind used for conditional-expectation arguments. It is technical bookkeeping inside the paper's framework rather than a new idea.

Uses

Nothing else in the paper

Used by

propCommon variation is negligibleclaimTemplate slices and bad-slot probabilityclaimSlice score lower bound via classification

Sources

PaperOpen
Section
§6.1 From sampled histories to the actual point
Page
—
Label
com:transfer
Line
sections/05-common-levels.tex:111
Leannot aligned

Phase 2 aligns this node to a Lean declaration.