OAI/MeasureTheory/Falconer/Estimates/FarRegionScales.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform shell regimes throughout the actual far region

  1. theorem OAI.Falconer.shell_regime_of_lower_distance line 10
  2. theorem OAI.Falconer.comparableFarRegion_lower line 27
  3. theorem OAI.Falconer.leftNoncomparableFar_lower line 34
  4. theorem OAI.Falconer.rightNoncomparableFar_lower line 47
  5. theorem OAI.Falconer.far_band_frequency_mono line 60