OAI/MeasureTheory/Falconer/Recursion/OrderedProfileIntervals.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Length and endpoint accounting for ordered profile intervals.

  1. theorem OAI.Falconer.ordered_interval_length_le line 9
  2. theorem OAI.Falconer.ordered_interval_count_bound line 24
  3. theorem OAI.Falconer.ordered_profile_increment_lower line 39