OAI/MeasureTheory/Falconer/Estimates/DyadicAveraging.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite dyadic averaging and the energy increment identity.

  1. def OAI.Falconer.dyadicAverage line 8
  2. theorem OAI.Falconer.dyadicAverage_nonneg line 12
  3. theorem OAI.Falconer.dyadicAverage_mono line 18
  4. theorem OAI.Falconer.dyadicAverage_const line 24
  5. theorem OAI.Falconer.dyadicAverage_add line 30
  6. theorem OAI.Falconer.dyadicAverage_sub line 37
  7. theorem OAI.Falconer.dyadicAverage_mul line 44
  8. theorem OAI.Falconer.dyadicAverage_comp line 50
  9. theorem OAI.Falconer.dyadicSlopeEnergy_eq_average line 57
  10. theorem OAI.Falconer.dyadicSlopeVariance_eq_average line 64
  11. theorem OAI.Falconer.dyadicAverage_centered_variance line 71
  12. theorem OAI.Falconer.dyadicAverage_markov line 82