OAI/MeasureTheory/Falconer/Estimates/SelectedRegularFiber.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Select an actual incident tube and a regular subset of its point fiber.

  1. theorem OAI.Falconer.pencilFiberEnergy_mono line 10
  2. theorem OAI.Falconer.regular_fiber_of_pencil_degree line 27