lemmaroutine

Pointwise bound on H_p^* via two neighbors

Lemma·ext:pointwise·§7.1 A pointwise estimate and its tail consequence

Statement (paper)

For every p∈Pp\in P and every pair of distinct neighbors q,q′∈Qq,q'\in Q, 2Hp∗≤3(Hq∗+Hq′∗+mpq+mpq′)+Wc+Wb+2log⁡2. 2H_p^*\le 3\bigl(H_q^*+H_{q'}^*+m_{pq}+m_{pq'}\bigr) +W_c+W_b+2\log 2.

In plain English

For every point p∈Pp\in P and any two distinct neighbors q,q′∈Qq,q'\in Q of pp, 2Hp∗≤3(Hq∗+Hq′∗+mpq+mpq′)+Wc+Wb+2log⁡22H_p^*\le 3(H_q^*+H_{q'}^*+m_{pq}+m_{pq'})+W_c+W_b+2\log 2.

Why it's here

This bounds the quantity Hp∗H_p^* at a point by the same quantity at two of its neighbors, plus the edge terms mpqm_{pq}, mpq′m_{pq'} and constant error terms WcW_c, WbW_b, 2log⁡22\log 2. On the tail set where Hp∗H_p^* is large, these constants can be absorbed, which yields the capped inequality used in the tail estimate.
Classified routine:
A pointwise inequality obtained by local bookkeeping: H_p^* at one point is compared with H_q^* and H_{q'}^* at two neighbors via the edge terms and fixed error constants. It feeds the tail estimate and is not itself a headline idea, so it is classed as routine; the exact entropy-style argument behind it cannot be confirmed from the given information.

Uses

Nothing else in the paper

Used by

claimCapped pointwise inequality on tail set

Sources

PaperOpen
Section
§7.1 A pointwise estimate and its tail consequence
Page
—
Label
ext:pointwise
Line
sections/06-extraction.tex:32
Leannot aligned

Phase 2 aligns this node to a Lean declaration.