claimroutineinferred_dep

Layer-cake bound on capped min-expectation

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

Statement (paper)

With

F_u=\{p:H_p^*>\max(u,R_0S)\}

G_u=\{q:H_q^*>u\}

h_P(u)=\mu(F_u)

h_Q(u)=\kappa(G_u)

and

\vartheta_t=\gamma^{-(1+2\eta)}(C_0/R_0)^\eta+\gamma^{-1}\xi_t=o(1)

, we have

\E_E[\min(H_p^*,H_q^*)\mathbf1_T]=\int_0^\infty\Prob_E(F_u,G_u)\dd u\le\vartheta_t\Bigl(\int_0^\infty h_P(u)\dd u\Bigr)^{1/2}\Bigl(\int_0^\infty h_Q(u)\dd u\Bigr)^{1/2}=\vartheta_t\sqrt{A_t\E_\kappa H_q^*}\le\vartheta_t\sqrt{C_0A_tS}.

In plain English

The expectation of

\min(H_p^*,H_q^*)

on the event

T

under the edge measure is written as an integral over

u

of the edge mass of

F_u\times G_u

. Expansion and Cauchy–Schwarz bound it by

\vartheta_t\sqrt{A_t\,\E_\kappa H_q^*}

, which is at most

\vartheta_t\sqrt{C_0A_tS}

, where

\vartheta_t=o(1)

Why it's here

The layer-cake formula turns the min into an integral of joint edge masses of the superlevel sets

F_u

and

G_u

. The expansion bound from the incidence piece gives

\Prob_E(F_u,G_u)\le\sqrt{h_P(u)h_Q(u)}\,((h_Ph_Q)^\eta+\xi_t)

. Using the cap

R_0S

and the marginal lower bound with

\gamma

, this is at most

\vartheta_t\sqrt{h_Ph_Q}

, and Cauchy–Schwarz in

u

finishes. The resulting

o(1)

factor in front of

\sqrt{A_tS}

is what the next step, absorbing the tail moment by Young's inequality, needs.

Classified routine:

A layer-cake formula followed by Cauchy–Schwarz in the level parameter, applied to the expansion bound supplied by the inc-piece proposition. It is standard bookkeeping inside the tail estimate.

Uses

propIncidence piece with degree and expansion control

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:142

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Layer-cake expansion bound on capped expectation" rests on inc:piece