OAI/MeasureTheory/Falconer/Shells/SmoothShellPartition.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.sourceShellBump line 11
  2. def OAI.PlanarFalconer.sourceShellLowpass line 17
  3. def OAI.PlanarFalconer.sourceShellBand line 18
  4. theorem OAI.PlanarFalconer.sourceShellLowpass_smooth line 20
  5. theorem OAI.PlanarFalconer.sourceShellBand_smooth line 23
  6. theorem OAI.PlanarFalconer.sourceShellLowpass_one line 26
  7. theorem OAI.PlanarFalconer.sourceShellLowpass_zero line 33
  8. theorem OAI.PlanarFalconer.sourceShellBand_abs_le line 41
  9. theorem OAI.PlanarFalconer.sourceShellBand_support_bounds line 49
  10. theorem OAI.PlanarFalconer.sourceShellBand_support line 64
  11. theorem OAI.PlanarFalconer.sourceShellBand_compact line 73
  12. theorem OAI.PlanarFalconer.sourceShellPartition_telescope line 78
  13. theorem OAI.PlanarFalconer.sourceShellLowpass_tendsto line 84