lemmaroutine

Tail of H star is negligible

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

Statement (paper)

Let R0=ϵ−2=k1/8R_0=\epsilon^{-2}=k^{1/8}. Then Eμ[Hp∗1{Hp∗>R0S}]=o(S). \E_\mu\bigl[H_p^*\mathbf1_{\{H_p^*>R_0S\}}\bigr]=o(S).

In plain English

With R0=ϵ−2=k1/8R_0=\epsilon^{-2}=k^{1/8}, the tail moment Eμ[Hp∗1{Hp∗>R0S}]\E_\mu[H_p^*\mathbf1_{\{H_p^*>R_0S\}}] is o(S)o(S).

Why it's here

The proof shows that points with very large Hp∗H_p^* contribute negligibly. It averages the capped pointwise inequality over a point and two neighbors, bounds the resulting min-expectation by a layer-cake and Cauchy–Schwarz argument with an o(1)o(1) factor, and absorbs the tail moment with Young's inequality. This truncation lets later steps, such as the band of accurate wedges, work with Hp∗H_p^* bounded by R0SR_0S at an o(S)o(S) cost.
Classified routine:
A truncation estimate proved by averaging a pointwise inequality, then applying layer-cake, Cauchy–Schwarz and Young's inequality. These are standard analytic tools used for bookkeeping inside the paper's extremal argument.

Uses

Nothing else in the paper

Used by

lemCommon height band of accurate wedges

Inside the proof

claimCapped pointwise inequality on tail setclaimAveraging over neighbor pairsclaimLayer-cake bound on capped min-expectationclaimYoung's inequality absorbs tail moment

Sources

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

Phase 2 aligns this node to a Lean declaration.