claimroutineinferred_dep

Capped pointwise inequality on tail set

Claim·§7.1 A pointwise estimate and its tail consequence·inside lemTail of H star is negligible

Statement (paper)

For all sufficiently large indices and every p∈T={p:Hp∗>R0S}p\in T=\{p:H_p^*>R_0S\}, and for distinct neighbors q,q′q,q' of pp, Hp∗≤3(min⁡(Hp∗,Hq∗)+min⁡(Hp∗,Hq′∗)+mpq+mpq′).H_p^*\le3\bigl(\min(H_p^*,H_q^*)+\min(H_p^*,H_{q'}^*)+m_{pq}+m_{pq'}\bigr).

In plain English

For sufficiently large indices, if Hp∗>R0SH_p^*>R_0S and q,q′q,q' are distinct neighbors of pp, then Hp∗≤3(min⁡(Hp∗,Hq∗)+min⁡(Hp∗,Hq′∗)+mpq+mpq′)H_p^*\le 3(\min(H_p^*,H_q^*)+\min(H_p^*,H_{q'}^*)+m_{pq}+m_{pq'}).

Why it's here

This turns the pointwise bound of Lemma 7.1 into a form with Hq∗H_q^* capped at Hp∗H_p^*, which is what the averaging step needs. On the tail set Hp∗>R0SH_p^*>R_0S is large, so the additive constants Wc+Wb+2log⁡2W_c+W_b+2\log 2 can be absorbed into the left side. Hence the factor 33 can be taken in place of the weaker coefficient, and the cap by min⁡\min follows because the bound is trivial when a neighbor's H∗H^* exceeds Hp∗H_p^*.
Classified routine:
Direct consequence of the pointwise bound (ext-pointwise): on the tail set the additive constants are absorbed into the left side, and the min-cap is trivial when a neighbor's H* exceeds H_p^*.

Uses

lemPointwise bound on H_p^* via two neighbors

Used by

claimAveraging over neighbor pairs

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Capped pointwise inequality on the tail set" rests on ext:pointwise