OAI/MeasureTheory/Falconer/Recursion/OrderedEndpointIntervals.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Apply interval gains to an ordered subfamily; omitted gaps use the nonempty-pencil estimate. No gain or profile hypothesis is imposed on a gap.

  1. def OAI.Falconer.OrderedBlockIntervals line 11
  2. theorem OAI.Falconer.OrderedBlockIntervals.end_le line 15
  3. theorem OAI.Falconer.profileEndpointBound_ordered_intervals line 21