AngularPairSwap.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Fubini for the spatially expanded angular term

Bounded measurable amplitudes on finite original laws are sufficient. There is no spatial differentiability requirement and no change of the point labels in the two endpoint factors.

theorem OAI.Falconer.angular_pair_spatial_swap line 16