claimroutineinferred_dep

Averaging over neighbor pairs

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

Statement (paper)

With

A_t=\E_\mu[H_p^*\mathbf1_T]

, where

p\sim\mu

and two neighbors are drawn independently and uniformly given

p

, one has

(1-d_{P,\min}^{-1})A_t\le 6\E_E[\min(H_p^*,H_q^*)\mathbf1_T]+C_m,

where

C_m

is an absolute upper bound for

6\E_E m_{pq}

In plain English

Writing

A_t=\E_\mu[H_p^*\mathbf1_T]

for the tail moment, averaging over a point

p

and two independently chosen neighbors gives

(1-d_{P,\min}^{-1})A_t\le 6\E_E[\min(H_p^*,H_q^*)\mathbf1_T]+C_m

, where

C_m

is an absolute bound on

6\E_E m_{pq}

Why it's here

This averages the capped pointwise inequality of the previous claim over

p\sim\mu

and over pairs of distinct neighbors. It converts a bound on

H_p^*

at a single point into a bound on the edge average of

\min(H_p^*,H_q^*)

on the tail set, plus the constant

C_m

. The factor

1-d_{P,\min}^{-1}

reflects excluding the case where the two neighbors coincide. The resulting edge-averaged bound is what the Young's inequality step then uses to absorb the tail moment

A_t

Classified routine:

Direct averaging of the previous capped pointwise inequality (claim-ext-tail-1) over p and pairs of neighbors. The only extra bookkeeping is the factor accounting for coincident neighbor pairs.

Uses

claimCapped pointwise inequality on tail set

Used by

claimYoung's inequality absorbs tail moment

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Averaging over neighbor pairs" rests on claim-ext-tail-1