OAI/MeasureTheory/Falconer/Radial/PlateScales.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Dyadic powers and the earlier scale used by the coarse plate filter

  1. def OAI.Falconer.plateScale line 12
  2. theorem OAI.Falconer.plateScale_eq line 14
  3. theorem OAI.Falconer.plateScale_pos line 17
  4. theorem OAI.Falconer.plateScale_le_one line 20
  5. theorem OAI.Falconer.plateScale_antitone line 23
  6. theorem OAI.Falconer.plateScale_rpow line 28
  7. theorem OAI.Falconer.plateScale_tendsto line 35
  8. theorem OAI.Falconer.plateScale_power_tendsto line 40
  9. theorem OAI.Falconer.plateScale_div_lower line 46
  10. theorem OAI.Falconer.plateScale_div_upper line 54
  11. theorem OAI.Falconer.plateScale_div_power line 67
  12. theorem OAI.Falconer.plate_exponent_gaps line 75