OAI/MeasureTheory/Falconer/Fourier/ScaledInverseIntegration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integrating the complete cell-scaled inverse

Every term uses the original endpoint measures. The distance weight is separated at the cell scale, and the radial coefficient is kept explicit.

  1. def OAI.Falconer.scaledInverseTerm line 16
  2. theorem OAI.Falconer.scaledWeightedInverseSum_eq_terms line 24
  3. theorem OAI.Falconer.scaledWeightedInverseSum_integrable line 36
  4. theorem OAI.Falconer.scaled_inverse_integration line 61