OAI/MeasureTheory/Falconer/Recursion/FrequencyIntervals.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Covering the actual radial interval by its dyadic frequency annuli

  1. def OAI.Falconer.radialIntervalMeasure line 12
  2. instance OAI.Falconer.radialIntervalMeasure_finite line 15
  3. theorem OAI.Falconer.radial_interval_cover_step line 20
  4. theorem OAI.Falconer.radial_interval_measure_step line 31
  5. theorem OAI.Falconer.radial_interval_dyadic_cover line 43