OAI/MeasureTheory/Falconer/Incidence/BlockPrefixBallBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Interpolate finite prefix tests between selected block depths. Only the actual maximum depth gap is charged, before passing to geometric balls.

  1. theorem OAI.Falconer.pointPrefixFiber_subset_take line 11
  2. theorem OAI.Falconer.dyadic_prefix_gap_bound line 20
  3. theorem OAI.Falconer.finite_block_prefix_ball_bound line 34