OAI/MeasureTheory/Falconer/Incidence/RegularEnergyPencils.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The high-energy deletion with its geometric budgets discharged.

  1. def OAI.Falconer.pencilEnergyBudget line 11
  2. def OAI.Falconer.pencilMomentBudget line 15
  3. def OAI.Falconer.pencilEnergyCutoff line 19
  4. theorem OAI.Falconer.prune_pencil_fiber_energy line 24