OAI/MeasureTheory/Falconer/Estimates/ScalarSeparatedTree.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite separated cluster trees. This geometric data will be extracted from the dyadic regularization; no extraction or nonconcentration theorem is assumed here. Leaves are original points and all parent sets are exact unions of their children.

  1. structure OAI.Falconer.ScalarSeparatedTree line 11
  2. theorem OAI.Falconer.ScalarSeparatedTree.child_nonempty line 31
  3. theorem OAI.Falconer.ScalarSeparatedTree.points_card line 37
  4. theorem OAI.Falconer.ScalarSeparatedTree.points_nonempty line 68