OAI/MeasureTheory/Falconer/Recursion/ProfileGainAccounting.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Add normal and good interval gains while charging the actual chord-error length and one fixed weak loss per interval.

  1. def OAI.Falconer.profileGainExponent line 11
  2. theorem OAI.Falconer.profile_gain_exponent_sum line 15
  3. theorem OAI.Falconer.profile_gain_exponent_lower line 27