OAI/MeasureTheory/Falconer/Estimates/DyadicSlopeEnergy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Dyadic slope energies for the quantitative differentiation of the planar branching profile. Only the Lipschitz constant two is needed.

  1. def OAI.Falconer.intervalSecantSlope line 10
  2. theorem OAI.Falconer.intervalSecantSlope_abs_le line 13
  3. theorem OAI.Falconer.intervalSecantSlope_children line 21
  4. def OAI.Falconer.dyadicSlopeEnergy line 29
  5. theorem OAI.Falconer.dyadicSlopeEnergy_nonneg line 33
  6. theorem OAI.Falconer.dyadicSlopeEnergy_le_four line 39
  7. theorem OAI.Falconer.dyadicSlopeEnergy_step_mono line 52
  8. theorem OAI.Falconer.dyadicSlopeEnergy_mono line 68