OAI/MeasureTheory/Falconer/Angular/InverseSphereFubini.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Original-pair and sphere integration of one inverse term

The spatial inverse power is separated after exchanging the sphere and original endpoint integrations. All measures on the endpoints remain the original restrictions; the Fourier multipliers have modulus one.

  1. theorem OAI.Falconer.spatial_inverse_sphere_joint_integrable line 17
  2. theorem OAI.Falconer.spatial_inverse_sphere_term_integrable line 56
  3. theorem OAI.Falconer.spatial_inverse_sphere_separation line 72