OAI/MeasureTheory/Falconer/Estimates/ScalarGroupedPaths.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact branching counts and first splits across groups of regularized dyadic levels. No abstract replacement for the original path set is used.

  1. theorem OAI.Falconer.Regularization.scalar_grouped_children_card line 10
  2. theorem OAI.Falconer.Regularization.scalar_first_prefix_split line 29
  3. theorem OAI.Falconer.Regularization.scalar_grouped_children_separated line 42