OAI/MeasureTheory/Falconer/Incidence/IncidenceBucketBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The pencil-cardinality pigeonhole has only a linear cost in the chosen block depth, with a fixed additive cost depending on the block width.

  1. theorem OAI.Falconer.incidence_bucket_count_bound line 10
  2. theorem OAI.Falconer.incidence_packing_factor_bound line 33