OAI/MeasureTheory/Falconer/Angular/CubeCapacity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite dyadic capacities in the original ambient dimension

These capacities construct the compactly supported Frostman law needed by the application. At each occupied cube the available mass is the smaller of its geometric capacity and the total available mass of its children.

  1. def OAI.Falconer.cubeOccupied line 17
  2. def OAI.Falconer.cubeCapacity line 21
  3. theorem OAI.Falconer.cubeOccupied_nonneg line 26
  4. theorem OAI.Falconer.cubeCapacity_nonneg line 31
  5. theorem OAI.Falconer.cubeCapacity_le_occupied line 39
  6. theorem OAI.Falconer.cubeOccupied_le line 45
  7. theorem OAI.Falconer.content_le_cubeOccupied line 52
  8. theorem OAI.Falconer.content_le_cube_children line 68
  9. theorem OAI.Falconer.ofReal_finset_sum_nonneg line 76
  10. theorem OAI.Falconer.content_le_cubeCapacity line 88
  11. theorem OAI.Falconer.exists_uniform_cube_capacity line 107