SpatialSharedBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Spatial Fourier integration followed by sphere Cauchy--Schwarz

This transfers the actual shared-angle integral of a separated inverse term to positive independent-angle energies, at the squared L1 cost of its spatial Fourier coefficient.

theorem OAI.Falconer.spatial_shared_integral_sq_le line 18