OAI/MeasureTheory/Falconer/Estimates/CommonTubePacking.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Separation supplies a second common-tube bound, independent of the pencil cardinality. Interpolating it with regularity detects large pencils.

  1. theorem OAI.Falconer.common_tube_packing_bound line 11
  2. theorem OAI.Falconer.intersect_tube_packing_bound line 69