OAI/MeasureTheory/Falconer/Radial/PublishedRadialMoment.lean

The exact all-dimensional published radial moment input

T. Orponen, On the dimension and smoothness of radial projections, Analysis & PDE 12 (2019), 1273–1294, proof of Theorem 1.13, equations (3.5)–(3.6), printed pp. 1290–1292. https://msp.org/apde/2019/12-5/apde-v12-n5-p06-s.pdf

Only s=h+delta/2, t=h-delta/4, p=1+delta/(8h) in dimension h+1 are used. The strict parameter inequalities are proved locally. On disjoint compact supports the source weight |x-y|^(-h) and its inverse are uniformly bounded, so the published moment yields this unweighted finite moment and absolute continuity. The reference measure is the actual Euclidean surface measure. The moment bound concerns the radial projection and its absolute continuity.