OAI/MeasureTheory/Falconer/Recursion/ProfileEndpointBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The induction statement retains the original reference profile. Its single budget bounds parent mass loss, pencil regularity and pencil size ratio.

  1. def OAI.Falconer.QuarterPencilData line 13
  2. def OAI.Falconer.ProfileEndpointBound line 20
  3. theorem OAI.Falconer.QuarterPencilData.mono line 34
  4. theorem OAI.Falconer.profileEndpointBound_trivial line 43
  5. theorem OAI.Falconer.ProfileEndpointBound.mono_budget line 52
  6. theorem OAI.Falconer.ProfileEndpointBound.mono_value line 61
  7. theorem OAI.Falconer.profileEndpointBound_retained_subset line 68