OAI/MeasureTheory/Falconer/Recursion/OrderedProfilePower.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Power accounting for the actual ordered-interval induction.

  1. theorem OAI.Falconer.list_prod_two_rpow line 9
  2. theorem OAI.Falconer.profileEndpointBound_ordered_power line 17