OAI/MeasureTheory/Falconer/Recursion/CriticalPotential.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic potential bound at the critical ball exponent

Unlike the strictly subcritical energy estimate, the finite critical estimate has one bounded contribution per dyadic scale. It is used on the outer intervals of the radial profile argument.

  1. theorem OAI.Falconer.regularized_potential_critical line 17