OAI/MeasureTheory/Falconer/Recursion/ScalarBranchGrowth.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite scalar branching with a reserved separation margin. This records exactly the tail-motion bookkeeping of the nonporous argument.

  1. theorem OAI.Falconer.scalar_branch_union_separated line 10
  2. theorem OAI.Falconer.scalar_branch_union_card line 34
  3. theorem OAI.Falconer.scalar_finite_branch_growth line 55