OAI/MeasureTheory/Falconer/Recursion/RoundedProfileGain.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The rounded decomposition supplies the actual normal/good cell hypotheses and retains a definite length of good cells.

  1. theorem OAI.Falconer.profileHighLength_nonneg line 12
  2. theorem OAI.Falconer.profileHighLength_antitone line 22
  3. theorem OAI.Falconer.rounded_profile_gain_cells line 40
  4. theorem OAI.Falconer.rounded_profile_good_length line 67