OAI/MeasureTheory/Falconer/Shells/FrequencyShell.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Gaussian localization for the actual frequency-shell law

  1. theorem OAI.Falconer.measurableSet_radialFrequencyAnnulus line 13
  2. instance OAI.Falconer.radialFrequencyMeasure_finite line 17
  3. theorem OAI.Falconer.radial_frequency_support line 32
  4. theorem OAI.Falconer.radial_frequency_polynomial_balls line 44
  5. theorem OAI.Falconer.radial_frequency_gaussian line 67