OAI/MeasureTheory/Falconer/Estimates/ScalarClusterTree.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Separated cluster trees retain all leaves in each terminal fiber. Their common terminal cardinality multiplies every level of the gain.

  1. structure OAI.Falconer.ScalarClusterTree line 9
  2. theorem OAI.Falconer.ScalarClusterTree.child_nonempty line 33
  3. theorem OAI.Falconer.ScalarClusterTree.points_card line 39
  4. theorem OAI.Falconer.ScalarClusterTree.points_nonempty line 70