OAI/MeasureTheory/Falconer/Radial/RadialIntervalEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Converting the proved frequency bound back to angular averages

  1. theorem OAI.Falconer.radial_interval_lintegral line 12
  2. theorem OAI.Falconer.dyadic_half_dimensional_average line 21