lemmaroutineunresolved_ref

Exponentially mixing averaging operator on conditional space

Rational averaging operator KK has ∥Kd−Π∥≤Cs2−csd\|K^d-\Pi\|\le C_s2^{-c_sd} in LsL_s
makes conditional averaging nearly exact
Lemma·lem:env-gap·§6 Conditional averaging in the shared environment

Statement (paper)

Consider the fixed product of rank channels, conditioned on retention of one specified identifier per conditioned channel. Include any designated set of independent uniform bits, with length padded to a multiple of HH, and freeze any remaining independent bits. There is a rational Markov averaging operator KK on this conditional space such that its stationary distribution is the indicated uniform conditional law and, for each fixed 2≤s<∞2\le s<\infty, ∥Kd−Π∥Ls→Ls≤Cs2−csd(d≥0). \|K^d-\Pi\|_{L_s\to L_s}\le C_s2^{-c_sd} \qquad(d\ge0). Here Π\Pi is conditional expectation over the variables being averaged. The constants are independent of the field size, retention side lengths, bit lengths, indicated identifiers, and frozen bits.

In plain English

On the conditional space of the fixed product of rank channels (with one retained identifier per conditioned channel, designated uniform bits included and the rest frozen), there is a rational Markov operator KK whose stationary law is the uniform conditional law. For each fixed 2≤s<∞2\le s<\infty, ∥Kd−Π∥Ls→Ls≤Cs2−csd\|K^d-\Pi\|_{L_s\to L_s}\le C_s2^{-c_sd}, where Π\Pi is conditional expectation over the averaged variables, with constants independent of field size, retention side lengths, bit lengths, identifiers and frozen bits.

Why it's here

This turns the uniform spectral gap for the affine group walk (lem-env-affine) into an explicit, rational, size-independent exponential contraction in every LsL_s norm, s≥2s\ge2, on the conditional space. Downstream, it lets the conditional averaging steps (such as the prefix bounds and the clean-block independence arguments) treat KdK^d as nearly exact conditional expectation, with error decaying like 2−csd2^{-c_sd} regardless of the parameters.
Classified routine:
Follows from the uniform spectral gap of the affine group walk (lem-env-affine) via standard conversion of an L_2 spectral gap into L_s contraction (Riesz–Thorin interpolation with the trivial L_infty bound), with the conditional space handled by bookkeeping over product structure and frozen bits.

Uses

lemUniform spectral gap for affine group actions

Used by

lemMean prefixes small, noise prefixes tinylemClean calculation is independent of the salt

Sources

PaperOpen
Section
§6 Conditional averaging in the shared environment
Page
—
Label
lem:env-gap
Line
sections/averaging.tex:108
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • warn
    unresolved_ref
    L_s contraction uses the external Riesz–Thorin interpolation theorem.