OAI/MeasureTheory/Falconer/Fourier/SeparatedInverseIntegration.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Integration of the actual finite separated inverse

The original endpoint laws are retained. Each finite angular factor is integrated through the one-order spatial Fourier identity, with its actual conjugation convention and no additional integrability assumptions.

  1. theorem OAI.Falconer.separated_factor_measurable line 19
  2. theorem OAI.Falconer.separated_sphere_integrable line 24
  3. theorem OAI.Falconer.separated_inverse_term_integrable line 51
  4. theorem OAI.Falconer.separated_sphere_spatial_integration line 96
  5. theorem OAI.Falconer.separated_inverse_integration line 151