claimroutineinferred_dep

Fourier mass on indicated frequency coset

Fourier mass on the indicated coset is at least

2^{-\ell r_{\rm s}}(\alpha/8)^2

makes the decoder hit the right coset

Claim·§5.6 Decoding the row advice·inside lemFourier decoding agrees with positive probability

Statement (paper)

With

\theta_\sigma=(\sigma|_H)\otimes z'

, one has

\E_\sigma\left[\mathbf 1_{\{\sigma|_H\ne0\}}\sum_{\Phi\in\theta_\sigma+H^*\otimes Z'}|\widehat f_\sigma(\Phi)|^2\right]\ge 2^{-\ell r_{\rm s}}\E_\sigma\bigl[\mathbf 1_{\{\sigma|_H\ne0\}}C_\sigma^2\bigr]\ge 2^{-\ell r_{\rm s}}(\alpha/8)^2,

i.e. the

O

-decoder samples a nontrivial restriction and a frequency in the coset

\theta_\sigma+H^*\otimes Z'

with at least this probability.

In plain English

With

\theta_\sigma=(\sigma|_H)\otimes z'

, the expected squared Fourier mass of

f_\sigma

on the coset

\theta_\sigma+H^*\otimes Z'

, restricted to

\sigma

with

\sigma|_H\ne0

, is at least

2^{-\ell r_{\rm s}}(\alpha/8)^2

. Equivalently, the

O

-decoder samples a nontrivial restriction and a frequency in that coset with at least this probability.

Why it's here

The previous claim gives average slice correlation

|C_\sigma|

of at least

\alpha/8

over nontrivial restrictions. Here that is converted into Fourier mass on the coset, losing a factor

2^{-\ell r_{\rm s}}

and squaring the bound via Cauchy–Schwarz/Jensen, so the decoder's chosen frequency lies in the right coset with the stated probability. The next claim uses this to show the decoded vector falls in the projected answer set.

Classified routine:

This is a standard Fourier-analytic step: Parseval bounds the coset Fourier mass below by the squared slice correlation, with a loss of

2^{-\ell r_s}

for the coset size. Jensen/Cauchy–Schwarz then squares the average bound from the previous claim.

Uses

claimSlice correlation survives nontrivial restriction

Used by

claimDecoded vector lands in projected answer set

Sources

PaperOpen

Section: §5.6 Decoding the row advice
Page: —
Label: —
Line: sections/04-matrix.tex:712

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Fourier mass on indicated frequency coset" rests on claim-lem-fourier-coset-decoding-1