OAI/MeasureTheory/Falconer/Estimates/ScalarInitialChildren.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The local geometric extraction at a block of the original dyadic tree. Large child families retain a fixed proportion and have a witnessed intermediate separation scale; small families can collapse.

  1. theorem OAI.Falconer.scalar_initial_children line 10
  2. theorem OAI.Falconer.scalar_small_children line 30