OAI/MeasureTheory/Falconer/Recursion/ProfileNormalBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The critical second-moment estimate supplies the normal-interval base case of the recursive profile endpoint bound.

  1. theorem OAI.Falconer.profileEndpointBound_normal line 11