OAI/MeasureTheory/Falconer/Recursion/PotentialFrostman.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-scale ball bounds control the regularized slicing potential

  1. theorem OAI.Falconer.regularized_potential_frostman line 12
  2. theorem OAI.Falconer.regularized_potential_global line 60