OAI/MeasureTheory/Falconer/Estimates/CommonTubePower.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Separating the scale power from the truncated common-tube kernel.

  1. theorem OAI.Falconer.truncatedPlanarDistance_inverse_power_le line 10
  2. theorem OAI.Falconer.intersect_tube_power_bound line 22