claimroutineinferred_dep

Young's inequality absorbs tail moment

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

Statement (paper)

Eventually 12At≤6ϑtC0AtS+Cm≤14At+36C0ϑt2S+Cm\tfrac12 A_t\le 6\vartheta_t\sqrt{C_0A_tS}+C_m\le \tfrac14 A_t+36C_0\vartheta_t^2S+C_m, and consequently AtS≤144C0ϑt2+4CmS⟶0\dfrac{A_t}{S}\le 144C_0\vartheta_t^2+\dfrac{4C_m}{S}\longrightarrow0.

In plain English

Eventually 12At≤6ϑtC0AtS+Cm≤14At+36C0ϑt2S+Cm\tfrac12 A_t\le 6\vartheta_t\sqrt{C_0A_tS}+C_m\le \tfrac14 A_t+36C_0\vartheta_t^2S+C_m, which gives At/S≤144C0ϑt2+4Cm/S→0A_t/S\le 144C_0\vartheta_t^2+4C_m/S\to0, so the tail moment AtA_t is o(S)o(S).

Why it's here

The edge-averaged inequality (with the factor 1−dP,min⁡−11-d_{P,\min}^{-1}, eventually at least 12\tfrac12) is combined with the layer-cake bound ϑtC0AtS\vartheta_t\sqrt{C_0A_tS} on the min-expectation. Young's inequality then moves 14At\tfrac14A_t to the left, and since ϑt=o(1)\vartheta_t=o(1) and CmC_m is constant while S→∞S\to\infty, this yields At=o(S)A_t=o(S), which is the tail bound of the parent lemma.
Classified routine:
Direct combination of the two preceding claims (neighbor-pair averaging and the layer-cake bound) with the elementary AM-GM/Young inequality 6ϑC0AS≤14A+36C0ϑ2S6\vartheta\sqrt{C_0AS}\le \tfrac14A+36C_0\vartheta^2S, followed by rearrangement to get At=o(S)A_t=o(S).

Uses

claimAveraging over neighbor pairsclaimLayer-cake bound on capped min-expectation

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Young's inequality absorbs tail moment" rests on claim-ext-tail-2
  • info
    inferred_dep
    outline: "Young's inequality absorbs tail moment" rests on claim-ext-tail-3