claimroutineinferred_dep

Summing shell estimates over radii

Sums shell bounds over radii by bounded overlap; far radii negligible
assembles the ball bound for general data
Claim·§B.1 Observation on a ball·inside lemLocal smoothing bound on small balls

Statement (paper)

Divide [T,2T][T,2T] into intervals of length between R/2R/2 and RR, centered at QiQ_i, and let hi(u,ω)=(Qi+u)αf((Qi+u)ω)1∣u∣≤5Rh_i(u,\omega)=(Q_i+u)^\alpha f((Q_i+u)\omega)\mathbf1_{|u|\le5R}. Then the input shells have bounded overlap, so ∑i∥hi∥pp≲T∥f∥pp\sum_i\|h_i\|_p^p\lesssim T\|f\|_p^p, and the profile estimate summed over ii gives the desired bound for the contribution of the radii ∣s−Qi∣≤5R|s-Q_i|\le5R. For T/2≤s≤3TT/2\le s\le3T with ∣s−Qi∣>5R|s-Q_i|>5R, the remaining kernel is bounded by CDs−α1∣t−s∣>3R⟨t−s⟩−DC_D s^{-\alpha}\mathbf1_{|t-s|>3R}\langle t-s\rangle^{-D}, and Young's inequality in tt bounds this contribution by CDRn/p+1−DT1/p∥f∥pC_D R^{n/p+1-D}T^{1/p}\|f\|_p; the radii outside [T/2,3T][T/2,3T] again give rapid decay in T+sT+s.

In plain English

Splitting [T,2T][T,2T] into intervals of length comparable to RR with centers QiQ_i, the shell data hih_i have bounded overlap, so ∑i∥hi∥pp≲T∥f∥pp\sum_i\|h_i\|_p^p\lesssim T\|f\|_p^p. Summing the profile estimate over ii bounds the contribution of radii ∣s−Qi∣≤5R|s-Q_i|\le5R, and the contribution of the remaining radii is bounded by CDRn/p+1−DT1/p∥f∥pC_D R^{n/p+1-D}T^{1/p}\|f\|_p, with radii outside [T/2,3T][T/2,3T] giving rapid decay in T+sT+s.

Why it's here

This turns the single-shell bound of the previous claim into a bound for general ff. Near radii are handled by applying the profile operator estimate to each hih_i and summing using bounded overlap of the shells. Far radii are handled by the kernel decay ⟨t−s⟩−D\langle t-s\rangle^{-D} with Young's inequality in tt, so the remainder is negligible for large DD.
Classified routine:
Standard decomposition into shells of width comparable to R with a bounded-overlap summation, plus Young's inequality applied to the rapidly decaying off-diagonal kernel; it follows directly from the preceding shell profile estimate.

Uses

claimShell profile operator approximates propagator

Used by

Nothing in the paper

Sources

PaperOpen
Section
§B.1 Observation on a ball
Page
—
Label
—
Line
sections/angular.tex:139
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Summation over shells and remainder kernel" rests on claim-lem-angular-ball-2