OAI/MeasureTheory/Falconer/Recursion/LocalProfileCounts.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Local covering numbers and fiber ratios expressed in the actual branching profile, for the regular-scale incidence argument.

  1. theorem OAI.Falconer.Regularization.blockProduct_relative_profile line 10
  2. theorem OAI.Falconer.Regularization.blockClass_local_covering_count line 22
  3. theorem OAI.Falconer.Regularization.blockClass_fiber_ratio line 38
  4. theorem OAI.Falconer.Regularization.blockClass_local_fiber_profile line 63